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

> LeanPlan is the first system to machine-check LLM-generated heuristics for admissibility via Lean 4, solving 281 IPC 2023 tasks—27.1% more than the state-of-the-art optimal planner Scorpion.

- **Source:** [arXiv](https://arxiv.org/abs/2610.08246)
- **Published:** 2026-10-10
- **Permalink:** https://picx.dev/p/PQFRYg
- **Whiteboard:** https://picx.dev/p/PQFRYg/image

## Summary

## 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)

```lean
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

| Domain | Strategy |
|--------|----------|
| **Miconic** | Action counting: $h(s) = 2|W(s)| + |R(s)| + |F(s)|$ where $W$ = waiting passengers, $R$ = riding passengers, $F$ = distinct required floors |
| **Spanner** | Action counting + dead-end detection: $h(s) = L(s) + \max(0, L(s) - C(s)) + D(s)$ where $L$ = loose nuts, $C$ = carried spanners, $D$ = distance to gate |
| **Sokoban** | Maximum of two distance-based bounds: $$h(s) = \max\left\{\sum_{b \text{ with unmet goal}} P_b(s) + A(s), \quad \max_{b \text{ with unmet goal}} J_b(s)\right\}$$ |

## 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

| Domain | Blind Scorpion | Blind LeanPlan | LM-cut | SCP | LeanPlan |
|--------|---------------|----------------|--------|-----|----------|
| **IPC 2023** | | | | | |
| Blocksworld | 6 | 6 | 11 | 11 | **20** |
| Childsnack | 9 | 9 | 9 | 9 | **16** |
| Ferry | 10 | 10 | 18 | 19 | **29** |
| Floortile | 10 | 10 | 20 | 20 | 20 |
| Miconic | 30 | 30 | 36 | **40** | 37 |
| Rovers | 15 | 12 | 16 | 17 | **18** |
| Satellite | 12 | 12 | 20 | **27** | 25 |
| Sokoban | 27 | 27 | 29 | **31** | 30 |
| Spanner | 30 | 30 | 30 | 30 | **72** |
| Transport | 8 | 8 | 9 | **17** | 14 |
| **Sum** | 157 | 154 | 198 | 221 | **281** |
| **New** | | | | | |
| Orrery | 0 | 0 | 1 | 18 | **20** |
| Cisterns | 9 | 8 | 10 | **26** | 25 |
| Qubit Routing | 0 | 0 | 0 | 7 | **22** |
| **Sum** | 9 | 8 | 11 | 51 | **67** |
| **Total** | 166 | 162 | 209 | 272 | **348** |

### 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

---

_Markdown view of https://picx.dev/p/PQFRYg, served by PicX — AI-generated visual whiteboard summaries of research papers._