# Provably Complete Generalized Planning with LLMs

arXiv: https://arxiv.org/abs/2609.27105 · HTML: https://mlsanity.com/paper/2609.27105/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 30 references that are in the map.
- First posted on arXiv 22 Sep 2026.

## Builds on (most cited first, 10 of 10)

- [Learning General Optimal Policies with Graph Neural Networks: Expressive Power, Transparency, and Limits](https://mlsanity.com/paper/2109.10129/) (2021)
- [Learning Features and Abstract Actions for Computing Generalized Plans](https://mlsanity.com/paper/1811.07231/) (2018)
- [AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement](https://mlsanity.com/paper/2412.06176/) (2024)
- [APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning](https://mlsanity.com/paper/2505.05758/) (2025)
- [Automated Proof Generation for Rust Code via Self-Evolution](https://mlsanity.com/paper/2410.15756/) (2024)
- [Features, Projections, and Representation Change for Generalized Planning](https://mlsanity.com/paper/1801.10055/) (2018)
- [Faults in Our Formal Benchmarking: Dataset Defects and Evaluation Failures in Lean Theorem Proving](https://mlsanity.com/paper/2606.29493/) (2026)
- [Improved Generalized Planning with LLMs through Strategy Refinement and Reflection](https://mlsanity.com/paper/2508.13876/) (2025)
- [A Case Study on Emergent Cheating and Whistleblowing in Autonomous Research Swarms](https://mlsanity.com/paper/2609.04170/) (2026)
- [Guarantees for Sound Abstractions for Generalized Planning (Extended Paper)](https://mlsanity.com/paper/1905.12071/) (2019)

## Built on by (most cited first, 1 of 1)

- [Learning How to Search for Plans with Exponentially Less Space](https://mlsanity.com/paper/2610.10954/) (2026)

## Abstract (arXiv)

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.