Elamur Research⌕
☰
home / papers / 2024 / DafnyBench: A Benchmark for Formal Software Verification

DafnyBench: A Benchmark for Formal Software Verification

Paper · 2024 · Chloe Loughridge, Qinyi Sun, Seth Ahrenbach et al.

Summary

Formal verification can mathematically guarantee that code meets its specification, but it demands a lot of expert effort. The authors argue that AI could automate this work, as it has for theorem proving. Progress, however, is held back by a lack of training and evaluation data: before this work, the largest benchmarks, Clover and dafny-synthesis, held only a few hundred programs combined. DafnyBench addresses this gap with 782 standalone Dafny programs (about 53,000 lines) drawn from deduplicated GitHub code, Clover and dafny-synthesis.

The main task, fill_hints, removes every assert and invariant annotation and asks an LLM to restore enough hints for the Dafny verifier to succeed. The model may not alter preconditions or postconditions or disable verification. Claude 3 Opus achieved the best result at roughly 68%. Feedback from error messages brought only modest gains, and success fell as programs got longer. The benchmark offers a much larger and harder baseline for measuring how well AI can verify software.

Key points

  • Dataset composition: 556 programs come from GitHub, 62 from Clover and 164 from dafny-synthesis.

    • The GitHub portion started from about 15,000 files, which shrank to about 5,000 after minhash deduplication.
    • Only files that verified under Dafny 4.3.0 and contained ensures, assert or invariant clauses were kept.

  • Program complexity: On average, each program has 2.12 methods, 1.03 functions and 1.40 lemmas, so it is more complex than Clover's single-method examples.

  • Success rates with up to 10 attempts (temperature 0.3):

    ModelSuccess
    Claude 3 Opus67.8%
    GPT-4 Turbo59.8%
    GPT-4o59.3%
    GPT-3.5 Turbo44.0%
    CodeLlama-7b-Instruct-hf28.0%
    No-LLM baseline (Dafny verifies without hints)26.9%

  • Effect of retries: The best models solved about 54% of programs on the first attempt. Retries with error feedback levelled off near 65% after roughly five attempts, which suggests models make limited use of Dafny's error messages.

  • Validity rules: An attempt fails if it modifies requires/ensures statements or uses {:verify false} or assume false. To avoid data contamination, models should not be trained on the GitHub repositories listed in the paper.

Our summary of the paper, in our own words — not its text. The work belongs to its authors; read it at the links above.

 Institutions

🎓Stanford UniversityStanford · United States567 works · 335,189 citations🎓Massachusetts Institute of TechnologyCambridge · United States274 works · 82,013 citations🎓Harvard UniversityCambridge · United States137 works · 45,850 citations🎓Northeastern UniversityBoston · United States70 works · 7,342 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksComputational Theory and Mathematics · 496 worksSoftware · 150 works

🧭 Topics 2Research subjects and languages the work is about.Reasoning · 1,948 worksEvaluation & benchmarks · 1,394 works

Cite

Cite as Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin and Max Tegmark. 2024. DafnyBench: A Benchmark for Formal Software Verification. arXiv:2406.08467.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.48550/arxiv.2406.08467 · arXiv 2406.08467

@misc{loughridge2024dafnybench,
  title = {{DafnyBench: A Benchmark for Formal Software Verification}},
  author = {Chloe Loughridge, Qinyi Sun, Seth Ahrenbach, Federico Cassano, Chuyue Sun, Ying Sheng, Anish Mudide, Md Rakib Hossain Misu, Nada Amin and Max Tegmark},
  year = {2024},
  doi = {10.48550/arxiv.2406.08467},
  eprint = {2406.08467},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2406.08467}
}

References

