DafnyBench

Dafnybench：正式軟件驗證的基準

我們的論文Dafnybench的數據集和代碼：正式軟件驗證的基準

數據集也可以下載嗎？擁抱臉。

概述

Dafnybench是培訓和評估機器學習系統的最大基準，用於正式軟件驗證，擁有750多個DAFNY程序。

用法

• 數據集：DAFNYBENCH的數據集（帶有782個程序）可以在DafnyBench目錄中找到，該目錄包含ground_truth set＆ hints_removed set（帶有編譯器提示，即annoataions，eman effecter，刪除）。
• 評估：通過要求模型填充來自hints_removed set的測試文件中缺失的提示並檢查是否可以通過dafny驗證重建程序中的測試文件中的丟失提示，從而評估LLM。請參考eval目錄。

設置進行評估？

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程序的集合。每個程序都有一個ground_truth版本，該版本已通過dafny＆a hints_removed版本進行了完全驗證，該版本已刪除提示（IE註釋）
• 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 }
}