LeanPlan：用 LLM 生成启发式并机器验证可采纳性的最优规划系统

LeanPlan 是首个用 LLM 生成启发式函数并对其可采纳性做机器验证的规划系统，从而找到最优规划。它通过智能体循环借助规划器反馈迭代改进可复用的领域特定启发式及其可采纳性证明。此前 LLM 生成的启发式虽在满足性规划中达到 SOTA，但不保证可采纳，可能产生次优规划。