arXiv cs.AI· Debargha Ganguly, Divya Raghunathan, Dejan Jovanovi\'c, Vikash Singh, Soonho Kong, Aaron Tomb, Aman Goel, Ferhat Erata, Sam Bayless·· 13 小时前AI 评分58
EasyProver：用递归智能体扩展 Lean 定理证明以验证真实代码
Scaling Lean Theorem Proving for Real-World Code Verification
AI 导读
论文提出 EasyProver，一个由隔离上下文的递归智能体、异步搜索、并行 tactic 探测和弹性 elaboration 服务构成的 Lean 证明系统。
正文 · AI 翻译
摘要：我们提出 EasyProver，一个由具有隔离上下文的递归智能体构建的 Lean 证明系统，具备异步搜索、并行策略探测和弹性精化服务。使用未经额外训练的现成前沿模型，它证明了 669/672 个 PutnamBench 问题以及全部六个 IMO 2026 形式化问题，并通过证明或反驳解决了 597/600 个 NTP4VC 验证条件以及全部 189 个 VERINA 任务。由于这些基准已接近饱和，我们还引入了 Aegis，它将竞赛编程问题转换为针对真实实现的难度更高的验证任务。该流水线编写安全的 Rust 解决方案，使用 Aeneas 将其转换为 Lean，生成规范，并为每个冻结语句标注经内核检查的证明或反驳。它产生了 2,045 个经过差分验证的 Rust-Lean 程序对和 11,533 个候选规范。与手写基准不同，这些任务带有来自定宽算术、显式失败、生成的循环、类型转换和函数化变异的实现级义务。在 2,000 个语句的分层样本上，EasyProver 在每条语句 30 分钟的预算内证明了 1,054 条（52.7%）。这些任务还可用于对其他证明器进行基准测试，并作为强化学习的奖励。
| 学科： | 计算与语言（cs.CL）；人工智能（cs.AI）；计算机科学中的逻辑（cs.LO）；软件工程（cs.SE） |
| 引用为： | arXiv:2610.38174 [cs.CL] |
| （或此版本的 arXiv:2610.38174v1 [cs.CL]） | |
| https://doi.org/10.48550/arXiv.2610.38174 由 DataCite 颁发的 arXiv DOI |
提交历史
来自：Debargha Ganguly [查看电子邮件]
[v1]
2026年10月28日星期三 02:23:25 UTC（2,533 KB）
来源：arXiv cs.AI · arxiv.org