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
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
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 A∗
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 A∗ search and the right columns use A∗ search with heuristics. SCP is Scorpion’s recommended configuration, which uses saturated cost partitioning Seipp et al. (2020) . All configurations prune actions with h2 mutexes Alcázar & Torralba (2015) . Bold values and shading mark the highest coverage in each row, including ties.
Figure 3: 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.
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.
Heuristics are a central component of deterministic planning, particularly in domain-independent settings where general applicability is prioritized over task-specific tuning. This work revisits that paradigm in light of recent advances in large language models (LLMs), which enable the automatic synthesis of heuristics directly from problem definitions -- bypassing the need for handcrafted domain knowledge. We present a method that employs LLMs to generate problem-specific heuristic functions from planning tasks specified through successor generators, goal tests, and initial states written in a general-purpose programming language. These heuristics are compiled and integrated into standard heuristic search algorithms, such as greedy best-first search. Our approach achieves competitive, and in many cases state-of-the-art, performance across a broad range of established planning benchmarks. Moreover, it enables the solution of problems that are difficult to express in traditional formalisms, including those with complex numeric constraints or custom transition dynamics. We provide an extensive empirical evaluation that characterizes the strengths and limitations of the approach across diverse planning settings, demonstrating its effectiveness.
Alexander Tuisov, Yonatan Vernik, Alexander Shleyfman
Independent Researcher · Computer Science Department, Bar-Ilan University
Automated Planning is a subfield of Artificial Intelligence (AI) where the main objective is generating a sequence of actions, known as a plan, that helps us reach a goal state from an initial state. A planning problem is defined by a set of objects, an initial state and a desired goal state. The objective is to compute a plan that'll lead us from the inital state to the goal state. Programs that generate plans are called planners. In this paper, we did a complementary study to the state-of-the-art LLM called PlanGPT which was released last year. We redid some experiments to verify whether planning with LLMs is \textbf{pertinent} and \textbf{worthwhile}. We also check whether the results obtained in the official PlanGPT paper for plan coverage were correct, and we also performed a more comprehensive study on PlanGPT's performance: in our paper PlanGPT's performance was evaluated using two metrics: Plan Cost and Plan Generation Time. The results of planGPT were compared to those produced by a traditional planner for the same plans and same metrics. We discovered that PlanGPT is no better than a Greedy search strategy.