論文の概要: DafnyBench: A Benchmark for Formal Software Verification

• arxiv url: http://arxiv.org/abs/2406.08467v1
• Date: Wed, 12 Jun 2024 17:53:31 GMT
• ステータス: 処理完了
• システム内更新日: 2024-06-13 15:27:35.128374
• Title: DafnyBench: A Benchmark for Formal Software Verification
• Title（参考訳）: DafnyBench: 形式的ソフトウェア検証のためのベンチマーク
• Authors: Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin, Max Tegmark,
• Abstract要約: DafnyBenchは、正式なソフトウェア検証のための機械学習システムのトレーニングと評価のための、同社のタイプの最大のベンチマークである。 我々は,GPT-4 や Claude 3 などの LLM を用いて,約 53,000 行のコードで 750 以上のプログラムを検証できるように,Dafny 形式検証エンジンに十分なヒントを自動生成する機能をテストする。
• 参考スコア（独自算出の注目度）: 5.369797450356865
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We introduce DafnyBench, the largest benchmark of its kind for training and evaluating machine learning systems for formal software verification. We test the ability of LLMs such as GPT-4 and Claude 3 to auto-generate enough hints for the Dafny formal verification engine to successfully verify over 750 programs with about 53,000 lines of code. The best model and prompting scheme achieved 68% success rate, and we quantify how this rate improves when retrying with error message feedback and how it deteriorates with the amount of required code and hints. We hope that DafnyBench will enable rapid improvements from this baseline as LLMs and verification techniques grow in quality.
• Abstract（参考訳）: DafnyBenchは、正式なソフトウェア検証のための機械学習システムのトレーニングと評価のための、そのタイプの最大のベンチマークである。 我々は,GPT-4 や Claude 3 などの LLM を用いて,約 53,000 行のコードで 750 以上のプログラムを検証できるように,Dafny 形式検証エンジンに十分なヒントを自動生成する機能をテストする。 最良のモデルとプロンプトスキームは68%の成功率を達成し、エラーメッセージのフィードバックで再試行した場合にどのように改善するか、必要なコードやヒントの量でどのように悪化するかを定量化する。 DafnyBenchは、LLMと検証技術の品質が向上するにつれて、このベースラインから迅速に改善できることを期待しています。

関連論文リスト

• Verifying LLM-Generated Code in the Context of Software Verification with Ada/SPARK [0.4143603294943439]
  大規模言語モデル(LLM)は、顕著なコード生成能力を示しているが、生成されたコードの正確性は本質的に信頼できない。 本稿では,ALM生成コードの信頼性を確保するために,形式的ソフトウェア検証,特にAdaのSPARKフレームワークを使用することの実現可能性について検討する。 本稿では,既存のプログラムのSPARKアノテーションを生成するためにLLMを利用するツールであるMarmaraganについて述べる。
  論文  参考訳（メタデータ） (2025-02-11T17:42:07Z)
• Proving the Coding Interview: A Benchmark for Formally Verified Code Generation [3.5319285228327417]
  FVAPPS (Formally Verified Automated Programming Progress Standards, FVAPPS) は,プログラムの記述と正確性を証明するための4715サンプルのベンチマークである。 我々は,機械学習とプログラム合成コミュニティに対して,汎用プログラミング問題とその関連した正当性仕様の解決に挑戦する。
  論文  参考訳（メタデータ） (2025-02-08T22:54:58Z)
• PerfCodeGen: Improving Performance of LLM Generated Code with Execution Feedback [78.89596149768458]
  大規模言語モデル(LLM)は、ソフトウェア開発タスクを支援するために広く採用されている。 LLM生成コードの性能を向上させるトレーニングフリーフレームワークPerfCodeGenを提案する。
  論文  参考訳（メタデータ） (2024-11-18T06:22:38Z)
• dafny-annotator: AI-Assisted Verification of Dafny Programs [4.651620941143133]
  本稿では,大言語モデルと検索を組み合わせたダファニーアノテーションの構築について検討する。 DafnyBench プログラムのコレクションから得られたテストセットでは、LLaMa 3.1 8B でガイドされたgreedy search が15.7%のメソッドに注釈を付けることに成功した。 我々の結果は、大規模な人為的な例がまだない言語のための有能なAIアシスタントへの道のりを示唆している。
  論文  参考訳（メタデータ） (2024-11-05T19:27:56Z)
• Revisiting VerilogEval: A Year of Improvements in Large-Language Models for Hardware Code Generation [6.463959200930805]
  オープンソースのVerilogEvalベンチマークのリリース以降,新しい商用およびオープンなモデルを評価する。 最先端のモデルでは測定可能な改善が得られます。 高いパスレートを達成するためには、迅速なエンジニアリングが不可欠であることに気付きました。
  論文  参考訳（メタデータ） (2024-08-20T17:58:56Z)
• FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Proving [53.43068330741449]
  大規模言語モデル(LLM)を用いた対話型形式検証環境FVELを提案する。 FVELは、検証対象のコードをIsabelleに変換し、LLMで証明された神経自動定理を用いて検証を行う。 FVELERデータセットには、Isabelleで定式化されたコード依存関係と検証プロセスが含まれており、758の理論、29,125のレムマ、200,646の証明ステップが含まれている。
  論文  参考訳（メタデータ） (2024-06-20T15:31:05Z)
• Self-play with Execution Feedback: Improving Instruction-following Capabilities of Large Language Models [54.14602121129874]
  トレーニングデータを自動的に生成する最初のスケーラブルで信頼性の高いAutoIFを導入する。 AutoIFは命令追従データ品質の検証をコード検証に変換する。
  論文  参考訳（メタデータ） (2024-06-19T13:29:53Z)
• 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)
• Code Prompting Elicits Conditional Reasoning Abilities in Text+Code LLMs [65.2379940117181]
  自然言語の問題をコードに変換する一連のプロンプトであるコードプロンプトを導入します。 コードプロンプトは複数のLLMに対して高速に向上することがわかった。 GPT 3.5を解析した結果,入力問題のコードフォーマッティングが性能向上に不可欠であることが判明した。
  論文  参考訳（メタデータ） (2024-01-18T15:32:24Z)
• Factcheck-Bench: Fine-Grained Evaluation Benchmark for Automatic Fact-checkers [121.53749383203792]
  本稿では,大規模言語モデル (LLM) 生成応答の事実性に注釈を付けるための総合的なエンドツーエンドソリューションを提案する。 オープンドメインの文書レベルの事実性ベンチマークを,クレーム,文,文書の3段階の粒度で構築する。 予備実験によると、FacTool、FactScore、Perplexityは虚偽の主張を識別するのに苦労している。
  論文  参考訳（メタデータ） (2023-11-15T14:41:57Z)

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

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