EasyProver：递归智能体如何攻克真实代码形式化验证

形式化验证长期停留在学术基准与小规模示例上，真实代码的验证却因状态空间爆炸、实现细节复杂而难以规模化。EasyProver 试图用一套由递归智能体驱动的 Lean 证明系统来弥合这道鸿沟——它不依赖专门训练的模型，仅用现成的前沿模型，就在多个接近饱和的基准上给出接近满分的成绩，并同步推出了面向真实实现的新基准 Aegis。

系统如何运行：隔离上下文与异步搜索

EasyProver 的核心是一组递归智能体，每个智能体拥有隔离的上下文。这种设计让证明搜索可以分叉而不互相污染，避免长上下文里的信息干扰。配合异步搜索与并行 tactic 探测，系统能同时尝试多条证明路径；弹性的 elaboration 服务则负责在需要时扩展计算资源，保证证明检查不被单点瓶颈卡住。

这套架构的关键判断在于：与其微调模型去适应证明助手，不如把工程重心放在编排层——让多个有限能力的智能体并行、递归地探索，再借助 Lean 内核的严格检查来筛选结果。原文指出系统"使用现成的前沿模型，没有额外训练"，这一点让 EasyProver 的复现门槛显著降低。

Lean 与 tactic 探测

Lean 是微软研究院主导开发的交互式定理证明器，同时是一门依赖类型编程语言。它既被数学家用来形式化定理，也被工程师用来验证程序正确性。与 Coq/Isabelle 类似，Lean 的证明本质上是一个由内核检查的项（term），而数学家常借助 tactic（策略）以更接近人类推理的方式逐步构造证明。Elaboration 指把用户书写的表面语法展开、推断隐式参数并补全类型信息，最终生成内核可检查项的过程，它往往计算密集且容易成为瓶颈。所谓“并行 tactic 探测”，即在一条证明路径上同时尝试多种战术（如归纳、化简、自动化求解），并行评估收益后再择优推进。这种策略与 Lean 内核的严格检查相结合，使搜索过程既保持高效，又保证每一步都可被可信地验证。

基准成绩：从 PutnamBench 到 VERINA

据论文数据，EasyProver 在 PutnamBench 上证明了 669/672 道题，完成了全部六个 IMO 2026 形式化问题，并在 NTP4VC 上解决了 597/600 个验证条件。VERINA 的全部 189 个任务也全部完成，方式包括证明与反证两种。

这些数字传递出一个明确信号：传统竞赛数学与部分程序验证基准已接近饱和。当证明系统能以如此高的比例通关，基准本身的区分度就所剩无几。作者也直言这些基准"接近饱和"，这正是他们转向构建新基准的直接动因。反证路径同样值得注意——系统不只会构造证明，也能给出被内核接受的反例，这对验证条件的真实性判断至关重要。

Aegis：把竞赛题变成真实实现的验证任务

Aegis 的构建流程颇有工程巧思。它先把竞赛编程问题转化为针对真实实现的、更难的验证任务：管道先写出安全的 Rust 解法，再借助 Aeneas 翻译成 Lean，随后生成规约，最后为每条冻结的语句标注经内核检查的证明或反证。

产出规模方面，Aegis 生成了 2,045 对经过差分验证的 Rust-Lean 程序对，以及 11,533 条候选规约。与手写基准的最大区别在于，这些任务携带实现层面的义务：固定宽度算术、显式失败、生成的循环、类型转换以及函数化的可变状态。换句话说，验证者必须直面真实代码里那些容易被教科书忽略的角落。

Aeneas 与 Rust-Lean 差分验证

Aeneas 是一个将 Rust 程序转化为 Lean 函数式模型的工具，由微软研究院等机构开发，用于对真实系统代码进行形式化推理。它把 Rust 的所有权、借用与可变状态翻译为纯函数式的 Lean 定义，使验证者能在定理证明器中讨论程序行为。所谓“差分验证”，是指同时保留 Rust 源码与其 Lean 模型，并检验两者在可观测行为上一致；在 Aegis 的流程中，管道还会为每条冻结语句生成规约，并标注经内核检查的证明或反证。这种双重表示让任务既贴近真实实现，又能在 Lean 中被机械检查，从而弥补手写基准往往忽略实现层义务（如固定宽度算术与显式失败）的缺陷。

真实代码上的表现与后续用途

在一份包含 2,000 条语句的分层样本上，EasyProver 在每条语句 30 分钟的时间预算内证明了 1,054 条，占 52.7%。原文用"much harder"形容这些任务相对竞赛基准的难度跃升——从接近满分跌到略高于一半，恰好说明 Aegis 并未被现有方法轻易击穿。

作者指出，这批任务还有两种用途：一是作为基准去评测其他证明器，二是作为强化学习的奖励信号。前者意味着社区有了一个不易饱和的评测场；后者则指向一条自我改进的路径——用内核检查过的证明与反证作为可验证奖励，训练更强的证明智能体。

可验证奖励与强化学习

形式化证明的内核检查结果天然构成一种“可验证奖励”：证明通过即正例，反证被接受即负例，无需人工标注或奖励模型。与 RLHF 依赖人类偏好不同，这种奖励信号由 Lean 内核机械判定，几乎不可伪造。将此类信号用于强化学习训练证明智能体，是近年来定理证明方向的重要思路——模型可以自主生成大量尝试，再由内核筛选，从而在无监督数据的情况下持续自我改进。Aegis 提供的真实实现任务进一步把这种奖励从竞赛数学扩展到工程代码，使训练分布更接近实际验证场景。

工程意义与待观察之处

EasyProver 的价值不只在分数，而在于展示了一条不依赖专门训练的规模化路径：隔离上下文、异步搜索、并行探测与弹性 elaboration 的组合，把通用模型的推理能力导向形式化证明这一高门槛领域。Aegis 则补上了评测侧的缺口，让"真实实现验证"有了可重复、可扩展的任务来源。

需要留意的是，52.7% 的通过率仍留下大量未解语句，固定宽度算术与显式失败等实现细节正是难点所在。系统在更大规模代码库、更长证明链上的表现，以及 Aegis 生成规约的质量分布，仍需更多独立分析来检验。