41 references, 17 of them with a card of ours. ↗ leads to the work, «find» searches for one we have no id for yet.

  1. Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, et al. Sparks of artificial general intelligence: Early experiments with gpt-4. arXiv preprint arXiv:2303.12712, 2023.
  2. Anthropic. The claude 3 model family: Opus, sonnet, haiku. Technical report, Anthropic, 2024. find
  3. Gemini Team, Rohan Anil, Sebastian Borgeaud, Yonghui Wu, Jean-Baptiste Alayrac, Jiahui Yu, Radu Soricut, Johan Schalkwyk, Andrew M Dai, Anja Hauth, et al. Gemini: a family of highly capable multimodal models. arXiv preprint arXiv:2312.11805, 2023.
  4. European Space Agency. Flight 501 failure, 1996. URL https://esamultimedia.esa.int/docs/esa-x-1819eng.pdf. Accessed: 2024-06-04. ↗
  5. Heartbleed. The heartbleed bug. https://heartbleed.com/, 2024. Accessed: 2024-06-04. ↗
  6. Wikipedia contributors. Shellshock (software bug). https://en.wikipedia.org/wiki/ Shellshock_(software_bug), 2024. Accessed: 2024-06-04. ↗
  7. Stanislas Polu and Ilya Sutskever. Generative Language Modeling for Automated Theorem Proving. arXiv, September 2020. doi: 10.48550/arXiv.2009.03393.
  8. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. HyperTree Proof Search for Neural Theorem Proving. arXiv, May 2022. doi: 10.48550/arXiv.2205.11491.
  9. Chuyue Sun, Ying Sheng, Oded Padon, and Clark Barrett. Clover: Closed-loop verifiable code generation. In ICLR 2024 Conference, 2024. URL https://openreview.net/forum?id= oSuVEv4X7w. ↗
  10. Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma, and James Noble. Towards ai-assisted synthesis of verified dafny methods. Proc. ACM Softw. Eng., 1(FSE), 2024. doi: 10.1145/ 3643763. URL https://doi.org/10.1145/3643763. ↗
  11. K Rustan M Leino. Program Proofs. MIT Press, 2023. find
  12. Kaiyu Yang and Jia Deng. Learning to prove theorems via interacting with proof assistants, 2019.
  13. Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar. Leandojo: Theorem proving with retrieval-augmented language models, 2023.
  14. Pisa: Isabelle proofs dataset. https://aitp-conference.org/2021/abstract/paper_ 17.pdf, 2021. ↗
  15. Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, and Kyunghyun Cho. Naturalproofs: Mathematical theorem proving in natural language. In Thirty-fifth Conference on Neural Information Processing Systems Datasets and Benchmarks Track (Round 1), 2021. URL https://openreview.ne… ↗
  16. Jasmin Christian Blanchette, Maximilian Haslbeck, Daniel Matichuk, and Tobias Nipkow. Mining the archive of formal proofs. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, pages 3–17, Cham, 2015. Springer International Pu… find
  17. Dan Hendrycks, Steven Basart, Saurav Kadavath, Mantas Mazeika, Akul Arora, Ethan Guo, Collin Burns, Samir Puranik, Horace He, Dawn Song, and Jacob Steinhardt. Measuring coding challenge competence with apps. arXiv preprint arXiv:2105.09938, 2021.
  18. Qinkai Zheng, Xiao Xia, Xu Zou, Yuxiao Dong, Shan Wang, Yufei Xue, Zihan Wang, Lei Shen, Andi Wang, Yang Li, Teng Su, Zhilin Yang, and Jie Tang. Codegeex: A pre-trained model for code generation with multilingual evaluations on humaneval-x, 2023. find
  19. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harri Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, et al. Evaluating large language models trained on code, 2021.
  20. Jacob Austin, Augustus Odena, Maxwell Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie Cai, Michael Terry, Quoc Le, and Charles Sutton. Program synthesis with large language models, 2021.
  21. Carlos E. Jimenez, John Yang, Alexander Wettig, Shunyu Yao, Kexin Pei, Ofir Press, Karthik Narasimhan, et al. Swe-bench: Can language models resolve real-world github issues?, 2023.
  22. Naman Jain, King Han, Alex Gu, Wen-Ding Li, Fanjia Yan, Tianjun Zhang, Sida Wang, Armando Solar-Lezama, Koushik Sen, and Ion Stoica. Livecodebench: Holistic and contamination free evaluation of large language models for code. arXiv preprint, 2024.
  23. OpenAI, Josh Achiam, Steven Adler, Sandhini Agarwal, Lama Ahmad, Ilge Akkaya, Florencia Leoni Aleman, Diogo Almeida, Janko Altenschmidt, Sam Altman, Shyamal Anadkat, Red Avila, Igor Babuschkin, Suchir Balaji, Valerie Balcom, Paul Baltescu, Haiming Bao, Mohammad Bavarian, Jeff Belgum, Irwan Bello, Ja… — GPT-4 Technical Report
  24. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — Language Models are Few-Shot Learners
  25. Code llama: Fine-tuning llama for code generation. https://huggingface.co/Phind/ Phind-CodeLlama-34B-v2, 2022. ↗
  26. Steve Klabnik and with contributions from the Rust Community Carol Nichols. The Rust Programming Language. No Starch Press, second edition, 2021. URL https://doc.rust-lang.org/stable/book/. ↗
  27. XAI-ORG. Grok-1 Model on Hugging Face. https://huggingface.co/xai-org/grok-1, 2024. Accessed: 2024-06-05. ↗
  28. David Brandfonbrener, Sibi Raja, Tarun Prasad, Chloe Loughridge, Federico Cassano, Jianang Yang, Simon Henniger, William E. Byrd, Robert Zinkov, and Nada Amin. Verified multi-step synthesis using large language models and monte carlo tree search, 2023. find
  29. Zhaoyu Li, Jialiang Sun, Logan Murphy, Qidong Su, Zenan Li, Xian Zhang, Kaiyu Yang, and Xujie Si. A survey on deep learning for theorem proving. arXiv preprint arXiv:2404.09939, 2024.
  30. Sandrine Blazy and Xavier Leroy. Mechanized semantics for the Clight subset of the C language. Journal of Automated Reasoning, 43(3):263–288, 2009. URL http://xavierleroy.org/ publi/Clight.pdf. ↗
  31. Nicholas D Matsakis and Felix S Klock II. The rust language. In ACM SIGAda Ada Letters, volume 34, pages 103–104. ACM, 2014. find
  32. The Coq Development Team. The Coq reference manual – release 8.19.0. https://coq.inria.fr/doc/V8.19.0/refman, 2024. ↗
  33. DANIL ANNENKOV, MIKKEL MILO, JAKOB BOTSCH NIELSEN, and BAS SPITTERS. Extracting functional programs from Coq, in Coq. Journal of Functional Programming, 32:e11, 2022. doi: 10.1017/S0956796822000077. — [doi:10.1017/s0956796822000077](https://doi.org/10.1017/s0956796822000077) find
  34. Design Automation Standards Committee and Automatic Test Program Generation Subcommittee. Ieee standard for vhdl language reference manual. IEEE Std 1076-2019, pages 1–673, 2019. doi: 10.1109/IEEESTD.2019.8938196. — [doi:10.1109/ieeestd.2019.8938196](https://doi.org/10.1109/ieeestd.2019.8938196) find
  35. Donald Thomas and Philip Moorby. The Verilog Hardware Description Language. Springer Publishing Company, Incorporated, 5th ed. edition, 2008. ISBN 0387849300. find
  36. Adam Procter, William L. Harrison, Ian Graves, Michela Becchi, and Gerard Allwein. Semantics driven hardware design, implementation, and verification with rewire. In Proceedings of the 16th ACM SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems 2015 CD-ROM, LCTES’15, Ne… — [doi:10.1145/2670529.2754970](https://doi.org/10.1145/2670529.2754970) find
  37. Xun Li, Mohit Tiwari, Jason K. Oberg, Vineeth Kashyap, Frederic T. Chong, Timothy Sherwood, and Ben Hardekopf. Caisson: a hardware description language for secure information flow. In Proceedings of the 32nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’11, page 109… — [doi:10.1145/1993498.1993512](https://doi.org/10.1145/1993498.1993512) find
  38. Wikipedia contributors. Jaccard index — wikipedia, the free encyclopedia. https://en.wikipedia.org/wiki/Jaccard_index, 2024. Accessed: 2024-03-27. ↗
  39. Wikipedia contributors. N-gram — Wikipedia, the free encyclopedia. wikipedia.org/wiki/N-gram, 2024. Accessed: 2024-03-27. https://en. find
  40. Chenghao Mou, Chris Ha, Kenneth Enevoldsen, and Peiyuan Liu. Chenghaomou/text-dedup: Reference snapshot, September 2023. URL https://doi.org/10.5281/zenodo.8364980. — [doi:10.5281/zenodo.8364980](https://doi.org/10.5281/zenodo.8364980) ↗
  41. Lianmin Zheng, Liangsheng Yin, Zhiqiang Xie, Jeff Huang, Chuyue Sun, Cody Hao Yu, Shiyi Cao, Christos Kozyrakis, Ion Stoica, Joseph E. Gonzalez, Clark Barrett, and Ying Sheng. Efficiently programming large language models using sglang, 2023. find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/loughridge-2024-dafnybench-benchmark-formal-software-verification/