arXiv cs.AI· Andr\'{e} G. Pereira, Augusto B. Corr\^ea, Felipe Meneguzzi, Jendrik Seipp·· 10 天前AI 评分27
LeanPlan：用 LLM 生成启发式并机器验证可采纳性证明的最优规划
LeanPlan: Optimal Planning with LLM-Generated Heuristics and Admissibility Proofs
AI 导读
LeanPlan 是首个用 LLM 生成启发式、并通过机器验证其可采纳性来求解最优规划的系统，在 Lean 4 中实现启发式、证明及带机器验证 grounding 与搜索的高效规划器。
正文 · AI 翻译
摘要：前沿大语言模型（LLM）能够生成启发式函数，引导搜索在满足性规划中达到最先进的性能，其中任何规划都是可接受的。然而，这些启发式函数不保证是可采纳的，可能导致次优规划。我们提出 LeanPlan，这是首个使用 LLM 生成的启发式函数寻找最优规划、且其可采纳性经过机器检验的规划系统。给定领域描述和训练任务，一个智能体循环利用规划器反馈来迭代改进可复用的领域特定启发式函数、其可采纳性证明以及所需的领域假设。LeanPlan 在 Lean 4 中实现了该启发式函数、其证明以及一个具有机器检验的接地和搜索的高效规划器。我们在国际规划竞赛的十个领域和三个新领域上评估 LeanPlan，使用的测试任务最多包含训练任务 57 倍之多的对象。在智能体循环中使用 GPT-5.6 Sol，我们成功为所有这些领域生成了启发式函数和可采纳性证明。使用所得的启发式函数，LeanPlan 通常比最先进的 Scorpion 规划器扩展更少的状态，并且总体上解决更多任务。
| 主题： | 人工智能（cs.AI）；机器学习（cs.LG）；符号计算（cs.SC） |
| 引用为： | arXiv:2610.08246 [cs.AI] |
| （或 arXiv:2610.08246v1 [cs.AI] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.08246 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Augusto B. Corrêa [查看电子邮件]
[v1]
2026年10月6日星期二 12:27:34 UTC（75 KB）
来源：arXiv cs.AI · arxiv.org