LLM自动生成完备性证明，13个规划领域12个拿下！
Provably Complete Generalized Planning with LLMs
📖 AI 总结
该研究针对广义规划中LLM生成的广义计划难以验证其完备性的问题，提出了一种自动生成可证明完备的广义计划的方法。作者设计了保持语义的PDDL到Lean转换，并利用LLM同时生成广义计划及其形式化完备性证明，证明的正确性由Lean内核保证。研究在13个常用基准域上使用GPT-5.6-Sol进行评估，其中12个域成功获得了带有有效完备性证明的广义计划。这一结果显著推进了自动广义规划完备性证明的技术水平，使广义计划的正确性从依赖人工评估转变为可由机器严格验证。
🔑 关键词速览
| Generalized Planning | 广义规划，指计算一个能解决某个规划领域中所有问题实例的通用规划，而非仅针对单个具体实例。 |
| PDDL | 规划领域定义语言，是人工智能规划中用于形式化描述规划领域和问题的标准语言。 |
| Lean | 一种交互式定理证明器与函数式编程语言，可用于形式化数学证明并借助其内核验证证明的正确性。 |
| Completeness Proof | 完备性证明，此处指形式化证明某个广义规划能够求解满足领域约束的所有实例。 |
| Semantic-preserving Conversion | 保持语义的转换，指在将 PDDL 描述转换为 Lean 表示时确保两者语义一致、不改变原意。 |
📱 每天一份 AI 前沿日报
关注公众号，每天 09:00 推送 · 不错过任何重磅