Paper Overview
Research Area: ML Authors: Katharina Stein, Chaahat Jain, Jörg Hoffmann, Alexander Koller Published: 2026-09-25 arXiv: 2609.27105
Summary
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, achieving perfect test data coverage on several domains. However, whether these generalized plans are actually complete—i.e., solve all instances of the domain—could previously only be determined by manual evaluation.
This paper presents an approach for automatically generating generalized plans in Lean, together with proofs of their completeness relative to an input specification of the domain constraints.
Key contributions
- Semantic-preserving PDDL-to-Lean conversion: a translation of planning domain descriptions into Lean that preserves semantics.
- LLM-generated plans and proofs: an LLM generates both the generalized plan and a formal proof that it solves every instance satisfying the domain constraints.
- Machine-checked correctness: the validity of the completeness proof is determined by the Lean kernel.
Results
Evaluated with GPT-5.6-Sol on 13 common benchmark domains, the method obtained generalized plans with valid completeness proofs for 12 of the 13 domains.
This represents a major step toward automated, provably complete generalized planning with LLMs.
Original 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...
Paper: https://arxiv.org/abs/2609.27105
--- *Auto-collected on 2026-09-25*