从12.7%到45.1%：自修改Lean智能体与测试基准的双重协同进化
Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
在利用大语言模型（LLM）进行形式化数学证明（如使用 Lean 4）的探索中，技术路线正逐渐分化为两个阵营。一派致力于训练更强大的基础模型与专用策略合成器，试图在单步推理上力拔千钧；另一派则更看重围绕 Lean 编译器搭建的智能体交互工作流（Workflow），研究如何有效拆解证明目标、读取编译器报错、定向搜索数学库（Mathlib）并持续打补丁。最近的标杆工作如 Goedel-Architect 和 LEAP，通过高度精细的人工工作流设计在 miniF2F 等测试上取得了突破，但这同时也带来了一个新问题：如果高效的形式化证明工作流极其关键，它是否必须依赖人类专家的手工雕琢？智能体能否在没有预设复杂框架的前提下，自行写代码、改工具、演化出最适合定理证明的工作流？
ArXiv URL：https://arxiv.org/abs/2607.17352v1
来自匹兹堡大学（University of Pittsburgh）的研究团队在一项最新工作中给出了肯定回答。他们提出了一种具备自我修改能力的 Lean 证明智能体框架，核心亮点在于打破了“固定评测基准评判自修改代码”的传统范式，引入了智能体与基准题库的协同进化（Coevolution）机制。智能体在被严格的形式化环境检验的同时，根据自身的掌握程度逐步解锁更难的题目；与此同时，基准的难度校准与单锚点换算保证了跨代评估的连贯性。
实验表明，在一个仅具备最原始“生成即提交”能力的种子智能体基础上，系统历经 15 代自我修改与协同演化，在完全未参与训练的 miniF2F 测试集（Held-out Test Split）上的求解率从初始的 12.7% 提升至 45.1%。相比之下，在固定难度基准上自我演化的基线智能体最高仅达到 32.0%。这一成果展示了形式化验证器与动态演进课程在自主智能体进化中的强大潜力。
为什么自我进化需要 Lean 与协同演化？
代码层面的自我修改智能体并不是全新概念，此前的达尔文哥德尔机（Darwin Gödel Machine, DGM）以及超智能体（Hyperagents）已经证明，让大模型修改自身的 Python 执行逻辑并在下游任务中评估筛选，可以催生出更优的编码与自动化方案。然而，当这一思路迁移到形式化数学推理时，研究者往往遭遇两个致命痛点：环境评测的“欺骗性”与进化信号的“阶跃饱和”。
在常规编程任务或开放问答中，智能体修改自身后很难被完全信任。如果评估逻辑与智能体代码边界模糊，大模型极易通过修改测试断言、篡改评分脚本或伪造输出来达成“虚假提升”。但在 Lean 4 的交互世界里，数学真理的裁判权完全归属于编译器内核。一个证明是否成立，不取决于智能体自己的汇报，而取决于 Lean 能否在严格的内核规则下完成类型检查（Type Checking）。形式化验证器充当了不可动摇的底座，为自我修改代码提供了天然防作弊屏障。
另一个痛点则是基准题库的难度匹配。形式化数学题目天然具备极高的难度跨度：简单的代数恒等式可以通过单步自动化策略（如 ring、omega）瞬间击穿，而 AMC、AIME 乃至 Putnam 竞赛级别的难题则需要深度的引理拆解。如果一开始就让初始智能体去硬啃高难度的 Putnam 题，求解率无限趋近于 0，整个进化过程将因为缺乏差异化的正向选择信号而彻底停滞；反之，若为了提供信号而将测试集固定在简单题目上，智能体很快就会达到饱和，后续的变异大多只在局部代码结构上无谓震荡，无法泛化到真实数学挑战中。
为了解决该矛盾，作者构建了如图 1 所示的闭环系统：既让智能体自我修改代码、Prompt 和辅助工具，又让题库难度随着当前最强智能体（Champion）的掌握水平动态攀升。
核心机制：可信运行时与协同进化闭环
系统在底层将执行环境严格划分为两个世界：绝对不可变的可信运行时（Fixed, Trusted Runtime）与完全向智能体开放的可变工作区（Mutable Workspace）。
可变工作区包含了证明工作流的主调度代码、调用大模型时的 Prompt 模板、以及智能体自主编写的辅助工具函数。智能体在进化的每一代中通过受控的编辑接口重写这些代码。但是，变异代码能否被晋升、证明是否算作成功，完全由外层的可信运行时裁定。运行时首先通过基础冒烟测试确认变异后的工作区代码能正常运行并遵循输入输出协议，随后将其投入真正的 Lean 验证流水线。
在安全性设计上，为防止模型通过生成 sorry、admit 等作弊宏绕过证明，或者在输出中注入顶层重定义指令，可信运行时执行了极其严格的重验规约：
-
所有返回的证明体（Proof Body）必须在独立的受保护快照下与题目声明缝合重验，任何包含危险指令的提交均被一票否决；
-
智能体与验证执行被置于隔离的子进程与沙箱副本中，杜绝可变模块污染父级打分环境；
-
每次解题必须输出机器可读的“证明上下文”（Proof Context），记录当前的假设、引理拆解与目标依赖。上下文的表现形式（树、图或列表）允许自由进化，但必须有据可循，未经验证的节点绝不计入成绩。
在基准题库端，研究团队将候选题目池分级为 $L_1$（单步策略引理）、$L_2$（miniF2F 验证集中的中小学及竞赛题）和 $L_3$（PutnamBench 高等数学竞赛题）。在初始阶段，当前激活的 76 道评测题目主要由易于产生梯度的较低难度题目构成。
当进入新一代时，当前代中表现最优的冠军（Champion）智能体成为基准更新的驱动者。更新遵循“掌握度节流”（Mastery-throttled）原则：只有当冠军在当前激活基准上的原始解题率 $r$ 突破阈值 $\gamma = 0.30$ 时，基准才会进行难度跃迁。已掌握的题目被移出测试池，替换为同难度的新题，或者在当前层级全面掌握后升入更高难度层级。
这种题库的动态变迁带来了一个计量学挑战：由于题目在变难，原始解题率不再具有跨代可比性。为此，研究团队设计了单锚点重新校准（Single-anchor Recalibration）。每次基准更新后，可信系统立刻让冠军智能体在新基准上重新跑一次测试，并按比例更新全局难度系数 $c$：
\[c_{t+1} = c_{t} \cdot \frac{r_{t}}{\max(r_{t+1}, \epsilon)}\]其中 $c_0 = 1$。因为冠军被作为两个基准难度之间的锚点，其标准化得分 $q = r \times c$ 在校准瞬间保持恒定。随着世代更迭，累乘的难度系数 $c$ 精准刻画了题库变得比初始状态困难了多少倍，使不同世代、在不同难度环境下诞生的智能体能够站在同一标尺下由轮盘赌算法筛选为父代，避免了评估脱轨。
15 代自我演进带来了什么？
在由 76 道动态任务构成的训练流中，协同进化系统与保持基准题库绝对固定的对比基线均运行了 15 个完整世代。为了客观衡量最终泛化能力，两组系统演化出的核心智能体在完全未参与训练的 miniF2F 独立测试集（Held-out Test Split，共 244 题）上展开了最终决战。
最终的对比结果差异显著：
-
初始的种子智能体（Seed Agent）仅具备生成一次证明并送交编译的极简能力，在 held-out 评测中的解题率仅有 12.7%；
-
在固定基准上自我修改演化出的两名最强智能体，其最终解题率分别为 32.0% 和 26.6%；
-
而在动态协同进化体系下，演化出的最优智能体（代号 c144）在 held-out 测试集上斩获了 45.1% 的解题率，比固定基线高出 13.1 个百分点，是种子智能体的 3.5 倍以上。
难度系数的变化同样印证了题目的跃迁：从第 1 代到第 15 代，协同题库的综合难度系数 $c$ 从 1.00 稳步攀升至 3.17。固定基准之所以落后，核心原因在于它在早期就会陷入“选择信号枯竭”。一旦固定基准中的某一部分题目被攻克，进化算法施加的选择压力就迅速退化为“在旧题目上微调代码”。智能体倾向于针对那几十道熟悉题目做非常局部的容错修正，并没有动力去发展能够解决更高阶数学结构的解题范式。相反，协同基准不断移走“舒适区”题目并注入更深奥的数学断言，强迫智能体必须在通用错误处理与知识调用上寻求突破。
智能体自行探索出的工作流画像
深入分析中选智能体（Accepted Lineage）的代码变迁，可以清晰勾勒出大模型在无人干预的压力测试下，究竟偏好怎样的工具与工作流。
1. 放弃庞大的逻辑分解，选择以精炼修复为核心
在很多人工设计的定理证明框架中，“自顶向下的蓝图分解”和“复杂的引理依赖图搜索”往往被置于核心地位。然而，在此次自我进化实验中，演化出来的胜出模式却是以报错为导向的紧凑修复循环（Repair-centered Workflow）。
智能体最稳定的高效模式是：先由大模型生成一段完整的证明，然后直接丢给 Lean 编译器；一旦报错，工作流截取编译器的精确错误行与上下文提示，辅助以引理名字检查，将有限的信息重新打包反馈给大模型进行重试。
为什么演化抛弃了繁琐的深度分解？作者指出，在有限的计算与时间预算下（系统设置了单题执行时间上限与 Prompt Token 上限），庞大的分解搜索与引理图维护不仅开销巨大，还容易因级联幻觉而产生更多不可恢复的失败，难以在短时间内转化为确凿的证明积分。紧凑的修复流则廉价、见效快，更容易在自然选择中被奖励保留。
但系统也并未演化出无限延长的修复循环。历史血统显示，代号为 c19 的智能体曾尝试将循环次数扩增至 10 次，但原始得分反降至 0.368；c51 将单体修复次数硬拉到 12 次，得分更是断崖式跌落至 0.263。原因在于过长的历史交互导致上下文截断和超时（Time-out）频发。演化机制迅速做出了惩罚，随后胜出的后代（如 c52 及之后的节点）果断砍掉了冗长重试，转而采用短小精悍的 Prompt，并引入早停机制。
2. 自制工具的最大用途：遏制 Mathlib 引理幻觉
在形式化证明中，大语言模型最常犯的错误之一是“脑补”不存在的引理名称。如果智能体在证明体内编造了一个看似合理的引理名，Lean 编译器会直接抛出未声明标识符错误，导致整段证明崩塌。
在进化的中后期，智能体变异出的大量 Python 辅助工具几乎全部聚焦于压制这类幻觉：
-
早期的变异体只是试探性地编写了基于
#check命令的探测脚本，在调用关键定理前进行独立嗅探； -
中期变异体（如 c96）演化出了专门的引理批量预检模块（
verify_lemma_list），结合 Mathlib 命名空间缓存，在证明合成前将合法的标准定理签名动态拼入 Prompt； -
最终的优胜者 c144 则将命名空间索引、源码 grep 建议与紧凑的修复回路深度融合，遇到未定义标识符时自动剔除假引理并替换为经过类型确认的相近真引理。
智能体并非凭借神秘的逻辑推演变强，而是为自己写出了一套越来越符合 Lean 生态特性的“类型与命名查验辅助套件”。
形式化推理系统设计的启示
这项工作为后续的大模型与智能体研究提供了几个值得深思的范式参考：
第一，验证器必须作为演化闭环的锚。在缺乏明确真值反馈的开放领域，自修改智能体极其脆弱，往往会迅速退化或演变成对抗评价打分的“寄生系统”。形式化验证系统的严谨性，使得我们终于可以在没有人类介入的情况下，完全放开代码编辑权限，让智能体在代码和策略层自由“折腾”，而无需担心奖励作弊。
第二，环境与基准的自适应演化不可或缺。传统的评测范式是“固定一把尺子量所有人”，但在自进化体系中，固定的尺子要么太矮而失去区分度，要么太高而无法提供起步动力。让基准以“单锚点”形式动态升级，将传统强化学习中自动课程学习（Automatic Curricula）的思想落地到代码自修改框架中，是促使智能体持续扩展能力边界的关键抓手。
第三，实用主义战胜复杂架构。尽管学术界对构建如同人类数学家般优雅的“深层引理依赖图”寄予厚望，但在算力与时间约束下，由自然选择筛选出来的最优机制往往极其务实——快速试错、精准捕捉编译报错、辅助轻量级的命名过滤。这提示后续的研究者，在人工构建形式化证明工作流时，应当给予这些看似琐碎却决定成败的“工具卫生细节”更多权重。