論文の概要: Self-Spec Verifiable Code Generation

• arxiv url: http://arxiv.org/abs/2609.39568v1
• Date: Wed, 30 Sep 2026 12:02:45 GMT
• ステータス: 翻訳完了
• システム内更新日: 2026-10-01 18:57:27.641441
• Title: Self-Spec Verifiable Code Generation
• Title（参考訳）: 自己検証可能なコード生成
• Abstract要約: 大型言語モデル(LLM)は、テストで欠落したコーナーケース上で信頼できないコードを生成するが、形式的検証はマシンチェック可能な保証を提供する。 自己検証可能なコード生成のためのベンチマークであるVeriCodeBenchを紹介する。
• 参考スコア（独自算出の注目度）: 33.09399251068682
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) may generate unreliable code on corner cases missed by testing, while formal verification can provide machine-checkable guarantees. Recently, researchers have proposed several benchmarks to evaluate the capabilities of LLMs in generating formally verifiable code, where LLMs need to formulate formal specifications, generate the corresponding code, and verify its correctness. However, existing benchmarks have two key limitations: (I) They primarily evaluate specification and code generation stage-wise, with code generation typically conditioned on an oracle specification. This setup overlooks whether strong stage-wise performance translates into end-to-end success. (II)They mainly focus on a single proof-oriented language and mathematically structured tasks, offering limited coverage of tasks common in software development. In this paper, we introduce VeriCodeBench, a benchmark for self-spec verifiable code generation, where the LLM relies solely on its own generated specification and code throughout the entire process. VeriCodeBench contains 400 language-native problems across C, Java, Rust, and Python, covering practical concerns in software development. We evaluate specification coverage, code validity, and joint problem-level success. We further introduce CodeNova to enhance the capabilities of LLMs in self-spec verifiable code generation. CodeNova makes requirements explicit through constraint-guided specification and uses verifier feedback to guide targeted implementation repairs. Experimental results reveal that self-generated specifications remain a major bottleneck, while providing more sophisticated specifications may not necessarily lead to higher verification success rates. CodeNova substantially improves performance across all evaluation metrics, enabling Claude Sonnet 5 to achieve the strongest results under the self-spec protocol.
• Abstract（参考訳）: 大型言語モデル(LLM)は、テストで欠落したコーナーケース上で信頼できないコードを生成するが、形式的検証はマシンチェック可能な保証を提供する。 近年、LLMが形式仕様を定式化し、対応するコードを生成し、その正当性を検証し、正式な検証可能なコードを生成する際のLCMの能力を評価するためのベンチマークが提案されている。 しかし、既存のベンチマークには2つの重要な制限がある。 (I) 主に仕様とコード生成を段階的に評価する。 このセットアップは、強力なステージワイドパフォーマンスがエンドツーエンドの成功に繋がるかどうかを見落としている。 (II)主に1つの証明指向言語と数学的に構造化されたタスクに焦点を当て、ソフトウェア開発に共通するタスクの限られた範囲を提供する。 本稿では,自己検証可能なコード生成のためのベンチマークであるVeriCodeBenchを紹介する。 VeriCodeBenchには、C、Java、Rust、Pythonで400の言語ネイティブな問題が含まれており、ソフトウェア開発における実践的な懸念をカバーしている。 我々は,仕様カバレッジ,コード妥当性,共同問題レベルの成功を評価する。 さらに、自己検証可能なコード生成におけるLLMの能力を高めるためにCodeNovaを導入します。 CodeNovaは制約付き仕様を通じて要求を明確にし、検証者フィードバックを使用して、対象とする実装の修正をガイドする。 実験結果から、自己生成仕様は依然として大きなボトルネックであり、より洗練された仕様を提供することは、必ずしも高い検証成功率につながるとは限らないことが判明した。 CodeNovaは、すべての評価指標のパフォーマンスを大幅に改善し、Claude Sonnet 5がセルフスペックプロトコルの下で最も強力な結果が得られるようにした。

関連論文リスト

• CodeSpecBench: Benchmarking LLMs for Executable Behavioral Specification Generation [49.30536937161147]
  本稿では,実行ベース評価プロトコルの下で実行可能な動作仕様生成のためのベンチマークであるCodeSpecBenchを紹介する。 CodeSpecBenchは関数レベルとリポジトリレベルのタスクの両方をサポートし、仕様を実行可能なPython関数としてエンコードする。 リポジトリレベルのタスクでは、最高のモデルが20.2%のパス率しか達成できないため、パフォーマンスが大幅に低下するのを観察します。
  論文  参考訳（メタデータ） (2026-04-14T04:31:45Z)
• Are LLMs Reliable Code Reviewers? Systematic Overcorrection in Requirement Conformance Judgement [8.059802912761919]
  我々は,大規模言語モデル(LLM)が自然言語要求にマッチするコードの体系的失敗を明らかにする。 より詳細なプロンプト設計、特に説明や修正提案を必要とするものは、より高い誤判定率をもたらす。 そこで本稿では,提案した修正を実効的証拠として扱う固定誘導検証フィルタを提案する。
  論文  参考訳（メタデータ） (2026-02-28T08:35:25Z)
• Evaluating and Achieving Controllable Code Completion in Code LLM [89.64782747840225]
  命令誘導型コード補完ベンチマークである制御可能コード補完ベンチマーク(C3-Bench)を提案する。 コード補完作業中に,オープンソースのプロプライエタリモデルと高度なプロプライエタリモデルの間に,命令追従機能にかなりのギャップがあることを明らかにする。 結果として得られたQwen2.5-Coder-C3は、C3-Bench上で最先端のパフォーマンスを達成する。
  論文  参考訳（メタデータ） (2026-01-22T11:40:04Z)
• 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)
• CodeIF: Benchmarking the Instruction-Following Capabilities of Large Language Models for Code Generation [20.013757490442064]
  タスク指向の命令に準拠する大規模言語モデル(LLM)の能力を評価するために設計された最初のベンチマークであるCodeIFを紹介する。 CodeIFは関数合成、アルゴリズム命令、コード説明など幅広いタスクを含んでいる。 我々はLLMによる広範囲な実験を行い、これらの課題の要求を満たす上での強みと限界を分析した。
  論文  参考訳（メタデータ） (2025-02-26T14:19:49Z)

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

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