LeanPlan：带可采纳性证明的 LLM 规划启发式

Frontier 大语言模型 (LLM) 可以生成启发式函数，指导搜索在令人满意的规划中实现最先进的性能，其中任何计划都是可以接受的。然而，这些启发法并不能保证是可接受的，并且可能导致计划不理想。我们推出 LeanPlan，这是第一个利用 LLM 生成的启发式算法找到最佳计划的规划系统，其可接受性经过机器检查。给定域描述和训练任务，Agentic 循环使用规划器反馈来迭代改进可重用的特定于域的启发式方法、其可接受性证明和所需的域假设。 LeanPlan 在 Lean 4 中通过机器检查的基础和搜索来实现启发式、其证明和高效规划器。我们在国际规划竞赛的 10 个领域和 3 个新领域上评估 LeanPlan，使用的测试任务的对象数量高达训练任务的 57 倍。通过 Agentic 循环中的 GPT-5.6 Sol，我们成功地为所有这些领域生成启发式和可接受性证明。通过由此产生的启发式方法，LeanPlan 通常比最先进的 Scorpion 规划器扩展更少的状态，并总体上解决更多任务。