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

Excerpt

arXiv:2610.08246v1 Announce Type: cross 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