Elamur Research⌕
☰
home / papers / 2024 / Towards AI-Assisted Synthesis of Verified Dafny Methods

Towards AI-Assisted Synthesis of Verified Dafny Methods

Paper · 2024 · Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma et al.

Summary

Large language models often produce code that looks plausible but is wrong, and they are especially weak at verification-aware languages such as Dafny. In Dafny, code must include formal specifications and proof annotations that the verifier (built on the Z3 SMT solver) can check. The authors present what they describe as the first empirical study of LLMs generating verifiable Dafny methods. They took 178 problems from Google's MBPP benchmark and asked GPT-4 and PaLM-2 to produce complete methods, including pre- and postconditions, loop invariants and other annotations. Three prompting strategies were compared. The outputs were checked with the Dafny verifier and also manually reviewed to confirm that the specifications were meaningful. GPT-4 clearly beat PaLM-2, and a Chain of Thought prompt enriched with retrieved, similar worked examples worked best for both models. The work also produced a new benchmark of verified Dafny programs. Its broader argument is that pairing generative models with formal checking can make machine-written code trustworthy rather than merely convincing.

Key points

  • Prompt types: a bare Contextless prompt; a Signature prompt that adds the method signature and test cases; and a CoT prompt that breaks the task into steps using retrieval-augmented few-shot examples.
  • GPT-4 results:
    • With the CoT prompt, it produced verified, human-approved Dafny methods for 58% of problems (103 of 178).
    • With the Contextless prompt, it reached only 19%.
    • With the Signature prompt, it reached about 10%.
  • Released dataset: MBPP-DFY-153 contains 153 Dafny problems with specifications, solutions and tests. Of these, 50 were written by hand and 103 were generated by GPT-4.
  • Setup: the experiments used Dafny 4.0 and a then-new GPT-4 version. The authors expect the results to shift, probably improving, with later releases.
  • Availability: all artifacts (benchmark, prompts, model outputs, manual evaluation) are public in the dafny-synthesis GitHub repository. The paper was published at FSE 2024.

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

🎓University of California, IrvineIrvine · United States45 works · 36,639 citations🎓Australian National UniversityCanberra · Australia27 works · 7,072 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 19,503 worksArtificial Intelligence · 18,805 worksInformation Systems · 1,888 worksComputer Science Applications · 184 works

Cite

Cite as Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma and James Noble. 2024. Towards AI-Assisted Synthesis of Verified Dafny Methods. arXiv:2402.00247.

The paper itself, not this page. BibTeX from the library's record of the work. DOI 10.1145/3643763 · arXiv 2402.00247

@misc{misu2024ai,
  title = {{Towards AI-Assisted Synthesis of Verified Dafny Methods}},
  author = {Md Rakib Hossain Misu, Cristina V. Lopes, Iris Ma and James Noble},
  year = {2024},
  doi = {10.1145/3643763},
  eprint = {2402.00247},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.1145/3643763}
}

