DafnyBench：形式化软件验证基准

Chloe Loughridge; Qinyi Sun; Seth Ahrenbach; Federico Cassano; Chuyue Sun; Ying Sheng; Anish Mudide; Md Rakib Hossain Misu; Nada Amin; Max Tegmark

DafnyBench：形式化软件验证基准

软件工程 2024-06-13 v1 人工智能机器学习编程语言

作者: Chloe Loughridge , Qinyi Sun , Seth Ahrenbach , Federico Cassano , Chuyue Sun , Ying Sheng , Anish Mudide , Md Rakib Hossain Misu , Nada Amin , Max Tegmark

在 arXiv 上查看 ↗ PDF ↗

摘要

我们介绍了DafnyBench，这是同类中最大的基准，用于训练和评估机器学习系统以进行形式化软件验证。我们测试了GPT-4和Claude 3等LLM自动生成足够提示的能力，以使Dafny形式化验证引擎成功验证超过750个程序（约53,000行代码）。最佳模型和提示方案实现了68%的成功率，我们量化了在重试并带有错误消息反馈时该率如何提高，以及随着所需代码和提示数量的增加该率如何下降。我们希望随着LLM和验证技术质量的提高，DafnyBench能够从这一基线实现快速改进。

关键词

形式化验证 Dafny 基准大型语言模型程序合成软件验证

引用

@article{arxiv.2406.08467,
  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},
  journal= {arXiv preprint arXiv:2406.08467},
  year   = {2024}
}

备注

Code & dataset available at: https://github.com/sun-wendy/DafnyBench

DafnyBench：形式化软件验证基准

摘要

关键词

引用

备注

相关论文