论文页面 - 扩展 Lean 定理证明器以实现真实代码验证

来源: https://huggingface.co/papers/2610.38174

摘要

EasyProver 是一个基于递归代理和异步搜索的 Lean 证明系统，几乎解决了所有 Putnam 和 IMO 基准问题；而 Aegis 则从竞赛编程题生成更难的验证任务，用于对证明器进行基准测试并支持强化学习。

我们提出了 EasyProver，一个基于递归代理构建的 Lean 证明系统，具备隔离上下文、异步搜索、并行策略探测以及弹性精化服务。使用一个开箱即用的前沿模型，无需额外训练，它就能证明 PutnamBench 672 个问题中的 669 个，以及 IMO 2026 全部六个形式化问题，并通过证明或反驳解决了 NTP4VC 600 个验证条件中的 597 个以及 VERINA 全部 189 个任务。由于这些基准已接近饱和，我们还引入了 Aegis，它将竞赛编程题目转换为针对真实实现的更难的验证任务。该流水线编写安全的 Rust 解决方案，通过 Aeneas 将其翻译为 Lean，生成规格说明，并为每条冻结的陈述标注经内核检查的证明或反驳。它共生成了 2,045 对经过差异化验证的 Rust-Lean 程序对和 11,533 条候选规格说明。与手工编写的基准不同，这些任务承载着来自定点算术、显式失败处理、生成式循环、类型转换和函数式化变异的实现级义务。在 2,000 条陈述的分层样本上，EasyProver 在每条陈述 30 分钟的预算内证明了 1,054 条（52.7%）。同样的任务也可以用于对其他证明器进行基准测试，以及作为 强化学习 的奖励信号。

查看 arXiv 页面 (https://arxiv.org/abs/2610.38174) 查看 PDF (https://arxiv.org/pdf/2610.38174) 添加到收藏 (https://huggingface.co/login?next=%2Fpapers%2F2610.38174)

在代理中获取此论文：

hf papers read 2610.38174

还没有最新版 CLI？curl -LsSf https://hf.co/cli/install.sh | bash

引用此论文的模型 0

暂无模型关联此论文

在模型 README.md 中引用 arxiv.org/abs/2610.38174 即可从此页面链接。

引用此论文的数据集 0

暂无数据集关联此论文

在数据集 README.md 中引用 arxiv.org/abs/2610.38174 即可从此页面链接。

引用此论文的 Spaces 0

暂无 Space 关联此论文

在 Space README.md 中引用 arxiv.org/abs/2610.38174 即可从此页面链接。

包含此论文的合集 0

暂无合集包含此论文

将此论文添加到合集 (https://huggingface.co/new-collection) 即可从此页面链接。