Provably Complete Generalized Planning with LLMs

The four main steps of the approach: Lean encoding, LLM-generated generalized plan, LLM-generated completeness proof, and Lean kernel check.

Overview

LLMs have shown strong performance on generalized planning, i.e. the generation of programs that solve instances of a given PDDL planning domain. However, LLM-generated code does not guarantee universal correctness on arbitrary instances. We show for the first time how to generate generalized plans with LLMs in a way that guarantees correctness of the plans.

We achieve this by using the LLM to synthesize generalized plans as Lean programs, together with correctness proofs that are then automatically checked by Lean. We evaluate the method on 13 planning domains. It produces a Lean-checked correctness proof for 12 of them. For the remaining domain, Transport, the generated plan still has perfect test coverage.

From finite evaluation to a completeness statement

A generalized plan is intended to solve all instances of a planning domain. Evaluation on a fixed test set can establish coverage on those instances, but it does not establish completeness for the domain.

Finite evaluation

The generated program is executed on a finite collection of planning tasks. This measures coverage on the test set but leaves instances outside that set unexamined.

Completeness theorem

The theorem quantifies over every possible initial state and goal that satisfies the stated domain constraints, and states that the generalized plan computes a valid plan for this input. We generate the theorem; the LLM generates a proof; Lean checks it.

A Spanner planning task: a person walks from a shed to a gate, collecting spanners along the way to tighten nuts at the goal. — **Example: Spanner.** Move from the shed to the gate. At each intermediate location, pick up every spanner. At the gate, tighten each loose nut with a different spanner.

Method

The method has four stages: encoding the PDDL semantics in Lean, generating a generalized plan, generating its completeness proof, and checking the result with Lean’s kernel.

Lean encoding

States, goals, actions, preconditions, and effects are automatically translated into Lean by domain-independent Python code. The translation preserves the semantics of PDDL.

Generalized plan

The LLM implements a "solve" function in Lean that maps a Lean-encoded PDDL instance to a list of planning actions.

Completeness proof

The LLM constructs a Lean proof for the correctness of the "solve" function.

Lean check

Lean verifies that the proof actually establishes correctness of the generated code. If it doesn't, the LLM revises the generalized plan and the proof until Lean accepts them.

The completeness theorem

The completeness statement quantifies over all valid initial states and goals. Its conclusion has two parts: every action returned by solve is sequentially applicable, and executing the plan reaches a state satisfying the goal.

The theorem itself is generated by Python code under our control (see box to the right). We also generate Lean functions that encode the preconditions and effects of each action, as specified by the PDDL domain (see the image at the top of the page). Thus, the LLM cannot prove a different theorem instead.

The PDDL domain by itself does not fully specify what the initial state may look like. For example, in the Spanner example above, a solvable instance must have at least as many spanners as nuts. We capture the specification of permissible instances in validity constraints; the completeness theorem is then about all valid instances.

theorem solveComplete
  (s : State)
  (g : Goal)
  (hinit : ValidInit s)
  (hgoal : ValidGoal s g) :
  ValidPlan (solve s g) s ∧
  SatisfiesGoal
    (runPlan (solve s g) s) g := by
  -- LLM-generated proof,
  -- checked by Lean's kernel

Experimental results

We used GPT-5.6-Sol to generate generalized plans in Lean for 13 test domains. The proof-generation procedure completed a Lean-checked proof for 12 domains. For Transport, the generalized plan achieved full coverage on the easy and medium IPC Learning Track test splits, but the proof-generation procedure did not complete a proof.

Seven proofs were generated and debugged as a whole. For five further domains, the LLM first produced a proof sketch and then completed it one declaration at a time. Total runtime for the domains with completed proofs ranged from 9 to 54 minutes. Crucially, this time has to be invested only once for each PDDL domain. After a generalized plan has been computed, it can simply be run as a program to solve PDDL test instances in milliseconds.

Domain	Outcome	Proof mode	LLM interactions	Total time	Lean proof
Delivery	Proved	Basic	1 GP + 3 proof	13 min	Lean file
Ferry	Proved	Basic	2 GP + 3 proof	12 min	Lean file
Grippers	Proved	Basic	2 GP + 3 proof	13 min	Lean file
Heavy	Proved	Basic	1 GP + 3 proof	9 min	Lean file
Hiking	Proved	Basic	1 GP + 2 proof	12 min	Lean file
Logistics	Proved	Basic	1 GP + 3 proof	20 min	Lean file
Satellite	Proved	Basic	1 GP + 4 proof	27 min	Lean file
Blocksworld	Proved	Iterative	2 GP + 24 proof	30 min	Lean file
Goldminer	Proved	Iterative	1 GP + 36 proof	47 min	Lean file
Miconic	Proved	Iterative	1 GP + 11 proof	25 min	Lean file
Rovers	Proved	Iterative	1 GP + 45 proof	54 min	Lean file
Spanner	Proved	Iterative	1 GP + 36 proof	49 min	Lean file
Transport	Tests pass	—	1 GP	4 min GP	—

BibTeX

@misc{stein2026provablycomplete,
  title  = {Provably Complete Generalized Planning with LLMs},
  author = {Katharina Stein and Chaahat Jain and J{\"o}rg Hoffmann
            and Alexander Koller},
  year   = {2026},
  note   = {Manuscript}
}