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

Motivation

• Earlier LLM-generated heuristics target satisficing planning, while optimal A* requires admissibility because overestimation can produce suboptimal plans.Testing on example tasks or learning values from solved examples cannot establish admissibility across every state and task.Source: §1 · p. 1

Approach

• LeanPlan generates domain-specific heuristics together with machine-checked admissibility proofs, giving optimality guarantees for tasks that satisfy the checked assumptions.The proofs concern the code the planner runs and cover every task satisfying the assumptions, not only training tasks.Source: §1 · p. 2
• An LLM coding agent revises a heuristic, its proof, and Boolean checks of the proof’s domain assumptions using planner feedback.Lean’s kernel checks proof correctness; accepted heuristics can then serve A* on new tasks without further LLM calls or new proofs.Source: §1 · p. 2

Results

• LeanPlan solves 281 IPC 2023 tasks and 67 new-domain tasks, 27.1% and 31.4% more than Scorpion, which solves 221 and 51 tasks.The evaluation covers 900 IPC test tasks and 270 test tasks from three new domains; the hardest IPC tasks have up to 57 times as many objects as the largest training tasks.Source: §1 · p. 2

Classical Planning

• A PDDL domain specifies reusable types, predicates, and action schemas, while each task supplies objects, an initial state, and a goal that are grounded into a finite task.Grounding instantiates the domain’s predicates and actions with the task’s objects.Source: §2 · p. 2
• An optimal plan has minimum cost among plans from the state, and optimal planning seeks one from the initial state.In the experiments, unit-cost actions make minimum-cost plans also minimum-length plans.Source: §2 · p. 3

Heuristic Search

• A* expands states minimizing known path cost plus heuristic value, and an admissible heuristic ensures an optimal plan whenever one exists.Admissibility means the heuristic never exceeds the optimal remaining plan cost.Source: §2 · p. 3
• Goal-aware and consistent heuristics are admissible: goal awareness sets goal-state values to zero, while consistency limits decreases across actions to their costs.LeanPlan proves these properties on reachable states, which suffices for plans from reachable states.Source: §2 · p. 3

Lean Programs and Proofs

• Lean’s type system represents executable functions and propositions in one language, and its kernel verifies proof terms against their claimed types.This lets a theorem refer directly to the definition of a total function, including its arithmetic and case distinctions.Source: §2 · p. 3

3 LEANPLAN

• LeanPlan supports the unit-cost STRIPS fragment of PDDL and translates each domain’s action schemas into a Lean module that fixes the heuristic’s vocabulary.A deterministic generator performs the translation.Source: §3 · pp. 3–4
• A certificate comprises Boolean checks for domain assumptions and verifies that the input domain has exactly the action schemas represented in the Lean module.LeanPlan refuses to use the heuristic on a task that fails any certificate check.Source: §3 · p. 4
• Under a task’s certificate, domain proofs establish goal awareness and consistency on reachable states, from which a shared theorem derives admissibility.The shared theorem connects those local proof obligations to the heuristic’s admissibility.Source: §3 · p. 4
• An LLM coding agent develops a domain heuristic and proves its required properties, then revises the artifacts using build and planner failures as feedback.The prompt requires certificates to accept all training tasks and asks the agent to continue refining after beating a baseline.Source: §3 · p. 4
• An automated controller rebuilds and checks the candidate, rejects untrusted proof shortcuts, and accepts it only if certificates pass and training performance meets specified Scorpion comparisons.Acceptance requires at least as many training tasks solved as Scorpion and strictly fewer total expansions on tasks both solve.Source: §3 · p. 4
• Certificate checks uncovered a Floortile training-task bug: its initial state marked a tile both occupied and clear, allowing another robot to move onto it.The authors reported the issue, and it was later fixed in the benchmark repository.Source: §3 · p. 4
• Figure 2’s lift example shows a passenger-action lower bound and a theorem proving that boarding reduces it by exactly one.The example uses unfolding and omega to close the arithmetic goal.Source: Figure 2 · p. 5
• LeanPlan grounds and validates each new task before running A*; its search uses duplicate detection, reopening, and goal tests at expansion time.Search guarantees certify returned plans as valid and optimal below bound B, but do not certify dead ends or unsolvable tasks.Source: §3 · p. 5

Miconic

• In Miconic, the heuristic counts two actions per waiting passenger, one per riding passenger, and each distinct required floor; each action reduces the bound by at most one.Under the certified location and goal assumptions, the heuristic is consistent and is zero at goals.Source: §4 · p. 5

Spanner

• In Spanner, the heuristic adds loose-nut tightening, missing-spanner pickup, and worker-to-gate distance bounds, and returns threshold B when too few usable spanners remain reachable.The dead-end test compares carried plus reachable usable spanners with the number of loose goal nuts.Source: §4 · pp. 5–6

Sokoban

• For Sokoban, the heuristic takes the maximum of aggregate pushes-plus-walking and per-box movement bounds because the bounds may count the same actions.The aggregate bound sums shortest-path pushes for unmet-goal boxes and adds the robot’s initial walk to a pushing position.Source: §4 · p. 6
• LeanPlan computes Sokoban distance tables by breadth-first search and checks that they satisfy properties used by the proof, such as distances decreasing by at most one per move.The proof does not establish that the table-generating search itself is correct.Source: §4 · p. 6

