[论文] Provably Complete Generalized Planning with LLMs

论文概要

研究领域: ML 作者: Katharina Stein, Chaahat Jain, Jörg Hoffmann, Alexander Koller 发布时间: 2026-09-25 arXiv: 2609.27105

中文摘要

广义规划旨在计算一个能解决规划领域所有实例的计划。近期工作用 LLM 自动生成并调试以 Python 程序形式表达的广义计划，在若干领域取得完美测试覆盖率。然而这些计划是否真的完备——即是否解决该领域所有实例——此前只能人工评估。本文提出一种方法：在 Lean 中自动生成广义计划，并给出其相对于输入的领域约束规范的形式化完备性证明。我们引入语义保持的 PDDL 到 Lean 转换，用 LLM 同时生成广义计划与"它解决每个满足领域约束的实例"的形式化证明。完备性证明的正确性由 Lean 内核判定。我们在 13 个常用基准领域上用 GPT-5.6-Sol 评估，其中 12 个领域获得了附带有效完备性证明的广义计划。这是自动广义规划完备性证明领域的一次重大进展。

原文摘要

Generalized planning aims to compute a plan that solves all instances of a planning domain. Recent work has used LLMs to automatically generate and debug such generalized plans in the form of Python programs and achieved perfect test data coverage for several domains. However, whether these generalized plans are actually complete, i.e. solve all instances of the domain, could only be determined by manual evaluation. Here, we present an approach for automatically generating generalized plans in Lean together with proofs of their completeness relative to a specification of the domain constraints provided as input. We introduce a semantic-preserving PDDL-to-Lean conversion, and use an LLM to generate both the generalized plan and the formal proof that it solves every instance satisfying the d...

#论文 #arXiv #ML #小凯