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

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

cs.AIOct 6, 2026

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

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

Organizations: Federal University of Rio Grande do Sul Brazil · University of Oxford United Kingdom · University of Aberdeen United Kingdom · Linköping University Sweden

Abstract

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.

Figures & tables

Panel of Figure 1 — Figure 1: Proof-guided heuristic development and reuse in LeanPlan. A deterministic generator translates the domain into a Lean module, and an agent revises a heuristic and its proof using feedback from Lean. At planning time, task checks enforce the proof assumptions.

		Blind $\mathrm{A}^{*}$		$\mathrm{A}^{*}$ with heuristics
				Scorpion	Scorpion
	Domain	Scorpion	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

Table 1: Tasks solved, with 90 per domain and separate sums for IPC 2023 and the new domains. Total combines both suites. The left columns use blind

\mathrm{A}^{*}

search and the right columns use

\mathrm{A}^{*}

search with heuristics. SCP is Scorpion’s recommended configuration, which uses saturated cost partitioning Seipp et al. (2020) . All configurations prune actions with

h^{2}

mutexes Alcázar & Torralba (2015) . Bold values and shading mark the highest coverage in each row, including ties.

Figure 3:

\mathrm{A}^{*}

search with heuristics on IPC 2023. Left: number of tasks solved within each reported per-task time threshold, with a logarithmic horizontal axis. Right: expansions of LeanPlan and SCP on the 211 tasks that both solve, with logarithmic axes. Each point represents one task, points below the diagonal favor LeanPlan and colors identify domains.

Appendix figures & tables2 assets

Supplementary material from the paper’s appendix.

Appendix

Figure 4: PDDL from the Miconic benchmark used in our experiments. The domain excerpt shows the boarding action and omits predicate declarations and other actions. The complete task asks the lift to carry passenger p1 from floor f2 to f3 .

Domain	Bound composition
Blocksworld	Maximum of unmet-clear count and required grab/place count, with held-block corrections and two actions per forced detour.
Childsnack	Unserved goal children, tray-loading shortfall, sandwich-making shortfall and necessary tray moves. Shortfalls account for gluten-free demand and existing sandwiches.
Ferry	Unmet car goals: three actions per nonaboard car or one or two per carried car, plus the maximum of repositioning and waiting-location corrections.
Floortile	Unmet painted goals, color changes and the maximum of farthest painting-position distance, half the unattended-tile count rounded up and distinct forced painting squares without a robot. Color changes cover missing colors and, with one robot, the color order forced within a column. A reachability test also detects dead ends.
Miconic	Boarding and leaving counts plus distinct required floors other than the current lift floor.
Rovers	Communication, sampling, imaging, calibration-shortfall and empty-store-shortfall counts, plus the maximum of travel and unoccupied required-waypoint counts.

Appendix

Table 2: Components of the registered domain heuristics. A maximum combines bounds that may count the same actions. Additive terms count separate necessary actions under the domain invariants.

Explore similar work

LLM-Evolved Pattern Generators for Optimal Classical Planning
Jun 1, 2026Windy Phung, Dominik Drexler, Arnaud Lequen +1Classical Planning Heuristics
Linköping University, Sweden
Successor-Generator Planning with LLM-generated Heuristics
Jan 30, 2025Alexander Tuisov, Yonatan Vernik, Alexander ShleyfmanClassical Planning Heuristics
Independent Researcher · Computer Science Department, Bar-Ilan University
A complementary study on PlanGPT: Evaluation with defined Performance Metrics and comparison with a planner
Jun 9, 2026Youssef Abdelkader, Humbert Fiorino, Damien PellierClassical Planning Performance Metric
Univ. Grenoble Alpes - LIG Grenoble, France

Jun 1, 2026, cs.AIJ/K move · Enter open · S save

LLM-Evolved Pattern Generators for Optimal Classical Planning

Windy Phung, Dominik Drexler, Arnaud Lequen, Jendrik Seipp

Linköping University, Sweden

Classical Planning Heuristics Planning

Open paper AskPDF arXiv

Learned heuristics have recently become a competitive alternative to traditional domain-independent heuristics for satisficing planning. Existing approaches, however, focus on improving search guidance rather than guaranteeing admissibility, which makes them unsuitable for optimal classical planning. We present the first method for learning domain-dependent heuristics that are admissible by design and thus preserve the optimality guarantees of A* search. Instead of learning a direct mapping from states to heuristic values, we learn to construct abstractions that induce admissible heuristics. We use an LLM-driven evolutionary program-synthesis framework to obtain, for each domain, a program that produces a pattern collection for any task in that domain, and we combine the resulting patterns admissibly via saturated cost partitioning. Empirically, the learned programs encode interpretable domain-specific insights, run with negligible overhead at test time and yield heuristics that match the coverage of state-of-the-art domain-independent baselines on several domains while evaluating each state substantially faster.

Abstract

Explore similar work

LLM-Evolved Pattern Generators for Optimal Classical Planning

Successor-Generator Planning with LLM-generated Heuristics

A complementary study on PlanGPT: Evaluation with defined Performance Metrics and comparison with a planner