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

📄 arXiv: 2610.08246v1 📥 PDF

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

分类: cs.AI, cs.LG, cs.SC

发布日期: 2026-10-06

💡 一句话要点

提出LeanPlan以解决LLM生成启发式函数的最优规划问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 最优规划 启发式函数 机器检查 大型语言模型 自动规划 机器人路径规划 复杂系统优化

📋 核心要点

  1. 现有方法生成的启发式函数可能导致次优计划，缺乏可接受性保证。
  2. LeanPlan通过机器检查LLM生成的启发式函数的可接受性，确保生成的计划是最优的。
  3. 在多个领域的实验中，LeanPlan的状态扩展数量通常少于现有的Scorpion规划器，解决的任务数量更多。

📝 摘要（中文）

前沿的大型语言模型（LLMs）能够生成启发式函数，指导搜索以实现满意规划的最佳性能。然而，这些启发式函数并不保证是可接受的，可能导致次优计划。本文介绍了LeanPlan，这是第一个能够找到最优计划的规划系统，利用机器检查的LLM生成启发式函数的可接受性。LeanPlan通过一个代理循环，使用规划者反馈迭代改进可重用的领域特定启发式函数及其可接受性证明。LeanPlan在Lean 4中实现了启发式函数、其证明以及高效的规划器，经过评估，在国际规划竞赛的十个领域和三个新领域中表现出色，成功生成了启发式函数和可接受性证明。

🔬 方法详解

问题定义：本文解决的问题是如何利用大型语言模型生成的启发式函数来实现最优规划，同时确保这些启发式函数的可接受性。现有方法的痛点在于生成的启发式函数可能导致次优解，缺乏有效的可接受性验证。

核心思路：LeanPlan的核心思路是通过一个代理循环，结合规划者的反馈，迭代改进领域特定的启发式函数及其可接受性证明。这种设计确保了生成的启发式函数不仅高效且具备理论上的可接受性。

技术框架：LeanPlan的整体架构包括三个主要模块：LLM生成启发式函数、机器检查可接受性证明的模块，以及高效的规划器。代理循环在这些模块之间进行交互，以优化启发式函数。

关键创新：LeanPlan的最大创新在于首次实现了机器检查的LLM生成启发式函数的可接受性，确保了生成计划的最优性。这与现有方法的本质区别在于，后者通常缺乏对启发式函数可接受性的验证。

关键设计：LeanPlan在设计上采用了高效的搜索算法，并在Lean 4中实现了启发式函数和其证明的机器检查。关键参数设置和损失函数的选择经过精心调整，以确保启发式函数的有效性和可接受性。

🖼️ 关键图片

img_0
img_1
img_2

📊 实验亮点

在实验中，LeanPlan在国际规划竞赛的十个领域和三个新领域中表现出色，成功生成了启发式函数和可接受性证明。与现有的Scorpion规划器相比，LeanPlan通常扩展的状态数量更少，解决的任务数量更多，显示出显著的性能提升。

🎯 应用场景

LeanPlan的研究成果在自动规划、机器人路径规划和复杂系统优化等领域具有广泛的应用潜力。通过确保生成的计划是最优的，LeanPlan可以在实际应用中提高效率，降低资源消耗，推动智能系统的进一步发展。

📄 摘要（原文）

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.