DafnyBench

Dafnybench：正式なソフトウェア検証のベンチマーク

私たちの論文のデータセットとコードdafnybench：正式なソフトウェア検証のためのベンチマーク

データセットはダウンロードできますか？顔を抱き締める。

概要

Dafnybenchは、750を超えるDAFNYプログラムを備えた、正式なソフトウェア検証のための機械学習システムのトレーニングと評価のための最大のベンチマークです。

使用法

• データセット：Dafnybenchのデータセット（782プログラム付き）は、 ground_truthセットとhints_removedセット（コンパイラヒント、つまりAnnoataions、削除）を含むDafnyBenchディレクトリにあります。
• 評価： hints_removedセットのテストファイルに不足しているヒントを記入し、再構成されたプログラムをDAFNYによって検証できるかどうかを確認するように、モデルにモデルに不足しているヒントを入力するように依頼することにより、dafnybenchのLLMSを評価します。 eval Directoryを参照してください。

評価のために設定しますか？

1. このチュートリアルに従って、マシンにDAFNYをインストールします
2. このリポジトリにクローンとcd
3. 次の行を実行して環境を設定します。

 python -m venv stats
source stats/bin/activate
pip install -r requirements.txt
cd eval

4. ルートディレクトリの環境変数を設定します。

 export DAFNYBENCH_ROOT=

5. マシン上のdafny実行可能ファイルへのパスの環境変数を設定します（たとえば、 /opt/homebrew/bin/Dafny ）：

 export DAFNY_PATH=

6. APIアクセスを介してLLMを評価している場合は、APIキーを設定します。例えば：

 export OPENAI_API_KEY=

7. 次のような単一のテストプログラムでLLMを評価することを選択できます。

 python fill_hints.py --model "gpt-4o" --test_file "Clover_abs_no_hints.dfy" --feedback_turn 3 --dafny_path "$DAFNY_PATH"

または、データセット全体で評価します。

 export model_to_eval='gpt-4o'
./run_eval.sh

コンテンツ ？

• DafnyBench
  • 782のDAFNYプログラムのコレクション。各プログラムには、dafny＆a hints_removedバージョンで完全に検証されたground_truthバージョンがあります（つまり、注釈）削除されました
• eval
  • dafnybenchでLLMを評価するスクリプトが含まれています
• results
  • results_summaryすべてのテストプログラムでLLMSの成功を要約するデータフレーム
  • reconstructed_files -LLM出力は、ヒントが満たされた状態で出力されます
  • analysis - 結果を分析するためのノートブックが含まれています

引用？

 @article { loughridge2024dafnybench ,
         title = { DafnyBench: A Benchmark for Formal Software Verification } , 
         author = { Chloe Loughridge and Qinyi Sun and Seth Ahrenbach and Federico Cassano and Chuyue Sun and Ying Sheng and Anish Mudide and Md Rakib Hossain Misu and Nada Amin and Max Tegmark } ,
         year = { 2024 } ,
         journal = { arXiv preprint arXiv:2406.08467 }
}