CoChat
Sign Up
Cited by 42Logic, programming, and type systemsSoftware Engineering ResearchTeaching and Learning Programming

Towards AI-Assisted Synthesis of Verified Dafny Methods

Open access
Misu, Md Rakib Hossain, Lopes, Cristina V., Ma, Iris, Noble, James·2024·Proceedings of the ACM on Software Engineering
DOI 10.1145/3643763
Open this paper in CoChat — free accountOpen PDF

Abstract

Large language models show great promise in many domains, including programming. A promise is easy to make but hard to keep, and language models often fail to keep their promises, generating erroneous code. A promising avenue to keep models honest is to incorporate formal verification: generating programs’ specifications as well as code, so that the code can be proved correct with respect to the specifications. Unfortunately, existing large language models show a severe lack of proficiency in verified programming. In this paper, we demonstrate how to improve two pretrained models’ proficiency in the Dafny verification-aware language. Using 178 problems from the MBPP dataset, we prompt two contemporary models (GPT-4 and PaLM-2) to synthesize Dafny methods. We use three different types of prompts: a direct Contextless prompt; a Signature prompt that includes a method signature and test cases, and a Chain of Thought (CoT) prompt that decomposes the problem into steps and includes retrieval augmentation generated example problems and solutions. Our results show that GPT-4 performs better than PaLM-2 on these tasks, and that both models perform best with the retrieval augmentation generated CoT prompt. GPT-4 was able to generate verified, human-evaluated, Dafny methods for 58% of the problems, however GPT-4 managed only 19% of the problems with the Contextless prompt, and even fewer (10%) for the Signature prompt. We are thus able to contribute 153 verified Dafny solutions to MBPP problems, 50 that we wrote manually and 103 synthesized by GPT-4. Our results demonstrate that the benefits of formal program verification are now within reach of codegenerating large language models. Likewise, program verification systems can benefit from large language models, whether to synthesize code wholesale, to generate specifications, or to act as a “programmer’s verification apprentice”, to construct annotations such as loop invariants which are hard for programmers to write or verification tools to find. Finally, we expect that the approach we have pioneered here — generating candidate solutions that are subsequently formally checked for correctness — should transfer to other domains (e.g., legal arguments, transport signaling, structural engineering) where solutions must be correct, where that correctness must be demonstrated, explained and understood by designers and end-users.

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Integrity signals

Registry

Crossref · 10.1145/3643763

Cites

61 of 61 references verified0 citation errors · 0 not checkable

Statistics

Claims the paper makes

The claims and statistics of this paper haven’t been checked yet.

Run the check — free, no account needed. It reads the open-access text and checks the sources it cites.

A few free checks a day · papers already verified open instantly · results are public

Claims other papers make about this one

Each is checked against this paper’s own text: does it say what the citing paper says it does?

  • MBPP-verified contains 78 programs from the original MBPP dataset.

    “In particular, MBPP -verified is sourced from (Yang et al., 2024;Misu et al., 2024) and contains 78 programs from the original MBPP dataset (Austin et al., 2021).”

    From AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinement (2024) · cites this paper as Misu et al., 2024

    Section 3.1 identifies the paper’s dataset as derived from MBPP, supporting the claimed MBPP origin. But it calls that dataset MBPP-san-DFY and reports 178 test problems; section 3.2 reports 50 human-written verified problems. Our copy does not identify an MBPP-verified dataset containing 78 programs. (LLM, conf=0.84)

    Experimental — accuracy not yet measured

Self-check

Percentages, sums and reported differences re-computed from the paper’s own numbers.

The self-check needs the paper’s full text.

Cites

Flagged first, then by citations

