Optimal planning system uses large language models with machine-checked proofs
LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs
Artificial IntelligenceMachine LearningSymbolic Computation
Summary
Planning systems help computers find the best ways to reach goals, but they usually guess shortcuts that might not always be the best. This paper describes LeanPlan, a system that uses large language models (LLMs) to create guiding functions and proves mathematically that these shortcuts won’t miss the best plan. The system improves these guides through feedback and checking to ensure it always finds the best solutions. It was tested on multiple planning challenges and often worked better than previous top planners.
What this means in practice
- •For robotics developers: Create robots that find the best sequences of actions efficiently by using proven heuristics generated with large language models.
- •For logistics planners: Improve automated route and resource planning by integrating verifiable heuristics for guaranteed optimal solutions in complex domains.
Authors
André G. Pereira, Augusto B. Corrêa, Felipe Meneguzzi, Jendrik Seipp
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.