An LLM generates generalized plans and completeness proofs in Lean, verified by Lean's kernel, using a semantics-preserving PDDL-to-Lean conversion.
Abstract
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.
Problem
Generalized planning seeks a single plan solving all instances of a PDDL planning domain. Prior LLM-generated generalized plans achieved high test coverage but their completeness (solving every valid instance) could only be checked manually.
Approach
A deterministic, domain-independent Python converter translates PDDL domains into a semantics-preserving Lean representation of states, actions, and instances. An LLM generates both a candidate generalized plan and a formal proof that it solves every instance satisfying the domain constraints. Lean's kernel verifies proof correctness, with automated debugging of LLM-generated Lean code.
Figure 2: Illustrations of the main steps of our approach for obtaining generalized plans in Lean and proving their completeness.
Results
Evaluated on 13 benchmark domains using GPT-5.6-Sol, the approach produced generalized plans with valid completeness proofs for 12 domains, advancing automatic generalized-plan completeness proving.
