LeanPlan：利用 LLM 生成的启发式函数与可采纳性证明进行最优规划

arXiv:2610.08246v1 公告类型：交叉收录 摘要：前沿大语言模型（LLM）能够生成启发式函数来引导搜索，在接受任意可行计划的满意规划中达到最先进的性能。然而，这些启发式函数并不保证具有可采纳性，可能导致次优计划。我们提出 LeanPlan，这是首个利用 LLM 生成且可采纳性经过机器检查的启发式函数来寻找最优计划的规划系统。给定领域描述和训练任务，智能体循环利用规划器的反馈，迭代改进可复用的领域专用启发式函数、其可采纳性证明以及所需的领域假设。LeanPlan 在 Lean 4 中实现了启发式函数、相应证明和高效规划器，其中实例化与搜索均经过机器检查。我们在 International Planning Competition 的十个领域及三个新领域上评估 LeanPlan，测试任务的对象数量最高达到训练任务的 57 倍。在智能体循环中使用 GPT-5.6 Sol 时，我们成功为所有这些领域生成了启发式函数及可采纳性证明。借助生成的启发式函数，LeanPlan 扩展的状态数通常少于最先进的 Scorpion 规划器，并且总体上解决了更多任务。