Provably Complete Generalized Planning with LLMs

Katharina Stein; Chaahat Jain; Jörg Hoffmann; Alexander Koller

cs.AISep 22, 2026

Provably Complete Generalized Planning with LLMs

Authors: Katharina Stein, Chaahat Jain, Jörg Hoffmann, Alexander Koller

Organizations: Saarland Informatics Campus, Saarland University, Saarbrücken, Germany · German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany

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.

Figures & tables

Figure 1: Illustration of an example planning task from the Spanner domain and a strategy for solving all Spanner tasks.

Figure 2: Illustrations of the main steps of our approach for obtaining generalized plans in Lean and proving their completeness.

Panel of Figure 3 — Figure 3: PDDL examples from the Spanner domain.

Panel of Figure 4 — Figure 4: Conversion $\llbracket\cdot\rrbracket$ commutes with each applicable ground action when applying this single action (left). Iterating the square over a full plan shows that $\llbracket\cdot\rrbracket$ also commutes with applying a sequence of actions (right).

Basic proof generation
Domain	N interactions			Time
Domain	GP	Prf.	Decl.	GP	Prf.	total
Delivery	1	3	–	121	671	792
Ferry	2	3	–	104	586	690
Grippers	2	3	–	119	661	780
Heavy	1	3	–	36	495	531

Table 1: Number of LLM interactions and run time of the pipeline (in seconds) for generating the generalized plan (GP) and its completeness proof (Prf.). “N interactions” counts the number of interactions, i.e. input-output pairs, with the LLM, including the initial generation and all debugging iterations. The upper part shows the domains for which the basic approach succeeded, the lower part shows the results using the iterative approach on the other domains. For the iterative approach, “Decl.” reports the maximum number of debugging iterations required for a single declaration.

Basic proof generation
Domain	N decl. GP		N decl. Prf.
Domain	given	LLM	given	LLM
Delivery	56	3	92	15
Ferry	45	7	83	7
Grippers	51	9	102	23
Heavy	47	5	76	9

Table 2: Number of Lean code declarations (i.e., lemmas, theorems, and definitions) involved in generating the generalized plan (GP) and its completeness proof (Prf.). “Given” reports the number of declarations provided to the LLM as part of the prompt (e.g., the domain formalization and, for proof generation, the complete GP code); “LLM” reports the number of individual declarations generated by the LLM itself.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Domain	Source of debugging problems	Instance Generator
delivery	Silver et al. (2024)
ferry	IPC Learning track 2023 ( Taitler et al. 2024 )
heavy	Silver et al. (2024)
hiking	Silver et al. (2024)
miconic	Silver et al. (2024)
spanner	IPC Learning track 2023 ( Taitler et al. 2024 )

Appendix

Table 3: The origin of the debugging tasks that we used for our experiments and the instance generators based on which we created the validity constraints.

LLM Planning

Large language model planning studies how models decompose goals, choose actions, and revise plans under constraints.

See all 142 papers

LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs
Oct 6, 2026André G. Pereira, Augusto B. Corrêa, Felipe Meneguzzi +1Automated Heuristic Design LLM Planning
Federal University of Rio Grande do Sul Brazil · University of Oxford United Kingdom · University of Aberdeen United Kingdom +1
GenePlan: Evolving Better Generalized PDDL Plans using Large Language Models
Mar 10, 2026Andrew Murray, Danial Dervovic, Alberto Pozanco +1Symbolic Planning LLM-Based Program Synthesis
J.P. Morgan AI Research
Generating Instance Generators in PDDL Planning
Sep 5, 2026Nicola J. Müller, Naya Rudolph, Katharina Stein +3LLM-Based Program Synthesis
German Research Center for Artificial Intelligence (DFKI), Saarbrücken, Germany · Saarland University, Saarland Informatics Campus, Saarbrücken, Germany · Center for European Research in Trusted Artificial Intelligence (CERTAIN) +1

Oct 6, 2026J/K move · Enter open · S save

LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs

André G. Pereira, Augusto B. Corrêa, Felipe Meneguzzi, Jendrik Seipp

Federal University of Rio Grande do Sul Brazil · University of Oxford United Kingdom · University of Aberdeen United Kingdom+1

Automated Heuristic Design LLM Planning Sequential Decision Making Symbolic Planning Formal Verification

Open paper AskPDF arXiv

Frontier large language models (LLMs) can generate heuristic functions that guide search to achieve state-of-the-art performance in satisficing planning, where any plan is acceptable. However, these heuristics are not guaranteed to be admissible and can lead to suboptimal plans. We introduce LeanPlan, the first planning system that finds optimal plans with LLM-generated heuristics whose admissibility is machine-checked. Given a domain description and training tasks, an agentic loop uses planner feedback to iteratively improve a reusable domain-specific heuristic, its admissibility proof and the required domain assumptions. LeanPlan implements the heuristic, its proof and an efficient planner with machine-checked grounding and search in Lean 4. We evaluate LeanPlan on ten domains from the International Planning Competition and three new domains, using test tasks with up to 57 times as many objects as the training tasks. With GPT-5.6 Sol in the agentic loop, we successfully generate heuristics and admissibility proofs for all these domains. With the resulting heuristics, LeanPlan usually expands fewer states than the state-of-the-art Scorpion planner and solves more tasks overall.

Abstract

LLM Planning

Explore similar work

LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs

GenePlan: Evolving Better Generalized PDDL Plans using Large Language Models

Generating Instance Generators in PDDL Planning