发表机构
Asymptotic（Asymptotic公司）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文用 Lean 4 支撑的 Rust 验证器 Rust-Prover 解决了 VeriContest 基准中的证明生成任务，证明了全部 1325 个定理，多数在低成本下完成，且翻译程序输出与 Rust 一致。
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 未能证明其中一个。
英文摘要
VeriContest is a benchmark of 1007 competitive-programming problems in Rust, each with a Verus specification, a judge-accepted solution, and a Verus proof. Its authors report that proof generation is the bottleneck for frontier models: given the specification and the code, the best model produces an accepted Verus proof for 13.95% of the problems on the first attempt. We report on solving the same proof-generation task with Rust-Prover, a verifier for Rust backed by Lean 4. The Verus specification and the Rust code are restated and translated into Lean, each specification becomes a theorem, and agents prove the theorems with Lean's kernel as the final check. All 1325 theorems of all 1007 problems were proved. 1259 of them were proved in one run of under 32 hours on Claude Opus 5.5, at a median of 3.2 minutes and $1.17 per proof, and 70% of them on the first iteration. The restated specifications were checked against the benchmark's test suites, and reviewed where no suite applies. None was wrong or weakened. The translated Lean programs were run on 21,413 of the benchmark's test cases and produced the same output as the Rust programs on every one. Across four Claude and four GPT models at five reasoning-effort settings, every current frontier model proves nearly all of a ten-theorem sample at every setting, and more effort raises the cost without raising the number of proofs. The cheapest Claude setting, Sonnet 5.5 at low effort, proves all of the 50 hardest theorems. We also rerun the benchmark's own Verus protocol with Claude Opus 5.5 on the 50 problems with the longest reference proofs. Opus 5.5 alone fails to prove one of them.