Research works printed but not linked: 33

  1. Aakanksha Chowdhery et al. 2022. PaLM: Scaling Language Modeling with Pathways. CoRR abs/2204.02311 (2022). · arXiv
  2. Miltiadis Allamanis, Earl T. Barr, Premkumar T. Devanbu, and Charles Sutton. 2018. A Survey of Machine Learning for Big Code and Naturalness. ACM Comput. Surv. 51, 4 (2018), 81:1-81:37. https://doi.org/10.1145/3212695 · DOI · Paper page
  3. Jacob Austin, Augustus Odena, Maxwell I. Nye, Maarten Bosma, Henryk Michalewski, David Dohan, Ellen Jiang, Carrie J. Cai, Michael Terry, Quoc V. Le, and Charles Sutton. 2021. Program Synthesis with Large Language Models. CoRR abs/2108.07732 (2021). https://arxiv.org/abs/2108.07732 · arXiv
  4. Stephen H. Bach, Victor Sanh, Zheng Xin Yong, Albert Webson, Colin Raffel, Nihal V. Nayak, Abheesht Sharma, Taewoon Kim, M. Saiful Bari, Thibault Févry, Zaid Alyafeai, Manan Dey, Andrea Santilli, Zhiqing Sun, Srulik Ben-David, Canwen Xu, Gunjan Chhablani, Han Wang, Jason Alan Fries, Maged Saeed AlShaibani, Shanya Sharma, Urmish Thakker, Khalid Almubarak, Xiangru Tang, Dragomir R. Radev, Mike Tian-Jian Jiang, and Alexander M. Rush. 2022. PromptSource: An Integrated Development Environment and Repository for Natural Language Prompts. In Proceedings of the 60th Annual Meeting of the Association for Computational Linguistics, ACL 2022 -System Demonstrations, Dublin, Ireland, May 22-27, 2022, Valerio Basile, Zornitsa Kozareva, and Sanja Stajner (Eds.). Association for Computational Linguistics, 93-104. https://doi.org/10.18653/V1/2022.ACL-DEMO. · DOI · Paper page
  5. Zekai Chen, Mariann Micsinai Balan, and Kevin Brown. 2023. Boosting Transformers and Language Models for Clinical Prediction in Immunotherapy. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 5: Industry Track), Sunayana Sitaram, Beata Beigman Klebanov, and Jason D Williams (Eds.). Association for Computational Linguistics, Toronto, Canada, 332-340. https://doi.org/10.18653/v1/2023.acl-industry.32 · DOI
  6. Robert Feldt and Ana Magazinius. 2010. Validity Threats in Empirical Software Engineering Research -An Initial Survey. In Proceedings of the 22nd International Conference on Software Engineering & Knowledge Engineering (SEKE'2010), Redwood City, San Francisco Bay, CA, USA, July 1 -July 3, 2010. Knowledge Systems Institute Graduate School, 374-379.
  7. Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. 2020. The 2020 expert survey on formal methods. In International Conference on Formal Methods for Industrial Critical Systems. Springer, 3-69.
  8. Samuel Greengard. 2021. The Internet of Things. MIT press.
  9. Chris Hawblitzel, Jon Howell, Jacob R. Lorch, Arjun Narayan, Bryan Parno, Danfeng Zhang, and Brian Zill. 2014. Ironclad Apps: End-to-End Security via Automated Full-System Verification. In 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI '14, Broomfield, CO, USA, October 6-8, 2014, Jason Flinn and Hank Levy (Eds.). USENIX Association, 165-181. https://www.usenix.org/conference/osdi14/technical-sessions/presentation/hawblitzel
  10. Yutai Hou, Hongyuan Dong, Xinghao Wang, Bohan Li, and Wanxiang Che. 2022. MetaPrompting: Learning to Learn Better Prompts. In Proceedings of the 29th International Conference on Computational Linguistics, COLING 2022, Gyeongju, Republic of Korea, October 12-17, 2022,
  11. Nicoletta Calzolari, Chu-Ren Huang, Hansaem Kim, James Pustejovsky, Leo Wanner, Key-Sun Choi, Pum-Mo Ryu, Hsin-Hsi Chen, Lucia Donatelli, Heng Ji, Sadao Kurohashi, Patrizia Paggio, Nianwen Xue, Seokhwan Kim, Younggyun Hahm, Zhong He, Tony Kyungil Lee, Enrico Santus, Francis Bond, and Seung-Hoon Na (Eds.). International Committee on Computational Linguistics, 3251-3262. https://aclanthology.org/2022.coling-1.287
  12. Albert Qiaochu Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygózdz, Piotr Milos, Yuhuai Wu, and Mateja Jamnik. 2022a. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 -December 9, 2022, Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Bel- grave, K. Cho, and A. Oh (Eds.). http://papers.nips.cc/paper_files/paper/2022/hash/377c25312668e48f2e531e2f2c422483- Abstract-Conference.html
  13. Sumith Kulal, Panupong Pasupat, Kartik Chandra, Mina Lee, Oded Padon, Alex Aiken, and Percy Liang. 2019. SPoC: Search-based Pseudocode to Code. In Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019, Vancouver, BC, Canada, Hanna M. Wallach, Hugo Larochelle, Alina Beygelzimer, Florence d'Alché-Buc, Emily B. Fox, and Roman Garnett (Eds.). 11883-11894.
  14. K. Rustan M. Leino. 2023. Program Proofs. MIT Press.
  15. K. Rustan M. Leino and Greg Nelson. 1998. An extended static checker for Modula-3. In International Conference on Compiler Construction. Springer, 302-305.
  16. Patrick S. H. Lewis, Ethan Perez, Aleksandra Piktus, Fabio Petroni, Vladimir Karpukhin, Naman Goyal, Heinrich Küttler, Mike Lewis, Wen-tau Yih, Tim Rocktäschel, Sebastian Riedel, and Douwe Kiela. 2020. Retrieval-Augmented Generation for Knowledge-Intensive NLP Tasks. In Advances in Neural Information Processing Systems 33: Annual Conference on Neural Information Processing Systems 2020, NeurIPS 2020, December 6-12, 2020, virtual, Hugo Larochelle, Marc'Aurelio Ranzato, Raia Hadsell, Maria-Florina Balcan, and Hsuan-Tien Lin (Eds.). https://proceedings.neurips.cc/paper/2020/ hash/6b493230205f780e1bc26945df7481e5-Abstract.html
  17. Liyi Li, Mingwei Zhu, Yi Lee, Le Chang, and Xiaodi Wu. 2022b. Quantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification. CoRR abs/2211.06411 (2022). https://doi.org/10.48550/arXiv.2211.06411 · DOI
  18. Yifei Li, Zeqi Lin, Shizhuo Zhang, Qiang Fu, Bei Chen, Jian-Guang Lou, and Weizhu Chen. 2023. Making Language Models Better Reasoners with Step-Aware Verifier. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), Anna Rogers, Jordan Boyd-Graber, and Naoaki Okazaki (Eds.). Association for Computational Linguistics, Toronto, Canada, 5315-5333. https://doi.org/10.18653/v1/2023.acl-long.291 · DOI · Paper page
  19. Mark Chen et al. 2021. Evaluating Large Language Models Trained on Code. CoRR abs/2107.03374 (2021). https: //arxiv.org/abs/2107.03374 · arXiv
  20. Nick McKenna, Tianyi Li, Liang Cheng, Mohammad Javad Hosseini, Mark Johnson, and Mark Steedman. 2023. Sources of Hallucination by Large Language Models on Inference Tasks. In Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023, Houda Bouamor, Juan Pino, and Kalika Bali (Eds.). Association for Computational Linguistics, 2758-2774. https://aclanthology.org/2023.findings-emnlp.182
  21. R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (Eds.). 1994. Selected Papers on Automath. North Holland.
  22. James Noble. 2024. Learn 'em Dafny. In Dafny Workshop at POPL (London, England). https://popl24.sigplan.org/details/dafny- 2024-papers/11/Learn-em-Dafny James Noble, David Streader, Isaac Oscar Gariano, and Miniruwani Samarakoon. 2022. More Programming Than Program- ming: Teaching Formal Methods in a Software Engineering Programme. In NASA Formal Methods -14th International Symposium, NFM 2022, Pasadena, CA, USA, May 24-27, 2022, Proceedings (Lecture Notes in Computer Science, Vol. 13260),
  23. OpenAI. 2023a. GPT-4 Technical Report. CoRR abs/2303.08774 (2023). https://doi.org/10.48550/arXiv.2303.08774 · DOI · Paper page
  24. Shuofei Qiao, Yixin Ou, Ningyu Zhang, Xiang Chen, Yunzhi Yao, Shumin Deng, Chuanqi Tan, Fei Huang, and Huajun Chen. 2023. Reasoning with Language Model Prompting: A Survey. In Proceedings of the 61st Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), ACL 2023, Toronto, Canada, July 9-14, 2023, Anna Rogers, Jordan L. Boyd-Graber, and Naoaki Okazaki (Eds.). Association for Computational Linguistics, 5368-5393. https://doi.org/10.18653/V1/2023.ACL-LONG.294 · DOI
  25. Rohan Anil et al. 2023. PaLM 2 Technical Report. CoRR abs/2305.10403 (2023). · arXiv
  26. Baptiste Rozière, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, Jérémy Rapin, et al. 2023. Code llama: Open foundation models for code. arXiv preprint arXiv:2308.12950 (2023). · arXiv
  27. Anthony J Viera, Joanne M Garrett, et al. 2005. Understanding interobserver agreement: the kappa statistic. Fam med 37, 5 (2005), 360-363. https://pubmed.ncbi.nlm.nih.gov/15883903/
  28. Yue Wang, Hung Le, Akhilesh Gotmare, Nghi D. Q. Bui, Junnan Li, and Steven C. H. Hoi. 2023. CodeT5+: Open Code Large Language Models for Code Understanding and Generation. (2023), 1069-1088. https://aclanthology.org/2023.emnlp- main.
  29. Y. Wang, W. Wang, S.R. Joty, and S.C.H. Hoi. 2021. CodeT5: Identifier-aware Unified Pre-trained Encoder-Decoder Models for Code Understanding and Generation. In EMNLP. https://doi.org/10.18653/v1/2021.emnlp-main.685 · DOI · Paper page
  30. Hillel Wayne. 2018. Temporal Logic. In Practical TLA+. Springer, 97-110.
  31. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Brian Ichter, Fei Xia, Ed H. Chi, Quoc V. Le, and Denny Zhou. 2022. Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 -December 9, 2022, Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (Eds.). http://papers.nips.cc/paper_files/paper/2022/hash/9d5609613524ecf4f15af0f7b31abca4-Abstract-Conference.html
  32. Yuhuai Wu, Albert Qiaochu Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with Large Language Models. In Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022, New Orleans, LA, USA, November 28 -December 9, 2022, Sanmi Koyejo, S. Mohamed, A. Agarwal, Danielle Belgrave, K. Cho, and A. Oh (Eds.). http://papers.nips.cc/paper_ files/paper/2022/hash/d0c6bc641a56bebee9d985b937307367-Abstract-Conference.html
  33. Michihiro Yasunaga and Percy Liang. 2020. Graph-based, Self-Supervised Program Repair from Diagnostic Feedback. In Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event (Proceedings of Machine Learning Research, Vol. 119). PMLR, 10799-10808. http://proceedings.mlr.press/v119/yasunaga20a.html