References

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

  1. Aakanksha Chowdhery et al. 2022. PaLM: Scaling Language Modeling with Pathways. CoRR abs/2204.02311 (2022).
  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 ↗
  3. Amazon. 2023. Automated reasoning. https://www.amazon.science/research-areas/automated-reasoning. [Online], [Accessed: 2023-09-20]. ↗
  4. 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 ↗
  5. Amos Azaria and Tom M. Mitchell. 2023. The Internal State of an LLM Knows When It’s Lying. 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, 967–976. h…
  6. 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 AlSh… — PromptSource: An Integrated Development Environment and Repository for Natural Language Prompts
  7. Clark W. Barrett, Roberto Sebastiani, Sanjit A. Seshia, and Cesare Tinelli. 2021. Satisfiability Modulo Theories. In Handbook of Satisfiability - Second Edition, Armin Biere, Marijn Heule, Hans van Maaren, and Toby Walsh (Eds.). Frontiers in Artificial Intelligence and Applications, Vol. 336. IOS Pr… — [doi:10.3233/faia201017](https://doi.org/10.3233/faia201017) find
  8. Luca Beurer-Kellner, Marc Fischer, and Martin T. Vechev. 2023. Prompting Is Programming: A Query Language for Large Language Models. Proc. ACM Program. Lang. 7, PLDI (2023), 1946–1969. https://doi.org/10.1145/3591300 ↗
  9. Franck Cassez, Joanne Fuller, Milad K. Ghale, David J. Pearce, and Horacio Mijail Anton Quiles. 2023. Formal and Executable Semantics of the Ethereum Virtual Machine in Dafny. In Formal Methods - 25th International Symposium, FM 2023, Lübeck, Germany, March 6-10, 2023, Proceedings (Lecture Notes in… — [doi:10.1007/978-3-031-27481-7_32](https://doi.org/10.1007/978-3-031-27481-7_32) find
  10. Aleksandar Chakarov, Aleksandr Fedchin, Zvonimir Rakamaric, and Neha Rungta. 2022. Better Counterexamples for Dafny. In TACAS (Lecture Notes in Computer Science, Vol. 13243), Dana Fisman and Grigore Rosu (Eds.). Springer, 404–411. https://doi.org/10.1007/978-3-030-99524-9_23 — [doi:10.1007/978-3-030-99524-9_23](https://doi.org/10.1007/978-3-030-99524-9_23) ↗
  11. Saikat Chakraborty and Baishakhi Ray. 2021. On Multi-Modal Learning of Editing Source Code. In 36th IEEE/ACM International Conference on Automated Software Engineering, ASE 2021, Melbourne, Australia, November 15-19, 2021. IEEE, 443–455. https://doi.org/10.1109/ASE51524.2021.9678559 — [doi:10.1109/ase51524.2021.9678559](https://doi.org/10.1109/ase51524.2021.9678559) ↗
  12. 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 Kleban… find
  13. Amazon CodeWhisperer. 2023. Amazon CodeWhisperer. https://aws.amazon.com/codewhisperer/. [Online], [Accessed: 2023-09-20]. ↗
  14. CompCert. 2023. CompCert. https://github.com/AbsInt/CompCert. [Online], [Accessed: 2023-09-20]. ↗
  15. Byron Cook. 2018. Formal Reasoning About the Security of Amazon Web Services. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (Lecture Notes in Computer Science, Vol… — [doi:10.1007/978-3-319-96145-3_3](https://doi.org/10.1007/978-3-319-96145-3_3) find
  16. GitHub Copilot. 2023. GitHub Copilot. https://github.com/features/copilot. [Online], [Accessed: 2023-09-20]. ↗
  17. Garett Cunningham, Razvan C. Bunescu, and David Juedes. 2022. Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs. (2022), 25–32. https://aclanthology.org/2022.mathnlp-1.4.pdf ↗
  18. Lukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reason. 61, 1-4 (2018), 423–453. https://doi.org/10.1007/S10817-018-9458-4 ↗
  19. Dafny. 2023. dafny-lang. https://github.com/dafny-lang/dafny. [Online], [Accessed: 2023-09-20]. ↗
  20. Hai Dang, Lukas Mecke, Florian Lehmann, Sven Goller, and Daniel Buschek. 2022. How to Prompt? Opportunities and Challenges of Zero- and Few-Shot Learning for Human-AI Interaction in Creative Applications of Generative Models. CoRR abs/2209.01390. https://doi.org/10.48550/arxiv.2209.01390 — [doi:10.48550/arxiv.2209.01390](https://doi.org/10.48550/arxiv.2209.01390) ↗
  21. Leonardo Mendonça de Moura and Nikolaj S. Bjørner. 2008. Z3: An Efficient SMT Solver. In TACAS. 337–340. https://doi.org/10.1007/978-3-540-78800-3_24 Niklas Deckers, Maik Fröbe, Johannes Kiesel, Gianluca Pandolfo, Christopher Schröder, Benno Stein, and Martin Potthast. 2023. The Infinite Index: Inf… ↗
  22. David Dohan, Winnie Xu, Aitor Lewkowycz, Jacob Austin, David Bieber, Raphael Gontijo Lopes, Yuhuai Wu, Henryk Michalewski, Rif A. Saurous, Jascha Sohl-Dickstein, Kevin Murphy, and Charles Sutton. 2022. Language Model Cascades. https://doi.org/10.48550/arXiv.2207.10342 ↗
  23. Andres Erbsen, Jade Philipoom, Jason Gross, Robert Sloan, and Adam Chlipala. 2020. Simple High-Level Code For Cryptographic Arithmetic: With Proofs, Without Compromises. ACM SIGOPS Oper. Syst. Rev. 54, 1 (2020), 23–30. https://doi.org/10.1145/3421473.3421477 — [doi:10.1145/3421473.3421477](https://doi.org/10.1145/3421473.3421477) ↗
  24. João Pascoal Faria and Rui Abreu. 2023. Case Studies of Development of Verified Programs with Dafny for Accessibility Assessment. In Fundamentals of Software Engineering - 10th International Conference, FSEN 2023, Tehran, Iran, May 4-5, 2023, Revised Selected Papers (Lecture Notes in Computer Scienc… — [doi:10.1007/978-3-031-42441-0_3](https://doi.org/10.1007/978-3-031-42441-0_3) find
  25. 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. Kn… find
  26. Emily First and Yuriy Brun. 2022. Diversity-Driven Automated Formal Verification. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022. ACM, 1–13. https://doi.org/10.1145/ 3510003.3510138 Emily First, Yuriy Brun, and Arjun Guha. 2020… — [doi:10.1145/3428299](https://doi.org/10.1145/3428299) find
  27. Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, ESEC/FSE 2023, San Francisco,…
  28. Ricardo Bedin França, Denis Favre-Felix, Xavier Leroy, Marc Pantel, and Jean Souyris. 2011. Towards Formally Verified Optimizing Compilation in Flight Control Software. In Bringing Theory to Practice: Predictability and Performance in Embedded Systems, DATE Workshop PPES 2011, March 18, 2011, Grenob… — [doi:10.4230/oasics.ppes.2011.59](https://doi.org/10.4230/oasics.ppes.2011.59) find
  29. Simon Frieder, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewicz, Philipp Christian Petersen, Alexis Chevalier, and Julius Berner. 2023. Mathematical Capabilities of ChatGPT. CoRR abs/2301.13867 (2023). https://doi.org/10.48550/arXiv.2301.13867 Boris A. Galitsky. 2023. Trut… ↗
  30. Preprints (2023). https://doi.org/10.20944/preprints202307.1723.v1 Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. 2020. — [doi:10.20944/preprints202307.1723.v1](https://doi.org/10.20944/preprints202307.1723.v1) ↗
  31. The 2020 expert survey on formal methods. In International Conference on Formal Methods for Industrial Critical Systems. Springer, 3–69. find
  32. GCC. 2023. GCC, the GNU Compiler Collection. https://gcc.gnu.org/. [Online], [Accessed: 2023-09-20]. ↗
  33. Claire Le Goues, K. Rustan M. Leino, and Michal Moskal. 2011. The Boogie Verification Debugger (Tool Paper). 7041 (2011), 407–414. https://doi.org/10.1007/978-3-642-24690-6_28 — [doi:10.1007/978-3-642-24690-6_28](https://doi.org/10.1007/978-3-642-24690-6_28) ↗
  34. Samuel Greengard. 2021. The Internet of Things. MIT press. find
  35. Sumit Gulwani, Oleksandr Polozov, and Rishabh Singh. 2017. Program Synthesis. Founds. Trends. Prog. Lang. 4, 1-2 (2017), 1–119. https://doi.org/10.1561/2500000010 ↗
  36. Kevin A Hallgren. 2012. Computing inter-rater reliability for observational data: an overview and tutorial. Tutorials in quantitative methods for psychology 8, 1 (2012), 23. https://doi.org/10.20982/tqmp.08.1.p023 — [doi:10.20982/tqmp.08.1.p023](https://doi.org/10.20982/tqmp.08.1.p023) ↗
  37. Chris Hawblitzel, Jon Howell, Manos Kapritsos, Jacob R. Lorch, Bryan Parno, Michael L. Roberts, Srinath T. V. Setty, and Brian Zill. 2015. IronFleet: proving practical distributed systems correct. In SOSP, Ethan L. Miller and Steven Hand (Eds.). ACM, 1–17. https://doi.org/10.1145/2815400.2815428 — [doi:10.1145/2815400.2815428](https://doi.org/10.1145/2815400.2815428) ↗
  38. 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-… find
  39. C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (1969), 576–580. https://doi.org/10.1145/363235.363259 Yutai Hou, Hongyuan Dong, Xinghao Wang, Bohan Li, and Wanxiang Che. 2022. MetaPrompting: Learning to Learn Better Prompts. In Proceedings of the 29th Internat… ↗
  40. Ahmed Irfan, Sorawee Porncharoenwase, Zvonimir Rakamaric, Neha Rungta, and Emina Torlak. 2022. Testing Dafny (experience paper). In ISSTA ’22: 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, Virtual Event, South Korea, July 18 - 22, 2022, Sukyoung Ryu and Yannis Smaragdaki… find
  41. 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…
  42. Ellen Jiang, Kristen Olson, Edwin Toh, Alejandra Molina, Aaron Donsbach, Michael Terry, and Carrie J. Cai. 2022b. Prompt-Maker: Prompt-based Prototyping with Large Language Models. In CHI ’22: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022 - 5 May 2022, Ext… — [doi:10.1145/3491101.3503564](https://doi.org/10.1145/3491101.3503564) find
  43. Cliff B Jones and Jayadev Misra. 2021. Theories of Programming: The Life and Works of Tony Hoare. find
  44. Morgan & Claypool. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David A. Cock, Philip Derrin, Dhammika Elkaduwe, Kai Engelhardt, Rafal Kolanski, Michael Norrish, Thomas Sewell, Harvey Tuch, and Simon Winwood. 2009. seL4: formal verification of an OS kernel.. In Proceedings of the… find
  45. 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,…
  46. K. Rustan M. Leino. 2017. Accessible Software Verification with Dafny. IEEE Softw. 34, 6 (2017), 94–97. https://doi.org/10. 1109/MS.2017.4121212 K. Rustan M. Leino. 2023. find
  47. Program Proofs. MIT Press. K. Rustan M. Leino and Greg Nelson. 1998. An extended static checker for Modula-3. In International Conference on Compiler Construction. Springer, 302–305. find
  48. Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107–115. https://doi.org/10.1145/ 1538788.1538814 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… find
  49. 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:10.48550/arxiv.2211.06411](https://doi.org/10.48550/arxiv.2211.06411) ↗
  50. 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…
  51. Vivian Liu and Lydia B. Chilton. 2022. Design Guidelines for Prompt Engineering Text-to-Image Generative Models. In CHI ’22: CHI Conference on Human Factors in Computing Systems, New Orleans, LA, USA, 29 April 2022 - 5 May 2022, Simone D. J. Barbosa, Cliff Lampe, Caroline Appert, David A. Shamma, St… — [doi:10.1145/3491102.3501825](https://doi.org/10.1145/3491102.3501825) find
  52. LLVM. 2023. The LLVM Compiler Infrastructure. https://llvm.org/. [Online], [Accessed: 2023-09-20]. ↗
  53. Aman Madaan, Shuyan Zhou, Uri Alon, Yiming Yang, and Graham Neubig. 2022. Language Models of Code are Few-Shot Commonsense Learners. In EMNLP, Yoav Goldberg, Zornitsa Kozareva, and Yue Zhang (Eds.). Association for Computational Linguistics, 1384–1403.
  54. Mark Chen et al. 2021. Evaluating Large Language Models Trained on Code. CoRR abs/2107.03374 (2021). https://arxiv.org/abs/2107.03374 ↗
  55. Ehsan Mashhadi and Hadi Hemmati. 2021. Applying CodeBERT for Automated Program Repair of Java Simple Bugs. In MSR. 505–509. https://doi.org/10.1109/MSR52588.2021.00063 — [doi:10.1109/msr52588.2021.00063](https://doi.org/10.1109/msr52588.2021.00063) ↗
  56. Antonio Mastropaolo, Nathan Cooper, David Nader-Palacio, Simone Scalabrino, Denys Poshyvanyk, Rocco Oliveto, and Gabriele Bavota. 2023. Using Transfer Learning for Code-Related Tasks. IEEE Trans. Software Eng. 49, 4 (2023), 1580–1598. https://doi.org/10.1109/TSE.2022.3183297 — [doi:10.1109/tse.2022.3183297](https://doi.org/10.1109/tse.2022.3183297) ↗
  57. 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 Pi…
  58. Jordan Meadows and André Freitas. 2022. A Survey in Mathematical Language Processing. CoRR abs/2205.15231 (2022). https://doi.org/10.48550/arXiv.2205.15231 — [doi:10.48550/arxiv.2205.15231](https://doi.org/10.48550/arxiv.2205.15231) ↗
  59. Bertrand Meyer. 1992. Applying ’Design by Contract’. Computer 25, 10 (1992), 40–51. find
  60. Microsoft. 2023a. The Dafny Programming and Verification Language. https://dafny.org/. [Online], [Accessed: 2023-09-20]. ↗
  61. Microsoft. 2023b. Microsoft Research. https://www.microsoft.com/en-us/research/. [Online], [Accessed: 2023-09-20]. ↗
  62. Toby C. Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: From General Purpose to a Proof of Information Flow Enforcement. In 2013 IEEE Symposium on Security and Privacy, SP 2013, Berkeley, CA, USA, May 19-22, 2… — [doi:10.1109/sp.2013.35](https://doi.org/10.1109/sp.2013.35) find
  63. Noor Nashid, Mifta Sintaha, and Ali Mesbah. 2023. Retrieval-Based Prompt Selection for Code-Related Few-Shot Learning. In 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023. IEEE, 2450–2462. https://doi.org/10.1109/ICSE48619.2023.00205 R.… — [doi:10.1109/icse48619.2023.00205](https://doi.org/10.1109/icse48619.2023.00205) ↗
  64. North Holland. 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 ↗
  65. James Noble, David Streader, Isaac Oscar Gariano, and Miniruwani Samarakoon. 2022. More Programming Than Programming: 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… — [doi:10.1007/978-3-031-06773-0_23](https://doi.org/10.1007/978-3-031-06773-0_23) find
  66. OpenAI. 2023a. GPT-4 Technical Report. CoRR abs/2303.08774 (2023). https://doi.org/10.48550/arXiv.2303.08774 ↗
  67. OpenAI. 2023b. OpenAI. https://platform.openai.com/docs/models. [Online], [Accessed: 2023-09-20]. ↗
  68. 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, T…
  69. Alec Radford, Karthik Narasimhan, Tim Salimans, Ilya Sutskever, et al. 2018. Improving language understanding by generative pre-training. find
  70. OpenAI.com. Laria Reynolds and Kyle McDonell. 2021. Prompt Programming for Large Language Models: Beyond the Few-Shot Paradigm. In CHI ’21: CHI Conference on Human Factors in Computing Systems, Virtual Event / Yokohama Japan, May 8-13, 2021, Extended Abstracts, Yoshifumi Kitamura, Aaron Quigley, Kat…
  71. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, and Zachary Tatlock. 2019. QED at Large: A Survey of Engineering of Formally Verified Software. Founds. Trends. Prog. Lang. 5, 2-3 (2019), 102–281. https://doi.org/10.1561/2500000045 — [doi:10.1561/2500000045](https://doi.org/10.1561/2500000045) ↗
  72. Rohan Anil et al. 2023. PaLM 2 Technical Report. CoRR abs/2305.10403 (2023).
  73. 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).
  74. M. Salvagno and A.G. Taccone, F.S.and Gerli. 2023. Artificial intelligence hallucinations. find
  75. Crit Care (2023). https://doi.org/10. 1186/s13054-023-04473-y Alex Sanchez-Stern, Yousef Alhessi, Lawrence K. Saul, and Sorin Lerner. 2020. Generating correctness proofs with neural networks. In Proceedings of the 4th ACM SIGPLAN International Workshop on Machine Learning and Programming Languages,…
  76. Janet Siegmund, Norbert Siegmund, and Sven Apel. 2015. Views on Internal and External Validity in Empirical Software Engineering. In 37th IEEE/ACM International Conference on Software Engineering, ICSE 2015, Florence, Italy, May 16-24, 2015, Volume 1, Antonia Bertolino, Gerardo Canfora, and Sebastia… — [doi:10.1109/icse.2015.24](https://doi.org/10.1109/icse.2015.24) find
  77. Mifta Sintaha, Noor Nashid, and Ali Mesbah. 2023. Katana: Dual Slicing Based Context for Learning Bug Fixes. ACM Trans. Softw. Eng. Methodol. 32, 4 (2023), 100:1–100:27. https://doi.org/10.1145/3579640 — [doi:10.1145/3579640](https://doi.org/10.1145/3579640) ↗
  78. Michele Tufano, Shao Kun Deng, Neel Sundaresan, and Alexey Svyatkovskiy. 2022a. METHODS2TEST: A dataset of focal methods mapped to test cases. In 19th IEEE/ACM International Conference on Mining Software Repositories, MSR 2022, Pittsburgh, PA, USA, May 23-24, 2022. ACM, 299–303. https://doi.org/10.1… — [doi:10.1145/3524842.3528009](https://doi.org/10.1145/3524842.3528009) find
  79. Michele Tufano, Cody Watson, Gabriele Bavota, Massimiliano Di Penta, Martin White, and Denys Poshyvanyk. 2019. An Empirical Study on Learning Bug-Fixing Patches in the Wild via Neural Machine Translation. ACM Trans. Softw. Eng. Methodol. 28, 4 (2019), 19:1–19:29. https://doi.org/10.1145/3340544 ↗
  80. Rosalia Tufano, Simone Masiero, Antonio Mastropaolo, Luca Pascarella, Denys Poshyvanyk, and Gabriele Bavota. 2022b. Using Pre-Trained Models to Boost Code Review Automation. In 44th IEEE/ACM 44th International Conference on Software Engineering, ICSE 2022, Pittsburgh, PA, USA, May 25-27, 2022. ACM,… — [doi:10.1145/3510003.3510621](https://doi.org/10.1145/3510003.3510621) find
  81. Rosalia Tufano, Luca Pascarella, and Gabriele Bavota. 2023. Automating Code-Related Tasks Through Transformers: The Impact of Pre-training. In 45th IEEE/ACM International Conference on Software Engineering, ICSE 2023, Melbourne, Australia, May 14-20, 2023. IEEE, 2425–2437. https://doi.org/10.1109/IC… — [doi:10.1109/icse48619.2023.00203](https://doi.org/10.1109/icse48619.2023.00203) ↗
  82. 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/ ↗
  83. 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.68 ↗
  84. 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 ↗
  85. Cody Watson, Nathan Cooper, David Nader-Palacio, Kevin Moran, and Denys Poshyvanyk. 2022. A Systematic Literature Review on the Use of Deep Learning in Software Engineering Research. ACM Trans. Softw. Eng. Methodol. 31, 2 (2022), 32:1–32:58. https://doi.org/10.1145/3485275 — [doi:10.1145/3485275](https://doi.org/10.1145/3485275) ↗
  86. Hillel Wayne. 2018. Temporal Logic. In Practical TLA+. Springer, 97–110. find
  87. 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 Processi…
  88. 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,…
  89. Yanming Yang, Xin Xia, David Lo, and John C. Grundy. 2022. A Survey on Deep Learning for Software Engineering. ACM Comput. Surv. 54, 10s (2022), 206:1–206:73. https://doi.org/10.1145/3505243 — [doi:10.1145/3505243](https://doi.org/10.1145/3505243) ↗
  90. Zhenkun Yang, Wen Wang, Jeremy Casas, Pasquale Cocchini, and Jin Yang. 2023. Towards A Correct-by-Construction FHE Model. IACR Cryptol. ePrint Arch. (2023), 281. https://eprint.iacr.org/2023/281 ↗
  91. 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.… find
  92. Hattie Zhou, Azade Nova, Hugo Larochelle, Aaron C. Courville, Behnam Neyshabur, and Hanie Sedghi. 2022. Teaching Algorithmic Reasoning via In-context Learning. CoRR abs/2211.09066 (2022). https://doi.org/10.48550/arXiv.2211.09066 ↗
  93. Received 2023-09-29; accepted 2024-01-23 find

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/misu-2024-ai-assisted-synthesis-verified-dafny/