5 EXPERIMENTAL RESULTS

• The evaluation uses ten IPC 2023 domains and three new domains, with 90 test tasks per domain and a 300-CPU-second, 8-GiB limit per run.The coding agent develops heuristics on training tasks and is sandboxed from test tasks; the agentic loop averages 69.8 minutes per domain and US$17.30 per domain.Source: §5 · pp. 6–7

5.1 BLIND SEARCH

• Blind LeanPlan solves nearly as many tasks as blind Scorpion, but its search takes about 1.5 times as long despite nearly identical total expansions on commonly solved IPC tasks.Blind LeanPlan solves 106 tasks within one second versus 116 for blind Scorpion, and 138 versus 139 within ten seconds.Source: §5.1 · p. 7

5.2 A∗SEARCH WITH HEURISTICS

• LeanPlan solves the most IPC 2023 tasks; beyond every training-task size, it solves 53 of 595 tasks versus 13 for SCP, 7 for LM-cut, and 0 for blind search.The evaluation includes 900 IPC 2023 test tasks and 270 tasks across three new domains; IPC hard tasks reach 57 times the largest training-task object count.Source: §5 · p. 6, §5.2 · pp. 7–8
• Within ten seconds, LeanPlan solves more tasks than SCP does within the full time limit; SCP’s curve starts after up to ten seconds of pattern-collection construction.LM-cut’s curve flattens early because heuristic evaluation is expensive; on tasks both solve, its search takes five times as long as LeanPlan’s.Source: §5.2 · p. 8, Figure 3 · p. 8
• On the 211 IPC tasks solved by both, LeanPlan expands fewer states than SCP on 152 and more on 55; generated heuristics cut expansions by over two orders of magnitude versus blind LeanPlan.The comparison is between complete planner configurations, not heuristics alone; outcomes vary by domain.Source: §5.2 · p. 8, Figure 3 · p. 8
• In the new domains, LeanPlan solves more tasks than SCP overall, especially in Qubit Routing, but solves one fewer in Cisterns after its certificate refuses three test tasks.Those are the only certificate refusals among 1,170 test tasks; SCP solves one refused task, while no configuration solves the other two.Source: §5.2 · p. 8

LLM-Guided Program Search

• LLM-guided program search can optimize performance on fixed instances, while counterexample-guided synthesis checks proposed programs against a formal specification.LeanPlan uses training-task search to measure heuristic informativeness and the Lean kernel to check admissibility.Source: §6 · p. 9

Learned Heuristics and Admissibility

• Learned heuristics often lack guarantees on unseen states, while established domain-independent heuristics are admissible by construction; Phung et al. (2026) use LLMs to generate pattern generators.Statistical generalization bounds do not guarantee admissibility on unseen states.Source: §6 · p. 9

Verification and Certificates in Planning

• Planning verification ranges from validating plans and proving optimality to domain-level heuristic proofs; LeanPlan proves admissibility once per domain rather than certifying each task.Its certificate is a fixed set of Boolean checks that establishes the premise of domain theorems for each task.Source: §6 · p. 9

Theorem Proving and Verified Code Generation

• LLMs can construct and repair formal proofs, but LeanPlan must make its heuristic informative as well as correct; the always-zero heuristic is admissible but uninformative.The paper measures informativeness through search on training tasks.Source: §6 · p. 9

7 CONCLUSIONS

• For all considered domains, LLM agents produced domain-specific heuristics and machine-checked admissibility proofs; LeanPlan usually expands fewer states than Scorpion and solves more tasks overall.The authors report that the proved heuristics exploit domain structure.Source: §7 · p. 9
• LeanPlan supports only unit-cost STRIPS PDDL, and the evaluation covers thirteen domains with one LLM and coding-agent harness.The proofs guarantee admissibility only on tasks satisfying checked domain assumptions, which can exclude test tasks.Source: §7 · p. 9
• The guarantees also rely on unchecked components, including Lean’s kernel, compiler and runtime, the PDDL parser, and the formalized PDDL semantics.Extending the approach to action costs and richer PDDL fragments, and evaluating other LLMs, remain open directions.Source: §7 · p. 10

AI USE STATEMENT

• LLM coding agents developed the heuristic programs and Lean proofs; AI assistants supported literature checks, manuscript revision, and analysis and figure preparation.Source: AI USE STATEMENT · p. 10

• The evaluation uses public planning benchmarks and three new benchmark domains, with no human subjects or personal data.Source: ETHICS STATEMENT · p. 10
• LeanPlan’s guarantees concern the PDDL model; an inaccurate model can still produce plans unsafe or suboptimal for the real system.Source: ETHICS STATEMENT · p. 10
• Developing each heuristic and proof requires LLM computation, but accepted heuristics are reused on new tasks without further LLM calls.Source: ETHICS STATEMENT · p. 10

