发表机构
University of Oxford; University of Aberdeen; Linköping University（牛津大学; 阿伯丁大学; 林雪平大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
LeanPlan利用LLM生成经机器验证可容许性的启发式函数，实现最优规划，在多个规划领域优于Scorpion规划器。
AI 中文摘要
前沿大型语言模型（LLM）能够生成启发式函数，引导搜索在满足性规划（即任何计划均可接受）中实现最先进的性能。然而，这些启发式函数不保证具有可容许性，可能导致次优计划。我们提出LeanPlan，这是首个利用LLM生成的启发式函数来寻找最优计划，并通过机器验证其可容许性的规划系统。给定领域描述和训练任务，一个智能体循环利用规划器反馈，迭代改进一个可复用的领域特定启发式函数、其可容许性证明以及所需的领域假设。LeanPlan在Lean 4中实现了该启发式函数、其证明以及具有机器验证的基化和搜索的高效规划器。我们在国际规划竞赛的十个领域和三个新领域上评估LeanPlan，使用测试任务中的对象数量高达训练任务的57倍。在智能体循环中使用GPT-5.6 Sol，我们成功地为所有这些领域生成了启发式函数和可容许性证明。利用生成的启发式函数，LeanPlan通常比最先进的Scorpion规划器扩展更少的状态，并总体上解决更多任务。
英文摘要
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.