Cited by

Sorted by citations

Related

Authors
Misu, M. R. H., Lopes, C. V., Ma, I., & Noble, J.
Affiliations
  • University of California, Irvine (US)
  • Australian National University (AU)
ORCID
Venue
Proceedings of the ACM on Software Engineering
Publisher
Association for Computing Machinery (ACM)
Published
2024-07-12
Volume
1
Issue
FSE
Pages
812-835
ISSN
2994-970X (ISSN-L)
DOI
10.1145/3643763
OpenAlex
W4391505367
Cited by
38
References
61
Citations by year
2026: 12 · 2025: 22 · 2024: 4
FWCI
5.63
Type
journal article
Language
en
Open access
Licence
Locations
  • Proceedings of the ACM on software engineering. (publishedVersion)
  • arXiv (Cornell University) (submittedVersion, cc-by)
  • arXiv (Cornell University) (cc-by)
Topics
  • Physical Sciences › Computer Science › Artificial Intelligence › Logic, programming, and type systems
  • Physical Sciences › Computer Science › Information Systems › Software Engineering Research
  • Physical Sciences › Computer Science › Computer Science Applications › Teaching and Learning Programming
Keywords
Dafny, formal verification, large language models, code generation, GPT-4, PaLM 2, chain-of-thought prompting, retrieval augmentation, program specification, loop invariants, prompt engineering

About these checks

Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.

Statistics and arithmetic are recomputed, not judged.

Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.

What counts as a claim ›How we measure confidence ›How we check this ›

Are you an author, or do you see a problem with this page? Request a review