論文の概要: A benchmark for vericoding: formally verified program synthesis

• arxiv url: http://arxiv.org/abs/2509.22908v1
• Date: Fri, 26 Sep 2025 20:36:20 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-30 22:32:18.932361
• Title: A benchmark for vericoding: formally verified program synthesis
• Title（参考訳）: 検証のためのベンチマーク:公式に検証されたプログラム合成
• Authors: Sergiu Bursuc, Theodore Ehrenborg, Shaowei Lin, Lacramioara Astefanoaei, Ionel Emilian Chiosa, Jure Kukovec, Alok Singh, Oliver Butterley, Adem Bizid, Quinn Dougherty, Miranda Zhao, Max Tan, Max Tegmark,
• Abstract要約: 私たちのベンチマークには12,504の正式な仕様が含まれており、Dafnyでは3,029、Verus/Rustでは2,334、Leanでは7,141です。 私たちは、リーンで27%、Verus/Rustで44%、Dafnyで82%のベリコード成功率を、既製のLLMを使っています。
• 参考スコア（独自算出の注目度）: 7.230309487789833
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark
• Abstract（参考訳）: 我々は,形式的な仕様から検証済みのコードを生成する,検証のための最大のベンチマークを提示し,テストする。 私たちのベンチマークには12,504の正式な仕様が含まれており、Dafnyでは3,029、Verus/Rustでは2,334、Leanでは7,141です。 これらのうち、6,174は目に見えない新しい問題である。 私たちは、リーンで27%、Verus/Rustで44%、Dafnyで82%のベリコード成功率を、既製のLLMを使っています。 自然言語記述を追加することでパフォーマンスが大幅に向上するわけではない。 LLMの進歩は、過去1年間で純粋なDafny検証の進歩を68%から96%に改善した。 ベンチマークと検証結果はhttps://github.com/Beneficial-AI-Foundation/vericoding-benchmarkで共有される。

関連論文リスト

• NoCode-bench: A Benchmark for Evaluating Natural Language-Driven Feature Addition [16.134058143793304]
  この研究は、現実世界のNL駆動機能追加タスクで大きな言語モデル(LLM)を評価するために設計されたベンチマークであるNoCode-benchを紹介する。 高品質で人間認証された114のインスタンスのサブセット、NoCode-bench Verifiedは信頼性の高い評価を保証する。 我々の実験によると、トークンの使用率が高いにもかかわらず、最高のLCMはタスク成功率28.07%しか達成せず、クロスファイル編集、理解、ツール呼び出しの課題を強調している。
  論文  参考訳（メタデータ） (2025-07-24T06:38:19Z)
• VERINA: Benchmarking Verifiable Code Generation [47.9771074559674]
  大規模言語モデル(LLM)は、ソフトウェア開発にますます統合されている。 検証可能なコード生成は、この制限に対処するための有望なパスを提供する。 現在のベンチマークでは、エンドツーエンドの検証可能なコード生成がサポートされていないことが多い。
  論文  参考訳（メタデータ） (2025-05-29T06:12:52Z)
• Evaluating Large Language Models for Code Review [2.0261749670612637]
  GPT4oとGemini 2.0 Flashを492 AIでテストしました。 GPT4o と Gemini 2.0 Flash はそれぞれ68.50% と63.89% のコード正当性を正しく分類し、67.83% と54.26% のコード正当性を修正した。
  論文  参考訳（メタデータ） (2025-05-26T16:47:29Z)
• How Should We Build A Benchmark? Revisiting 274 Code-Related Benchmarks For LLMs [60.25940747590386]
  本稿では,コード関連ベンチマークの開発を包括的に管理するためのガイドラインとして,55の基準チェックリストからなるHow2Benchを提案する。 私たちは過去10年以内にリリースされた274のベンチマークをプロファイルし、問題を見つけました。 ベンチマークの70%近くはデータ品質保証の措置を取らず、10%以上がオープンソースでも、部分的にはオープンソースでもなかった。
  論文  参考訳（メタデータ） (2025-01-18T09:51:57Z)
• Inference-Time Decontamination: Reusing Leaked Benchmarks for Large Language Model Evaluation [61.350306618479365]
  ベンチマークの漏洩は、大規模言語モデルの真のパフォーマンスの正確な評価を防ぐことができる。 この問題に対処するため,ITD(Inference-Time Decontamination)を提案する。 ITDは、GSM8Kで22.9%、MMLUで19.0%の膨張精度を低下させる。
  論文  参考訳（メタデータ） (2024-06-20T04:35:59Z)
• DafnyBench: A Benchmark for Formal Software Verification [5.369797450356865]
  DafnyBenchは、正式なソフトウェア検証のための機械学習システムのトレーニングと評価のための、同社のタイプの最大のベンチマークである。 我々は,GPT-4 や Claude 3 などの LLM を用いて,約 53,000 行のコードで 750 以上のプログラムを検証できるように,Dafny 形式検証エンジンに十分なヒントを自動生成する機能をテストする。
  論文  参考訳（メタデータ） (2024-06-12T17:53:31Z)
• LEVER: Learning to Verify Language-to-Code Generation with Execution [64.36459105535]
  本稿では,プログラムの実行結果の検証を学習することで,言語からコードへの生成を改善するシンプルな手法であるLEVERを提案する。 具体的には、LLMからサンプリングされたプログラムが、自然言語入力、プログラム自体とその実行結果に基づいて正しいか否かを判定するために、検証者を訓練する。 LEVER はベースコード LLMs (4.6% から 10.9% まで) を継続的に改善し、それらすべてに対して新しい最先端の結果を得る。
  論文  参考訳（メタデータ） (2023-02-16T18:23:22Z)

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

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