Summary

• LeanPlan is the first planning system that finds optimal plans using LLM-generated heuristics whose admissibility is machine-checked via the Lean 4 proof assistant.
• It uses an agentic loop where an LLM coding agent iteratively generates a domain-specific heuristic, its admissibility proof, and domain assumptions, with feedback from the Lean compiler and planner execution.
• LeanPlan solves 281 IPC 2023 tasks and 67 new-domain tasks, 27.1% and 31.4% more than the state-of-the-art optimal planner Scorpion (221 and 51 tasks respectively).
• The system successfully generated verified heuristics for all 13 domains (10 IPC 2023 domains + 3 new domains), with test tasks containing up to 57 times more objects than training tasks.
• The generated heuristics remain effective far outside the training distribution, solving 53 tasks beyond training sizes compared to 13 for Scorpion SCP.

Introduction and Theoretical Foundation

Classical planning involves finding action sequences transforming an initial state to a goal state. Heuristic search is a dominant approach, where a heuristic function estimates remaining cost to goal. Domain-specific heuristics can be far more informative than domain-independent ones but traditionally require human expert design.

Large language models (LLMs) can now automate heuristic design for satisficing planning (any valid plan), but their heuristics lack admissibility guarantees needed for optimal planning. A heuristic is admissible if it never overestimates the true remaining cost $h^*(s)$. This guarantee must hold for every state of every task in the domain, including tasks far larger than training examples—something testing or statistical bounds cannot establish.

The theoretical foundation builds on two local properties that together imply admissibility:

• Goal-aware: $h(s) = 0$ for every goal state $s$
• Consistent: $h(s) \leq c(a) + h(s')$ for every transition $s \xrightarrow{a} s'$

Along any plan, these properties ensure the heuristic value at the start is at most the plan's cost. LeanPlan proves these properties for all reachable states, which suffices since every state on a plan from a reachable state is itself reachable.

Methodology

Architecture

LeanPlan's pipeline (Figure 1) involves:

1. Domain Translation: A deterministic generator translates PDDL action schemas into a Lean module, fixing the vocabulary for heuristics and proofs.

2. Agentic Development Loop: An LLM coding agent (GPT-5.6 Sol) receives:

   • The generated Lean module
   • Training tasks
   • Heuristic interface and shared proof library
   • Baseline Scorpion results for comparison

3. Proof Obligations: For domain $d$, task $p$, ground task $T$, and heuristic $h$, the domain theorems prove for all reachable states $s \in R$:

$$h(s) = 0 \quad \text{for every goal state } s \in R \tag{1}$$ $$h(s) \leq c(a) + h(s') \quad \text{for every transition } s \xrightarrow{a} s' \text{ with } s \in R \tag{2}$$

4. Certificate System: Boolean checks on task objects, initial state, and goal that the proof relies on. The certificate must accept all training tasks and is evaluated before search.

5. Automated Verification: A controller rejects candidates using prohibited constructs (sorry, admit, native_decide), rebuilds everything, and requires the heuristic to solve at least as many training tasks as Scorpion while expanding strictly fewer states on shared tasks.

Example Heuristic (Miconic)

def passengerBound (w r : Nat) : Nat := 2 * w + r
theorem boarding_step (w r : Nat) :
    passengerBound (w + 1) r =
    1 + passengerBound w (r + 1) := by
  unfold passengerBound
  omega

Generated Heuristic Strategies

Empirical Validation / Results

Experimental Setup

• 10 IPC 2023 Learning Track domains (900 test tasks) + 3 new domains (270 test tasks)
• Test tasks with 2.5 to 57 times more objects than training tasks
• 300 CPU seconds and 8 GiB memory limit per task
• Agentic loop: 69.8 minutes average per domain, ~33.7M input tokens (98.6% cached)

Coverage Results

Key Findings

• Blind search comparison: LeanPlan's proof-checked grounding/search costs little coverage vs. Scorpion, with ~1.5× slower state expansion but nearly identical expansions.
• Spanner dominance: LeanPlan solves 72/90 tasks (vs. 30 for SCP), attributed to the dead-end detection in its heuristic.
• Generalization: On 595 IPC 2023 tasks with more objects than training, LeanPlan solves 53 vs. 13 for SCP.
• Expansion efficiency: On 211 tasks both solve, LeanPlan expands fewer states on 152 tasks (vs. 55 for SCP).
• Scaling: LeanPlan solves more tasks within 10 seconds than SCP does within the full 300-second limit.

Theoretical and Practical Implications

Theoretical Contributions

1. Machine-checked optimality: The approach proves admissibility for all tasks satisfying certificate assumptions, not just training tasks—addressing a fundamental limitation of statistical generalization bounds.

2. Proof-guided heuristic development: Demonstrates that requiring formal proofs does not force weak heuristics; the proved heuristics exploit rich domain structure.

3. Separation of concerns: The certificate system explicitly identifies domain assumptions that PDDL doesn't enforce, making implicit assumptions explicit and checkable.

Practical Implications

• Cost efficiency: Average US$17.30 per domain for heuristic generation (one-time cost), reusable across unlimited tasks.
• Verification infrastructure: The Lean kernel serves as a small, trusted proof checker, independent of the LLM's self-reported success.
• Limitations: Only unit-cost STRIPS fragment supported; certificates can reject valid test tasks (as in Cisterns); no unsolvability certification; trust in Lean's kernel, compiler, and PDDL parser remains.

Conclusion

LeanPlan demonstrates that LLM-generated heuristics can achieve state-of-the-art optimal planning performance with machine-checked admissibility guarantees. The system successfully generated verified heuristics for all 13 domains, outperforming the state-of-the-art Scorpion planner on most domains while providing formal optimality guarantees that Scorpion lacks.

Future directions include:

• Extending to action costs and richer PDDL fragments
• Evaluating other LLMs, including open-weight models
• Addressing certificate refusals through more varied training sets
• Potentially certifying unsolvability and dead-end detection