arXiv cs.AI· Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi·· 6 天前AI 评分62
用 Lean 4 后端 Rust 验证器 Rust-Prover 完成 VeriContest 全部 1325 个定理证明
Solving VeriContest with a Lean-Backed Rust Verifier
AI 导读
论文报告用 Lean 4 后端验证器 Rust-Prover 完成 VeriContest 的证明生成任务，1007 道题的全部 1325 个定理均被证明。其中 1259 个定理在 Claude Opus 5.5 上单次运行不到 32 小时内完成，中位耗时 3.2 分钟、每个证明 1.17 美元，70% 在首次迭代即通过。
正文 · AI 翻译
摘要：VeriContest 是一个包含 1007 道 Rust 竞赛编程题目的基准测试，每道题都配有 Verus 规范、一个评测通过的解答以及一个 Verus 证明。其作者报告称，证明生成是前沿模型的瓶颈：在给定规范和代码的情况下，最佳模型首次尝试即可为 13.95% 的题目生成评测通过的 Verus 证明。我们报告了使用 Rust-Prover（一个由 Lean 4 支持的 Rust 验证器）解决同一证明生成任务的情况。Verus 规范和 Rust 代码被重新表述并翻译为 Lean，每个规范成为一个定理，智能体以 Lean 的内核作为最终检查来证明这些定理。全部 1007 道题目的全部 1325 个定理均被证明。其中 1259 个定理在 Claude Opus 5.5 上以一次运行在 32 小时内完成证明，每个证明的中位时间为 3.2 分钟、成本为 1.17 美元，且其中 70% 在第一次迭代中完成。重新表述的规范已对照基准测试的测试套件进行检查，并在没有适用测试套件的地方进行了人工审查。没有一个是错误的或被弱化的。翻译后的 Lean 程序在基准测试的 21,413 个测试用例上运行，且每一个的输出都与 Rust 程序相同。在四个 Claude 和四个 GPT 模型、五种推理强度设置下，每个当前前沿模型在每种设置下都能证明一个十定理样本中的几乎全部定理，而提高推理强度只会增加成本，不会增加证明数量。最便宜的 Claude 设置，即低推理强度的 Sonnet 5.5，证明了全部 50 个最难的定理。我们还使用 Claude Opus 5.5 在 50 个参考证明最长的题目上重新运行了基准测试自身的 Verus 协议。仅 Opus 5.5 就未能证明其中之一。
| 学科： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI）；软件工程（cs.SE） |
| 引用为： | arXiv:2610.03994 [cs.LO] |
| （或 arXiv:2610.03994v2 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.03994 arXiv 颁发的 DOI，经由 DataCite |
提交历史
来自：Jun Xu [查看电子邮件]
[v1]
2026年10月2日星期五 19:56:10 UTC（11 KB）
[v2]
2026年10月9日星期五 15:19:31 UTC（12 KB）
来源：arXiv cs.AI · arxiv.org