EasyProver：让Lean证明器走向真实代码验证

导语

自动定理证明正在从“解数学题”转向“检查真实程序”。论文《Scaling Lean Theorem Proving for Real-World Code Verification》介绍了EasyProver，并配套提出Aegis数据生成流程，试图解决一个越来越明显的问题：当传统基准被模型接近解决后，如何继续衡量证明系统在复杂软件上的可靠性？

EasyProver如何扩展搜索能力

EasyProver建立在Lean之上，核心并不是重新训练一个专用模型，而是把现成的前沿模型组织成协作式证明系统。其主要机制包括：

• 使用递归代理拆解和推进证明任务；
• 为不同搜索分支提供隔离上下文，降低相互干扰；
• 通过异步搜索和并行战术尝试扩大探索范围；
• 采用可弹性扩展的 elaboration 服务，处理Lean代码的解析与类型检查负载。

在PutnamBench中，系统解决了672道题中的669道；在材料列出的六个IMO 2026形式化任务中全部完成。在NTP4VC验证条件上，EasyProver解决597/600个任务，并对189个VERINA任务全部给出证明或反驳。这里的结果显示，工程化的搜索调度同样可能成为自动证明性能的关键，而不只是模型本身的规模。

Aegis把难点放回程序实现

研究团队认为，上述基准已接近饱和，因此设计了Aegis。它从竞赛编程问题出发，生成安全Rust程序，再借助Aeneas将实现转换到Lean，并自动产生候选规格。每个冻结后的命题都通过内核检查的证明或反驳进行标注。

Aegis目前生成了2,045组经过差分验证的Rust-Lean程序对，以及11,533条候选规格。与手工编写的数学基准相比，这些任务必须面对固定宽度整数运算、显式失败路径、生成式循环、类型转换，以及将可变操作函数化等问题，因此更接近实际软件验证中的摩擦点。

在分层抽取的2,000条语句上，EasyProver在每条30分钟的预算内证明了1,054条，占52.7%。这个比例并非“已经解决真实代码验证”，但它提供了比传统题库更有区分度的测试面。Aegis还可以用于评估其他证明器，或作为强化学习中的奖励来源。

意义与局限

这项工作的重要性在于，它把证明系统的竞争从单一准确率，推进到搜索架构、验证数据和程序语义的共同较量。内核检查的标签有助于减少未经验证的自动生成结论，而Rust到Lean的转换则让实现行为成为规格验证的一部分。

同时，52.7%的结果也说明真实代码仍远比标准数学题复杂。未来系统需要更好地处理长程程序依赖、规格质量和反驳结果的可解释性。对开发者而言，Aegis提供了一个方向：AI代码生成的下一步，不只是写出能运行的程序，还要能对固定实现给出机器可检查的保证。

来源：Hugging Face Daily Papers