• Figure 4 shows a PDDL excerpt from the Miconic benchmark alongside a complete task.Source: A PDDL INPUT EXAMPLE · p. 15, Figure 4 · p. 15
• The excerpt shows the boarding action, which puts a passenger aboard when the lift is at that passenger’s origin floor.Source: A PDDL INPUT EXAMPLE · p. 15
• The complete task asks the lift to carry passenger p1 from floor f2 to f3.Source: Figure 4 · p. 15

B PROOF INTERFACE AND SEARCH CONDITIONS

• The ImprovedProof contract has goal-awareness and consistency fields; a Boolean check supplies the theorem premise, while the runtime evaluator is the function whose properties are proved.Source: B PROOF INTERFACE AND SEARCH CONDITIONS · p. 15
• Grounding proofs transfer packed-state plans to grounded operators while preserving goal satisfaction and cost, so the search guarantees concern the executable grounded task.Source: B PROOF INTERFACE AND SEARCH CONDITIONS · p. 16
• A returned plan is proved executable and goal-reaching, and optimality is relative to valid plans costing less than B = 240; fuel exhaustion is reported as failure, not unsolvability.Search does not certify that pruned states are dead ends, and the theorems apply when the explicit fuel suffices to return a plan.Source: B PROOF INTERFACE AND SEARCH CONDITIONS · p. 16

C NEW DOMAINS

• Orrery routes wheel-position changes through couplings, Cisterns redistributes water through hoses, and Qubit Routing swaps qubits on a grid to execute gates in order.Source: C NEW DOMAINS · p. 16

D DOMAIN HEURISTIC DETAILS

• Table 2 distinguishes maxima, which may combine bounds counting the same actions, from additive terms, which count separate necessary actions under domain invariants.Source: D DOMAIN HEURISTIC DETAILS · p. 16, Table 2 · p. 17
• Miconic’s heuristic counts waiting passengers twice, riding passengers once, and needed floors other than the lift’s current floor, deduplicating shared floors.Source: D DOMAIN HEURISTIC DETAILS · p. 18
• For Cisterns, the heuristic takes the maximum of two lower-bound families: selected demand sets and integer potentials constrained across tanks sharing a hose.Compilation greedily selects 28 demand sets and generates 17 candidate potentials; certificates check the resulting sets and potentials against every ground action.Source: D DOMAIN HEURISTIC DETAILS · p. 20
• Qubit Routing adds the remaining gate-execution count to a swap bound formed from the largest gate deficit and matching-based bounds.Source: D DOMAIN HEURISTIC DETAILS · p. 20

• Certificate conditions supplement ordinary validation and exact action-schema matching by checking type declarations, initial-state premises, static predicates, and dynamic goals.Source: §D.1 · p. 20
• Childsnack and Ferry impose task-specific goal and initial-state constraints that support their resource-count and capacity-one invariants.Source: §D.1 · p. 21
• Floortile, Miconic, and Rovers certificates constrain types, goals, static predicates, or initial relations; Floortile additionally imposes a compiled-task bound relative to B.Source: §D.1 · p. 21
• Satellite and Qubit Routing certificates check task-specific goal forms and preserved relations, including single-valued initial assignments and mutual exclusion of active gates or qubit positions.Source: §D.1 · pp. 21–22
• Sokoban and Blocksworld certificates require well-formed initial configurations, including unambiguous occupancy and, for Blocksworld, terminating support chains.Source: §D.1 · pp. 20–22
• Distance-table checks verify bounded entries and edge consistency; a failed check selects zero tables during compilation rather than rejecting the task.Source: §D.1 · p. 22

E EXPERIMENT RECORDS

• 8,550 configuration–task runs are recorded; 5,850 belong to the five reported configurations, with separate IPC and new-domain snapshots.The snapshots contain 7,200 IPC runs and 1,350 new-domain runs.Source: E EXPERIMENT RECORDS · p. 22
• All 1,157 solved runs of the reported configurations have completed-run expansion measurements, and checkpoint counts are excluded from expansion comparisons.Each reported configuration has a run for each of the 90 test tasks per domain.Source: E EXPERIMENT RECORDS · p. 23
• The IPC 2023 comparison suites use task intersections: 198 for three heuristic configurations, 211 for LeanPlan–Scorpion, and 154 for blind configurations.Figure 3 uses this suite only; runtime curves include solved runs and end at full-budget coverage.Source: E EXPERIMENT RECORDS · p. 23
• LeanPlan total time includes validation, grounding, h2 pruning, heuristic setup, and search; search time begins after grounding and h2 pruning.Expansion counts exclude stale queue entries and the popped goal, and planners use their own expansion definitions.Source: E EXPERIMENT RECORDS · p. 23

F AGENT PROMPT

• The agent must refine a domain-specific heuristic beyond merely beating Scorpion, while leaving a working proof and passing certificates.The prompt asks it to continue refinement until it cannot improve the candidate further.Source: F AGENT PROMPT · pp. 23, 25
• The proof must establish goal-awareness and consistency for the compiled heuristic on certificate-admitted states, and the certificate must accept every training task.The prompt states that goal-awareness and consistency give admissibility, which gives optimality.Source: F AGENT PROMPT · pp. 23–24