論文の概要: VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation

• arxiv url: http://arxiv.org/abs/2605.08553v1
• Date: Fri, 08 May 2026 23:25:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-05-12 23:28:49.730619
• Title: VeriContest: A Competitive-Programming Benchmark for Verifiable Code Generation
• Title（参考訳）: VeriContest: 検証可能なコード生成のための競合プログラミングベンチマーク
• Authors: Zichen Xie, Mrigank Pawagi, Yuxin Liu, Aaditi Rai, Lize Shao, John Berberian, Sicong Che, Wenxi Wang,
• Abstract要約: 大規模言語モデルは自然言語から有用なコードを生成することができるが、その出力は正確性を保証することなく得られる。 検証可能なコード生成は、モデルに実行可能なコードだけでなく、正式な仕様やマシンチェック可能な証明を生成することを要求することによって、テストを越える道を提供する。 We present VeriContest, a benchmark of 946 competitive-playming problem from LeetCode and Codeforces for verible code generation in Rust with Verus。
• 参考スコア（独自算出の注目度）: 2.2194977808724405
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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, focus on only one 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 946 competitive-programming problems from LeetCode and Codeforces for verifiable code generation in Rust with Verus. Each problem pairs a natural language description with 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 further strengthen benchmark quality, we use testing as an additional quality-assurance layer for validating postcondition completeness. VeriContest supports isolated and compositional evaluation of specification generation, code generation, proof generation, and end-to-end verified program synthesis. Evaluating ten state-of-the-art models reveals a sharp gap between coding ability and verifiable code generation: the strongest model reaches 92.18% on natural-language-to-code generation, but only 48.31% on specification generation, 13.95% on proof generation, and 5.29% end-to-end. These results identify proof and specification generation as the central bottlenecks for models and establish VeriContest as a rigorous platform for measuring and training future systems that generate code with machine-checkable correctness.
• Abstract（参考訳）: 大規模言語モデルは自然言語から有用なコードを生成することができるが、その出力は正確性を保証することなく得られる。 検証可能なコード生成は、モデルに実行可能なコードだけでなく、正式な仕様やマシンチェック可能な証明を生成することを要求することによって、テストを越える道を提供する。 しかし、この方向の進捗を測るのは困難である。既存のベンチマークは、しばしば小さく、パイプラインの1つの部分にのみ焦点を合わせ、根本的な証明や厳密な仕様検証の欠如、主流のソフトウェア開発から遠く離れたターゲットの検証設定などである。 We present VeriContest, a benchmark of 946 competitive-playming problem from LeetCode and Codeforces for verible code generation in Rust with Verus。 各問題には、専門家公認の形式仕様、判断承認されたRustコード、Verusチェックされた証明、肯定的かつ否定的なテストスイートと、自然言語記述が組み合わせられている。 VeriContestは、手作業による検証済みのシード問題から、ヒューマン・イン・ザ・ループ・レビューによる半自動拡張まで、3フェーズのパイプラインを通じて構築されている。 ベンチマーク品質をさらに高めるため、テストはポストコンディショナリの完全性を検証するための付加的な品質保証層として使用します。 VeriContestは、仕様生成、コード生成、証明生成、エンドツーエンドの検証プログラム合成の分離および構成的評価をサポートする。 10つの最先端モデルを評価すると、コーディング能力と検証可能なコード生成の間に大きなギャップが生じる:最強のモデルは自然言語からコード生成において92.18%に達するが、仕様生成では48.31%、証明生成では13.95%、エンドツーエンドでは5.29%である。 これらの結果から、モデルの中心的ボトルネックとして証明と仕様生成が特定され、マシンチェック可能な正確性でコードを生成する将来のシステムを測定するための厳密なプラットフォームとしてVeriContestが確立される。

関連論文リスト

• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
  論文  参考訳（メタデータ） (2026-02-10T06:58:26Z)
• VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code [25.916111156888235]
  我々は,Large Language Models (LLM) の形式的検証のための新しいベンチマークを導入する。 筆者らのフレームワークは, 基調整合を定式化された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。 以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。
  論文  参考訳（メタデータ） (2025-10-07T13:19:05Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。 LLM生成コードの正確性を保証することは依然として困難である。 検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
  論文  参考訳（メタデータ） (2025-05-29T06:12:52Z)
• VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [9.383313869205628]
  本稿では,自然言語記述からエンドツーエンドのプログラム検証を評価する新しいベンチマークを提案する。 評価の結果,o3-miniのような最先端(SOTA)モデルでさえ,パスレートが4%未満であることが確認された。
  論文  参考訳（メタデータ） (2025-05-25T19:00:52Z)
• CodeT: Code Generation with Generated Tests [49.622590050797236]
  テストケースを自動的に生成するための事前学習言語モデルについて検討する。 CodeTは生成されたテストケースを使ってコードソリューションを実行し、次に最良のソリューションを選択します。 我々は,HumanEvalとMBPPのベンチマークを用いて,5種類の事前学習モデル上でCodeTを評価する。
  論文  参考訳（メタデータ） (2022-07-21T10:18:37Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。