論文の概要: AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms

• arxiv url: http://arxiv.org/abs/2602.09464v1
• Date: Tue, 10 Feb 2026 06:58:26 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-02-11 20:17:43.416361
• Title: AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms
• Title（参考訳）: AlgoVeri: 古典的アルゴリズムによる検証済みコード生成のためのベンチマーク
• Authors: Haoyu Zhao, Ziran Yang, Jiawei Li, Deyuan He, Zenan Li, Chi Jin, Venugopal V. Veeravalli, Aarti Gupta, Sanjeev Arora,
• Abstract要約: 既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
• 参考スコア（独自算出の注目度）: 54.99368693313797
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: 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.
• Abstract（参考訳）: 検証コーディング(Vericoding)とは、厳密な仕様から正式に認証されたコードを生成することを指す。 最近のAIモデルは、バリコーディングにおいて有望であるが、パラダイム間評価のための統一された方法論が欠如している。 既存のベンチマークでは、個々の言語/ツール(例えば、Dafny、Verus、Lean)のみをテストする。 このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。 同一の機能契約を強制することにより、AlgoVeriは検証システムにおける重要な能力ギャップを明らかにする。 ハイレベルな抽象化とSMT自動化がワークフローを簡素化するDafny(Gemini-3 Flashの40.3$%)では、フロンティアモデルが大きな成功を収める一方、Verus(24.7$%)のシステムレベルのメモリ制約の下でパフォーマンスが崩壊し、Lean(7.8%)が要求する明示的な証明構築(7.8%)が実現された。 Gemini-3は、反復的な修復を効果的に活用してパフォーマンスを向上し(例えば、Dafnyのトリプルパスレート)、GPT-OSSは早期に飽和する。 Dafnyはモデルを論理的正当性にフォーカスできるようにしますが、VerusとLeanのトラップモデルは永続的な構文的およびセマンティック障壁において使用できます。 すべてのデータおよび評価コードはhttps://github.com/haoyuzhao123/algoveri.comで見ることができる。

関連論文リスト

• Prism: Efficient Test-Time Scaling via Hierarchical Search and Self-Verification for Discrete Diffusion Language Models [96.0074341403456]
  LLM推論を改善するための実用的な方法として、推論時計算が再導入されている。 テスト時間スケーリング(TTS)アルゴリズムの多くは、自動回帰デコーディングに依存している。 そこで我々は,dLLM のための効率的な TTS フレームワーク Prism を提案する。
  論文  参考訳（メタデータ） (2026-02-02T09:14:51Z)
• Do Large Language Models Respect Contracts? Evaluating and Enforcing Contract-Adherence in Code Generation [11.445615378917578]
  PACTは、プログラムアセスメントおよび契約順応評価フレームワークである。 契約違反に焦点を当てた包括的なテストスーツコーパスを提供する。 様々なプロンプト条件下でのコード生成の体系的解析を可能にする。
  論文  参考訳（メタデータ） (2025-10-14T01:12:37Z)
• 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)
• From Benchmark Data To Applicable Program Repair: An Experience Report [1.6913109767046948]
  本稿では,プログラムの自動修復へのアプローチについて述べる。 我々はこの目的を達成するために文学の様々な技法を組み合わせている。 実験の結果,我々の手法は標準ベンチマークの他の手法よりも優れていることがわかった。 綿密な検査では、これらのテクニックはいずれも、業界で見られる現実的な欠陥には効かない。
  論文  参考訳（メタデータ） (2025-08-22T03:59:27Z)
• VERINA: Benchmarking Verifiable Code Generation [46.582574591358735]
  大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。 LLM生成コードの正確性を保証することは依然として困難である。 検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
  論文  参考訳（メタデータ） (2025-05-29T06:12:52Z)
• Learning to Solve and Verify: A Self-Play Framework for Code and Test Generation [69.62857948698436]
  大規模言語モデル(LLM)の最近の進歩は、コーディングベンチマークのパフォーマンスを改善している。 しかし、手軽に利用できる高品質なデータの枯渇により、改善は停滞している。 本稿では,単一モデルのコードとテスト生成能力を共同で改善するセルフプレイ・ソルバ検証フレームワークであるSol-Verを提案する。
  論文  参考訳（メタデータ） (2025-02-20T18:32:19Z)
• MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data [85.50740598523818]
  MUSTARDは、高品質で多様性のある定理と証明データの均一な合成をマスターするフレームワークである。 5,866個の有効なデータポイントを持つMUSTARDSAUCEベンチマークを示す。 我々は広範囲な解析を行い、MUSTARDが検証された高品質なステップバイステップデータを生成することを示す。
  論文  参考訳（メタデータ） (2024-02-14T05:57:58Z)

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

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