AWS/UIUC Maestro：全局协调失败原因与证明能力提升

查看PDF HTML（实验性）

摘要：Lean越来越多地被用于验证LLM代理生成的数学证明和软件，但编写形式化证明仍然很困难。现有的证明系统采用分而治之的方法，递归地将难以证明的证明义务分解成更简单的引理，并对任何抵抗证明的引理再次进行分解。然而，一个引理可能因为不同的原因而抵抗证明，包括指导不足、错误陈述或产生它的分解中的缺陷。现有的系统无法区分这些情况，因为失败的尝试报告的只是失败本身，而且响应仅限于失败的节点，而不考虑整个证明或修改其上的计划。因此，系统可能会继续沿着有缺陷的证明方向分解义务，直到预算耗尽，导致整个证明尝试失败。我们引入了Maestro，一个Lean证明工具，它通过全局协调处理失败。证明器报告它们失败的原因，而不仅仅是它们失败了，一个看到整个证明的协调器会选择适当的响应，例如引导陷入困境的证明器、纠正错误的引理或撤回有缺陷的子树并重新规划它。相同的工具也扩展到验证代码生成，其中检查到的反例会将代码送回进行修复。我们使用四个前沿的LLM在七个数学和三个软件验证基准上评估了Maestro。它在每个基准上证明了比每个模型的本地编码代理（Claude Code或Codex）更多的目标，在每个代理尚未饱和的基准上，最大的收益在研究级数学上。与Claude Opus 5一起，它发现了arXivLean 2026年6月发布中的48个定理中的34个定理的证明，而本地代理发现了19个。它还在他们共享的每个基准上都优于所有已发表的证明系统，解决了669/672 PutnamBench、59/60 Lean-IMO-Bench和6/6 IMO 2026。

投稿历史

从：Haoyu Li [查看电子邮件]
[v1] 周一，19 Oct 2026 07:21:10 UTC (402 KB)