論文の概要: VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code

• arxiv url: http://arxiv.org/abs/2510.06296v1
• Date: Tue, 07 Oct 2025 13:19:05 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-10-09 16:41:20.107241
• Title: VeriEquivBench: An Equivalence Score for Ground-Truth-Free Evaluation of Formally Verifiable Code
• Title（参考訳）: VeriEquivBench: 形式的検証可能なコードの地平自由評価のための等価スコア
• Authors: Lingfei Zeng, Fengdi Che, Xuhan Huang, Fei Ye, Xu Xu, Binhang Yuan, Jie Fu,
• Abstract要約: 我々は,Large Language Models (LLM) の形式的検証のための新しいベンチマークを導入する。 筆者らのフレームワークは, 基調整合を定式化された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。 以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。
• 参考スコア（独自算出の注目度）: 25.916111156888235
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Formal verification is the next frontier for ensuring the correctness of code generated by Large Language Models (LLMs). While methods that co-generate code and formal specifications in formal languages, like Dafny, can, in principle, prove alignment with user intent, progress is bottlenecked by specification quality evaluation. Current benchmarks rely on matching against ground-truth specifications, a manual and expertise-intensive process that has limited existing datasets to a few hundred simple problems and also suffers from a reliability issue. To address this, we introduce VeriEquivBench, a new benchmark with $2,389$ complex algorithmic problems that probe the limitations of current models in both code generation and formal reasoning. Our evaluation framework replaces ground-truth matching with a formally grounded metric, the equivalence score, and rigorously verifies the quality of generated specifications and code. Our results show that generating formally verifiable code remains a profound challenge for state-of-the-art LLMs. This underscores both the difficulty of the task and the need for benchmarks like VeriEquivBench to drive progress toward scalable and reliable coding agents.
• Abstract（参考訳）: 形式検証は、Large Language Models (LLM) が生成するコードの正しさを保証するための次のフロンティアである。 Dafnyのようなフォーマルな言語でコードと公式な仕様を共同生成するメソッドは、原則としてユーザ意図と整合性を証明できますが、仕様の品質評価によって進歩がボトルネックになります。 既存のデータセットを数百の単純な問題に制限し、信頼性の問題も抱えている。 これを解決するために、コード生成と形式的推論の両方における現在のモデルの限界を探索する、2389ドルの複雑なアルゴリズム問題を持つ新しいベンチマークであるVeriEquivBenchを紹介した。 評価の枠組みは, 接地された基準, 等価スコアに置き換え, 生成された仕様やコードの品質を厳格に検証する。 以上の結果から,形式的検証可能なコードを生成することは,最先端のLLMにとって依然として大きな課題であることがわかった。 このことは、タスクの難しさとVeriEquivBenchのようなベンチマークが、スケーラブルで信頼性の高いコーディングエージェントへの進歩を促進する必要性の両方を浮き彫りにしている。

関連論文リスト

• Scaling Code-Assisted Chain-of-Thoughts and Instructions for Model Reasoning [65.20602712957725]
  Cacoは、高品質で検証可能な多様な命令-CoT推論データの合成を自動化する新しいフレームワークである。 我々の研究は、人間の介入なしに自己持続的で信頼できる推論システムを構築するためのパラダイムを確立します。
  論文  参考訳（メタデータ） (2025-10-05T07:59:24Z)
• Taming Imperfect Process Verifiers: A Sampling Perspective on Backtracking [54.43083499412643]
  言語モデルの生成能力をプロセス検証器と組み合わせたテストタイムアルゴリズムは、新しい推論能力を引き出すための有望なレバーを提供する。 提案手法は, 理論的に根拠付きバックトラックを用いて, 検証誤差に対して, 確実な堅牢性を実現するための新しいプロセス誘導型テスト時間サンプリングアルゴリズムであるVGBを導入する。
  論文  参考訳（メタデータ） (2025-10-03T16:21:14Z)
• CAAD: Context-Aware Adaptive Decoding for Truthful Text Generation [31.469511576774252]
  大規模言語モデルに対する文脈対応適応型復号法を提案する。 当社のアプローチは、TrathfulQAで平均2.8%の改善を実現しています。 モデルに依存しない,スケーラブルで,効率的な手法では,1世代パスしか必要としない。
  論文  参考訳（メタデータ） (2025-08-04T08:28:25Z)
• IFEvalCode: Controlled Code Generation [69.28317223249358]
  本稿では,Code LLMの命令追従能力を改善するために,前方および後方制約生成を提案する。 IFEvalCodeは、7つのプログラミング言語の1.6Kテストサンプルからなる多言語ベンチマークである。
  論文  参考訳（メタデータ） (2025-07-30T08:08:48Z)
• Re:Form -- Reducing Human Priors in Scalable Formal Software Verification with RL in LLMs: A Preliminary Study on Dafny [68.00108157244952]
  強化学習(RL)で訓練された大規模言語モデル(LLM)は、信頼性も拡張性もない、という大きな課題に直面している。 有望だが、ほとんど報われていない代替手段は、フォーマルな言語ベースの推論である。 生成モデルが形式言語空間(例えばダフニー)で機能する厳密な形式体系におけるLLMの接地は、それらの推論プロセスと結果の自動的かつ数学的に証明可能な検証を可能にする。
  論文  参考訳（メタデータ） (2025-07-22T08:13:01Z)
• VERINA: Benchmarking Verifiable Code Generation [47.9771074559674]
  大規模言語モデル(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)
• VEL: A Formally Verified Reasoner for OWL2 EL Profile [0.0]
  VEL はマシンチェック可能な正当性証明を備えた公式な EL++ 推論器である。 本研究は,理論および実装レベルでの正確性を確保するために,推論アルゴリズムの機械化の必要性を実証するものである。
  論文  参考訳（メタデータ） (2024-12-11T19:17:28Z)

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

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