Maestro系统为Lean证明引入全局调度，研究级定理求解率提升63%

当AI证明系统卡在某个引理无法推进时，传统做法几乎总是重复同一套动作：将目标进一步拆解为更小的子任务，再尝试证明——即便这些子任务本身可能基于错误假设或伪命题。这种“越拆越深、越深越死”的困境，长期制约着形式化证明在高等数学领域的实用化。近期，由伊利诺伊大学厄巴纳-香槟分校（UIUC）与AWS AI Labs等机构联合提出的Maestro系统，首次将“全局调度”理念引入Lean证明流程，从根本上改变了失败响应逻辑，使研究级定理的自动求解成功率提升63%。

Maestro的核心创新在于打破“局部试错—无限拆解”的闭环，代之以一个持续在线、可访问完整证明蓝图的持久化协调者（Persistent Coordinator）。该协调者不直接参与证明计算，而是作为整个系统的“总指挥”，依据来自多个并行Worker的结构化反馈，动态调整证明策略：重试、补引理、修正命题，甚至整体撤换路线。这一设计源于对现有系统盲区的清醒认知——引理失败的原因千差万别：可能是缺关键辅助信息；可能是引理本身为假；也可能是上层分解路径根本错误。而传统系统既无法区分这三类情况，也无法跳出当前节点进行回溯干预。

• Provers（证明者）：并行攻击开放义务，但关键改进在于——失败时必须提交诊断报告，说明尝试路径、失败归因（局部缺失？全局错误？），若怀疑命题为假，还需提供经Lean验证的反例；
• Lemma planner（引理规划器）：将自然语言证明计划转化为Lean代码，并主动识别“多计划反复卡在同一硬核义务”的现象，向协调者预警潜在病灶；
• Explorers（探索者）：仅在诊断库无解时启用，不受既有计划约束，自主寻找替代路径；协调者甚至会“裸派”探索者（不给任何提示），避免自身偏见窄化搜索空间；
• Implementer（实现者）：专司验证码任务，负责编写代码并接受严格检验——不仅需通过编译，还需满足算法正确性与复杂度要求。

协调者掌握两项关键能力：其一是全局蓝图改写权。不同于传统系统仅能“加法式”补充引理，Maestro协调者可在单次编辑中同步执行删除伪命题、合并共享引理、替换父猜想等操作。论文中一个典型案例显示，一次修订直接废弃22条已证引理（其中19条已完成证明），这种“敢于推倒重来”的决策能力是旧有架构无法实现的。

其二是异步事件驱动的终止判断。传统流水线依赖固定轮次与超时机制，易造成“快者等待慢者”或“近成功者被截断”。Maestro让Worker在宽预算下异步运行，是否终止某次尝试，由协调者根据实时证据动态裁决：有效但缓慢的继续推进，钻牛角尖的及时叫停。

实证结果印证了该架构的有效性。在FATE-X基准集上，Maestro在Fable 5与GPT-5.6 Sol两个子集中分别解决91+6题与84+6题（括号内为Refuted数），显著优于纯Agent（77/70题）与朴素分解方案（76/72题）。在更具挑战性的PutnamBench（672题）中，Maestro解出669题；IMO 2026全部六道题均被完整证明。值得注意的是，其“证伪”能力同样严谨：系统对“命题为假”的主张采取零信任策略，要求所有反例必须在冻结上下文中通过Lean编译验证，确保结论可靠。

这一进展的意义不仅在于性能提升，更在于为形式化证明提供了可审计、可解释的工程范式。整个证明过程以事件流形式记录，每一步决策均有据可查；协调者的调度逻辑本身也可作为元推理研究对象。开源承诺（论文声明代码将公开）进一步推动社区共建——尽管目前HTML版尚未提供直接仓库链接，但技术细节已充分披露。

从更广视角看，Maestro代表了AI for Formal Methods领域的重要转向：从“ brute-force 拆解”走向“诊断-决策-重构”的认知闭环1。它呼应了近期关于“验证成本远低于生成成本”的行业共识——正如庚辛资本指出，“生成是指数，验证是线性”，高效验证机制将成为AI4S（AI for Science）落地的关键杠杆。而在评判环节，类似卡内基梅隆大学提出的“自信时接受，不确定时升级”分层裁判思路，也正与Maestro的“诊断驱动调度”形成方法论共振：二者都强调，智能系统必须具备对自身能力边界的感知与响应能力，而非盲目执行预设流程。

Maestro尚未宣称要替代人类数学家，但它确实让机器在面对复杂证明时，第一次展现出接近人类研究员的“战略调整”能力：知道何时坚持、何时放弃、何时另辟蹊径。对于形式化验证、程序正确性保障乃至未来AI自主科研系统而言，这种“会思考失败”的架构，或许比单纯提升单步推理速度更具长远价值。