可证明完备的基于LLM的广义规划

中文摘要 AI 辅助

广义规划旨在计算一个能够解决规划领域所有实例的计划。近期的工作利用LLM自动生成和调试以Python程序形式表示的广义计划，并在多个领域实现了完美的测试数据覆盖率。然而，这些广义计划是否真正完备，即是否解决领域的所有实例，只能通过人工评估来确定。在此，我们提出一种方法，在Lean中自动生成广义计划，并附带相对于输入提供的领域约束规范的完备性证明。我们引入了一种保持语义的PDDL到Lean的转换，并使用LLM同时生成广义计划和形式化证明，证明该计划解决了满足领域约束的每个实例。完备性证明的正确性由Lean的内核确定。我们在13个常用基准领域上评估了我们的方法，使用GPT-5.6-Sol作为LLM。对于其中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 domain constraints. The correctness of the completeness proof is determined by Lean's kernel. We evaluate our approach on 13 commonly used benchmark domains, using GPT-5.6-Sol as the LLM. For 12 of the domains we obtain generalized plans together with valid completeness proofs. This is a major advancement of the state of the art in automatic generalized-plan completeness proofs.

发表机构

• Saarland University（萨尔大学）
• German Research Center for Artificial Intelligence (DFKI)（德国人工智能研究中心（DFKI））

机构由 AI 辅助整理，请以论文原文为准。