論文の概要: VERINA: Benchmarking Verifiable Code Generation
- arxiv url: http://arxiv.org/abs/2505.23135v1
- Date: Thu, 29 May 2025 06:12:52 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-30 18:14:07.709875
- Title: VERINA: Benchmarking Verifiable Code Generation
- Title（参考訳）: VERINA: 検証可能なコード生成のベンチマーク
- Authors: Zhe Ye, Zhengxu Yan, Jingxuan He, Timothe Kasriel, Kaiyu Yang, Dawn Song,
- Abstract要約: 大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。
検証可能なコード生成は、この制限に対処するための有望なパスを提供する。
現在のベンチマークでは、エンドツーエンドの検証可能なコード生成がサポートされていないことが多い。
- 参考スコア（独自算出の注目度）: 47.9771074559674
- License: http://creativecommons.org/licenses/by-sa/4.0/
- Abstract: Large language models (LLMs) are increasingly integrated in software development, but ensuring correctness in LLM-generated code remains challenging and often requires costly manual review. Verifiable code generation -- jointly generating code, specifications, and proofs of code-specification alignment -- offers a promising path to address this limitation and further unleash LLMs' benefits in coding. Yet, there exists a significant gap in evaluation: current benchmarks often lack support for end-to-end verifiable code generation. In this paper, we introduce Verina (Verifiable Code Generation Arena), a high-quality benchmark enabling a comprehensive and modular evaluation of code, specification, and proof generation as well as their compositions. Verina consists of 189 manually curated coding tasks in Lean, with detailed problem descriptions, reference implementations, formal specifications, and extensive test suites. Our extensive evaluation of state-of-the-art LLMs reveals significant challenges in verifiable code generation, especially in proof generation, underscoring the need for improving LLM-based theorem provers in verification domains. The best model, OpenAI o4-mini, generates only 61.4% correct code, 51.0% sound and complete specifications, and 3.6% successful proofs, with one trial per task. We hope Verina will catalyze progress in verifiable code generation by providing a rigorous and comprehensive benchmark. We release our dataset on https://huggingface.co/datasets/sunblaze-ucb/verina and our evaluation code on https://github.com/sunblaze-ucb/verina.
- Abstract（参考訳）: 大規模言語モデル(LLM)はソフトウェア開発にますます統合されているが、LLM生成コードの正確性を保証することは依然として困難であり、しばしば手作業によるレビューを必要とする。
検証可能なコード生成 -- コード、仕様、コード固有化アライメントの証明を共同で生成する -- は、この制限に対処し、コーディングにおけるLLMのメリットをさらに解き放つ、有望な道を提供する。
現在のベンチマークでは、エンドツーエンドの検証可能なコード生成がサポートされていないことが多い。
本稿では,コード,仕様,証明生成を包括的かつモジュール的に評価できる高品質なベンチマークであるVerina(Verifiable Code Generation Arena)を紹介する。
Verinaは189の手作業によるリーンのコーディングタスクで構成されており、詳細な問題記述、リファレンス実装、正式な仕様、広範なテストスイートを備えている。
現状のLLMの広範な評価は、検証可能なコード生成、特に証明生成において、検証領域におけるLLMベースの定理証明の改善の必要性を浮き彫りにしている。
最高のモデルであるOpenAI o4-miniは61.4%の正しいコードと51.0%の音と完全な仕様、そして3.6%の成功例を生成できる。
Verinaが厳格で包括的なベンチマークを提供することで、検証可能なコード生成の進歩を触媒することを期待しています。
データセットはhttps://huggingface.co/datasets/sunblaze-ucb/verinaで、評価コードはhttps://github.com/sunblaze-ucb/verinaで公開しています。
関連論文リスト
- CONCUR: Benchmarking LLMs for Concurrent Code Generation [3.386685695989279]
コード生成にLLM(Large Language Models)を活用することは、ソフトウェア工学の分野において、共通のプラクティスとして現れつつある。
既存のベンチマークは主にシーケンシャルなコードに焦点を当てており、並行コード生成でLLMを効果的に評価する能力がない。
このギャップに対処するため、並列コードを生成するLLMの能力を評価するためのベンチマークCONCURを設計した。
論文 参考訳（メタデータ） (2026-03-04T03:22:26Z) - Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。
より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。
そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
論文 参考訳（メタデータ） (2026-02-28T08:35:25Z) - AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
既存のベンチマークでは、個々の言語/ツールのみをテストするため、パフォーマンス番号は直接比較できない。
このギャップに対処するAlgoVeriは、Dafny、Verus、Leanで77ドルの古典的アルゴリズムのベリコーディングを評価するベンチマークです。
論文 参考訳（メタデータ） (2026-02-10T06:58:26Z) - Evaluating and Achieving Controllable Code Completion in Code LLM [89.64782747840225]
命令誘導型コード補完ベンチマークである制御可能コード補完ベンチマーク(C3-Bench)を提案する。
コード補完作業中に,オープンソースのプロプライエタリモデルと高度なプロプライエタリモデルの間に,命令追従機能にかなりのギャップがあることを明らかにする。
結果として得られたQwen2.5-Coder-C3は、C3-Bench上で最先端のパフォーマンスを達成する。
論文 参考訳（メタデータ） (2026-01-22T11:40:04Z) - 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) - CodeGrad: Integrating Multi-Step Verification with Gradient-Based LLM Refinement [12.792149709662874]
CodeGradは厳密な検証技術を反復生成ループに直接組み込む、原則化されたフレームワークを導入している。
コードを微分可能な変数として扱い、構造化されたフィードバックと数学的制約をテキストの擬似階調に変換する。
我々は,HumanEval,HumanEval+,LiveCodeBenchベンチマーク上でCodeGradを評価する。
論文 参考訳（メタデータ） (2025-08-12T22:03:54Z) - IFEvalCode: Controlled Code Generation [69.28317223249358]
本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。
IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
論文 参考訳（メタデータ） (2025-07-30T08:08:48Z) - VerifyThisBench: Generating Code, Specifications, and Proofs All at Once [5.783301542485619]
エンドツーエンドのプログラム検証タスクにおいて,大規模言語モデル(LLM)を評価するために設計された新しいベンチマークを導入する。
評価の結果,o3-miniのような最先端(SOTA)モデルでさえ4%未満のパス率を達成でき,多くの出力がコンパイルに失敗していることがわかった。
論文 参考訳（メタデータ） (2025-05-25T19:00:52Z) - CodeIF: Benchmarking the Instruction-Following Capabilities of Large Language Models for Code Generation [20.013757490442064]
タスク指向の命令に準拠する大規模言語モデル(LLM)の能力を評価するために設計された最初のベンチマークであるCodeIFを紹介する。
CodeIFは関数合成、アルゴリズム命令、コード説明など幅広いタスクを含んでいる。
我々はLLMによる広範囲な実験を行い、これらの課題の要求を満たす上での強みと限界を分析した。
論文 参考訳（メタデータ） (2025-02-26T14:19:49Z) - CodeRAG-Bench: Can Retrieval Augment Code Generation? [78.37076502395699]
検索拡張生成を用いたコード生成の系統的,大規模な解析を行う。
まず、コード生成タスクの3つのカテゴリを含む総合的な評価ベンチマークであるCodeRAG-Benchをキュレートする。
CodeRAG-Bench上のトップパフォーマンスモデルについて、1つまたは複数のソースから検索したコンテキストを提供することにより検討する。
論文 参考訳（メタデータ） (2024-06-20T16:59:52Z) - SWT-Bench: Testing and Validating Real-World Bug-Fixes with Code Agents [10.730852617039451]
ユーザ問題をテストケースに形式化するLLMベースのコードエージェントについて検討する。
我々は人気のあるGitHubリポジトリに基づいた新しいベンチマークを提案し、現実世界の問題、地味なバグフィックス、ゴールデンテストを含む。
コード修復用に設計されたコードエージェントは,テスト生成用に設計されたシステムの性能を上回っている。
論文 参考訳（メタデータ） (2024-06-18T14:54:37Z) - VersiCode: Towards Version-controllable Code Generation [58.82709231906735]
大規模言語モデル(LLM)は、コード生成において大きな進歩を遂げていますが、既存の研究は、ソフトウェア開発の動的な性質を説明できません。
バージョン別コード補完(VSCC)とバージョン別コードマイグレーション(VACM)の2つの新しいタスクを提案する。
VersiCodeについて広範な評価を行い、バージョン管理可能なコード生成が確かに重要な課題であることを示した。
論文 参考訳（メタデータ） (2024-06-11T16:15:06Z) - InfiBench: Evaluating the Question-Answering Capabilities of Code Large Language Models [56.723509505549536]
InfiBenchは、私たちの知識に合ったコードのための、最初の大規模フリーフォーム質問回答(QA)ベンチマークです。
慎重に選択された234の高品質なStack Overflow質問で構成されており、15のプログラミング言語にまたがっている。
InfiBench上で100以上の最新のコードLLMに対して,系統的評価を行い,新しい知見と洞察に富んだ結果を得た。
論文 参考訳（メタデータ） (2024-03-11T02:06:30Z) - StepCoder: Improve Code Generation with Reinforcement Learning from
Compiler Feedback [58.20547418182074]
2つの主要コンポーネントからなるコード生成の新しいフレームワークであるStepCoderを紹介します。
CCCSは、長いシーケンスのコード生成タスクをCurriculum of Code Completion Subtaskに分割することで、探索課題に対処する。
FGOは、未実行のコードセグメントをマスクすることでのみモデルを最適化し、Fine-Grained Optimizationを提供する。
提案手法は,出力空間を探索し,対応するベンチマークにおいて最先端の手法より優れた性能を発揮する。
論文 参考訳（メタデータ） (2024-02-02T13:14:31Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。