Maestro: Agentic Formal Proof Development by Coordination
作者: Haoyu Li, Zeren Shui, Yuhao Zhang, Ferhat Erata, Benjamin Mikek, Murali Krishna Ramanathan, Hao Zhou
分类: cs.LG
发布日期: 2026-10-19
💡 一句话要点
提出Maestro以解决形式证明开发中的失败协调问题
🎯 匹配领域: 支柱五：交互与反应 (Interaction & Reaction)
关键词: 形式证明 全局协调 数学验证 软件验证 大型语言模型
📋 核心要点
- 现有的形式证明系统在处理复杂证明时，无法有效区分失败原因，导致无效的分解和重复尝试。
- Maestro通过全局协调机制，允许证明者报告失败原因，并由协调者选择适当的响应策略，从而优化证明过程。
- 在实验中，Maestro在多个基准测试中超越了现有的证明系统，尤其在研究级数学问题上表现出色。
📝 摘要（中文）
Lean越来越多地用于验证由大型语言模型（LLM）代理生成的数学证明和软件，但编写形式证明仍然困难。现有的证明系统采用分而治之的方法，将复杂的证明义务递归分解为更简单的引理。然而，现有系统无法区分失败的原因，导致可能在错误的证明方向上不断分解，直到预算耗尽。本文提出了Maestro，一个通过全局协调处理失败的Lean证明工具，允许证明者报告失败原因，协调者则根据整体证明选择适当的响应。通过对四个前沿LLM在七个数学和三个软件验证基准上的评估，Maestro在每个未饱和的基准上都证明了比每个模型的本地编码代理更多的目标，尤其在研究级数学上取得了显著进展。
🔬 方法详解
问题定义：本文要解决的问题是现有形式证明系统在面对复杂证明时，无法有效识别失败原因，导致无效的分解和重复尝试，最终影响证明的成功率。
核心思路：Maestro的核心思路是通过全局协调机制，使得证明者不仅报告失败，还能提供失败原因，协调者根据整体证明情况选择相应的响应策略，从而优化证明过程。
技术框架：Maestro的整体架构包括多个模块：证明者模块、协调者模块和反馈机制。证明者模块负责执行证明，协调者模块负责整合信息并制定响应策略，反馈机制则用于修正错误和重新规划。
关键创新：Maestro的主要创新在于其全局协调机制，能够识别并处理不同类型的失败，区别于现有方法仅能报告失败的局限性。
关键设计：在设计上，Maestro允许证明者提供失败原因，协调者根据这些信息选择指导、修正或重新规划的策略，确保整个证明过程的高效性和准确性。具体的参数设置和网络结构细节在论文中进行了详细描述。
🖼️ 关键图片
📊 实验亮点
在实验中，Maestro在七个数学和三个软件验证基准上表现优异，成功证明了669个PutnamBench中的672个目标，59个Lean-IMO-Bench中的60个目标，以及6个IMO 2026中的全部目标，显示出其在形式证明领域的强大能力。
🎯 应用场景
Maestro的研究成果在形式证明和软件验证领域具有广泛的应用潜力，能够提高数学证明的自动化程度和软件的可靠性。未来，Maestro可能在教育、科研和工业界的形式验证任务中发挥重要作用，推动相关领域的发展。
📄 摘要（原文）
Lean is increasingly used to verify mathematical proofs and software produced by LLM agents, but writing formal proofs remains hard. Existing prover systems take a divide-and-conquer approach that recursively decomposes hard proof obligations into easier lemmas and splits again any lemma that resists proof. However, a lemma can resist proof for different reasons, including insufficient guidance, a false statement, or a flaw in the decomposition that produced it. Existing systems cannot tell these apart as a failed attempt reports little beyond its failure, and responses are confined to the failing node without considering the rest of the proof or revising the plan above it. The system may thus keep decomposing obligations along a flawed proof direction until the budget runs out, causing the whole proof attempt to fail. We introduce Maestro, a Lean prover harness that handles failures through global coordination. Provers report why they failed, not just that they failed, and a coordinator that sees the whole proof chooses an appropriate response, such as guiding a stuck prover, correcting a false lemma, or retracting a flawed subtree and replanning it. The same harness extends to verified code synthesis, where a checked counterexample sends the code back for repair. We evaluate Maestro with four frontier LLMs on seven mathematics and three software verification benchmarks. It proves more targets than each model's native coding agent (Claude Code or Codex) on every benchmark the agent has not already saturated, with the largest gains on research-level mathematics. With Claude Opus 5, it discovers its own proofs of 34 of the 48 theorems in the June 2026 release of arXivLean, against 19 for the native agent. It also outperforms all published prover systems on every benchmark they share, solving 669/672 PutnamBench, 59/60 Lean-IMO-Bench, and 6/6 IMO 2026.