AlgoVeri：面向经典算法的验证代码生成对齐基准
AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
AI总结：
为解决跨范式验证代码生成评估缺乏统一方法的问题，提出AlgoVeri基准，在Dafny、Verus和Lean三种语言上评估77个经典算法的验证代码生成，揭示不同验证系统的能力差距。
摘要：
验证代码生成指从严格规范生成形式化验证的代码。近期AI模型在验证代码生成方面展现出潜力，但缺乏跨范式的统一评估方法。现有基准仅测试单一语言/工具（如Dafny、Verus和Lean），且各自覆盖非常不同的任务，因此性能数据无法直接比较。我们通过AlgoVeri基准填补这一空白，该基准在Dafny、Verus和Lean上评估77个经典算法的验证代码生成。通过强制使用相同的功能契约，AlgoVeri揭示了验证系统中的关键能力差距。前沿模型在Dafny中取得了可观的成功（Gemini-3 Flash为40.3%），其中高层抽象和SMT自动化简化了工作流，但在Verus的系统级内存约束（24.7%）和Lean所需的显式证明构造（7.8%）下性能急剧下降。除了总体指标，我们还发现了测试时计算动态的显著差异：Gemini-3有效利用迭代修复提升性能（例如，在Dafny中通过率提高三倍），而GPT-OSS则早期饱和。最后，我们的错误分析表明，语言设计影响改进轨迹：Dafny允许模型专注于逻辑正确性，而Verus和Lean将模型困在持久的语法和语义障碍中。所有数据和评估代码可在https://github.com/haoyuzhao123/algoveri获取。
英文摘要：
Vericoding refers to the generation of formally verified code from rigorous specifications. Recent AI models show promise in vericoding, but a unified methodology for cross-paradigm evaluation is lacking. Existing benchmarks test only individual languages/tools (e.g., Dafny, Verus, and Lean) and each covers very different tasks, so the performance numbers are not directly comparable. We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean. By enforcing identical functional contracts, AlgoVeri reveals critical capability gaps in verification systems. While frontier models achieve tractable success in Dafny ($40.3$% for Gemini-3 Flash), where high-level abstractions and SMT automation simplify the workflow, performance collapses under the systems-level memory constraints of Verus ($24.7$%) and the explicit proof construction required by Lean (7.8%). Beyond aggregate metrics, we uncover a sharp divergence in test-time compute dynamics: Gemini-3 effectively utilizes iterative repair to boost performance (e.g., tripling pass rates in Dafny), whereas GPT-OSS saturates early. Finally, our error analysis shows that language design affects the refinement trajectory: while Dafny allows models to focus on logical correctness, Verus and Lean trap models in persistent syntactic and semantic barriers. All data and evaluation code can be found at https://github.com/haoyuzhao123/algoveri.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
