Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
Yuqing Li, Zeguan Wu, Yu Gan, Junyu Liu
cs.AI, cs.LG, quant-ph
2026-07-20
这篇用一个小型可信运行时包裹完全可变的工作区(工作流、提示、工具),让代理和基准共同演化,每代胜者改任务分布。15 代后留出 miniF2F 解题率从种子 12.7% 升到 45.1%,固定基准对照只到 32.0%。
形式化数学证明(用 Lean)里,Agent 强不强不只看证明器本身,还看它围绕 Lean 的工作流:怎么拆解证明义务、怎么用工具、怎么读编译器反馈、怎么诊断失败、怎么修复、怎么维护证明上下文。手工设计的工作流(LEAP、Goedel-Architect)能把 miniF2F-test 推到 99.2%,说明工作流是性能大头。这篇问的是:这种工作流能不能演化出来,不必手工设计?
架构是一个小型、固定、可信的运行时,包裹一个完全可变的工作区。运行时管正确性(Lean 验证、评测、基准管理),自己不被演化搜索碰到;工作区里的证明工作流、提示、工具全可变,任由代理重写。
和大多数自演化系统不同的是,这套系统让代理和它的基准一起演化。每代之间,得分最高的代理(冠军)通过两种方式修订任务分布。一是 mastery-throttled curriculum(掌握节流的课程):某一级被掌握后才引入更难的题,具体说,当某级掌握度 m 低于阈值 0.70 就同级换题,达到 0.70 就升级。二是 single-anchor recalibration(单锚点重校准):基准变了之后,把冠军在新基准上重跑一遍,保持分数可比。
整个演化锁在一个 Lean 接地的验证回路里。不管代理怎么改自己,只有当行为在可信 Lean 快照下产出被验证的证明才算成功;每次尝试必须吐出机器可读、Lean 接地的证明上下文,表示形式可以变,「接地的真实性」被强制。这套重验证专门防伪造:拒绝顶层 Lean 命令、要求真证明、清洗证书。
跑了 15 个活跃代,活跃基准 76 个任务(初始 L1:L2:L3=27:46:3),在从不参与训练的 miniF2F 留出测试集(244 题)上评测,后端是 DeepSeek(deepseek-v4-pro,贪心解码):
| 配置 | 留出集解题率 |
| 种子代理 | 12.7% |
| 最佳固定基准代理 | 32.0% |
| 最佳共演化代理(第 15 代) | 45.1% |
基准难度系数从 1.00 涨到 3.17,说明课程确实在变难。共演化比固定基准多出 13 个百分点,验证了「代理和基准一起长」的价值。
演化过程里有个反直觉的发现:赢的工作流是「以修复为中心」(生成证明、读 Lean 反馈、有限重试),不是以拆解为中心。拆解类工作流反复出现,但都被竞争淘汰,因为多一层拆解就多几个失败点(JSON 解析错、引理不自洽、提示变长、超时)。被演化出来的可变工具,主要是用来查证那些幻觉出来的 Lean 函数名(#check 探针、引理验证、带命名空间的搜索)。很大的修复循环(10-12 次)也被淘汰,因为不稳定。
对做形式化证明或 agent 工作流的人,这篇示范了一种省人工的路子:别手写工作流,让它在一个可信验证回路里自己长出来。更重要的是,它把「基准」从被动标尺变成主动的共演化对象,用掌握节流的课程自动调节难度,避免了固定基准早早就被「刷爆」、失去训练信号的问题。这套思路不限于 Lean,任何有可信验证器的 agent 场景都能借。
留出集 45.1% 离手工设计的 Goedel-Architect 的 99.2% 还差很远(虽然后端不同,不完全可比),说明演化到顶尖手工工作流还有距离,可能需要更长的运行、更大的种群。研究只跑了单次,没有方差估计。赢的路径始终是「以修复为中心」,拆解这条路没走通,作者自己也觉得应该直接奖励「被验证的拆解」。证明上下文最终稳定成浅层支撑,没长成深层的依赖图。后端即便温度设为 0,输出仍有不可忽略的不稳定。