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 }
}