arXiv · Software Engineering· Traian Serbanuta, Jun Xu, Andrei Stefanescu, Cosmin Radoi·2026-10-12 12:00· 2 小时前精选AI 评分61

用 Lean 4 后端 Rust 验证器解决 VeriContest

Solving VeriContest with a Lean-Backed Rust Verifier

AI 导读

论文报告用 Rust-Prover 解决 VeriContest 的证明生成任务，Verus 规范和 Rust 代码被转写为 Lean 定理，1007 个问题的 1325 个定理全部得证。

推荐理由

原文用 Lean 4 后端重做 VeriContest 证明任务，给出成本、中位耗时和模型对比，可作为形式化验证与模型推理投入的参照。