← 研踪 PaperTrailarXiv:2605.08553 · v2
VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
首次提交 2026-05-09 07:25
版本更新 2026-11-08 04:48
雷达观测 2026-11-10 12:16
摘要
Large language models can generate useful code from natural language, but their outputs come without correctness guarantees. Verifiable code generation offers a path beyond testing by requiring models to produce not only executable code, but also formal specifications and machine-checkable proofs. Progress in this direction, however, is difficult to measure: existing benchmarks are often small, cover only part of the pipeline, lack ground-truth proofs or rigorous specification validation, or target verification settings far from mainstream software development. We present VeriContest, a benchmark of 1,006 competitive-programming problems from LeetCode and Codeforces for verifiable code generation in Rust with Verus. Each problem includes a natural language description, expert-validated formal specifications, judge-accepted Rust code, Verus-checked proofs, and positive and negative test suites. VeriContest is constructed through a three-phase pipeline that scales from manually verified seed problems to semi-automated expansion with human-in-the-loop review. To strengthen benchmark quality, we also use testing to validate postcondition completeness. VeriContest supports both isolated and compositional evaluation of specification, code, and proof generation, and end-to-end verified program synthesis. Evaluating ten state-of-the-art models reveals a sharp gap between ordinary coding and verifiable code generation: the strongest model reaches 97.51% on natural-language-to-code generation, but only 57.16% on specification generation, 13.82% on proof generation, and 6.76% end-to-end. These results identify proof and specification generation as the central bottlenecks for current models and establish VeriContest as a rigorous platform for evaluating and training future systems that generate code with machine-checkable correctness.
作者备注：Accepted to NeurIPS 2026 (Evaluations & Datasets Track)
观测到的版本
相邻记录可能跳过中间版本；首次发现 v2 及以上也会标为版本更新。
v2 · 2026-11-08 04:48 · 最新观测版本
VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
Large language models can generate useful code from natural language, but their outputs come without correctness guarantees. Verifiable code generation offers a path beyond testing by requiring models to produce not only executable code, but also formal specifications and machine-checkable proofs. Progress in this direction, however, is difficult to measure: existing benchmarks are often small, cover only part of the pipeline, lack ground-truth proofs or rigorous specification validation, or target verification settings far from mainstream software development. We present VeriContest, a benchmark of 1,006 competitive-programming problems from LeetCode and Codeforces for verifiable code generation in Rust with Verus. Each problem includes a natural language description, expert-validated formal specifications, judge-accepted Rust code, Verus-checked proofs, and positive and negative test suites. VeriContest is constructed through a three-phase pipeline that scales from manually verified seed problems to semi-automated expansion with human-in-the-loop review. To strengthen benchmark quality, we also use testing to validate postcondition completeness. VeriContest supports both isolated and compositional evaluation of specification, code, and proof generation, and end-to-end verified program synthesis. Evaluating ten state-of-the-art models reveals a sharp gap between ordinary coding and verifiable code generation: the strongest model reaches 97.51% on natural-language-to-code generation, but only 57.16% on specification generation, 13.82% on proof generation, and 6.76% end-to-end. These results identify proof and specification generation as the central bottlenecks for current models and establish VeriContest as a rigorous platform for evaluating and training future systems that generate code with machine-checkable correctness.
查看此版本解读 →查看此版本原文 ↗