{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,17]],"date-time":"2026-10-17T19:17:37Z","timestamp":1792264657817,"version":"4.4.0"},"reference-count":104,"publisher":"Association for Computing Machinery (ACM)","issue":"FSE","license":[{"start":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T00:00:00Z","timestamp":1720742400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Proc. ACM Softw. Eng."],"published-print":{"date-parts":[[2024,7,12]]},"abstract":"<jats:p>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\u2019 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.<\/jats:p>\n                  <jats:p>\n                    In this paper, we demonstrate how to improve two pretrained models\u2019 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\n                    <jats:italic toggle=\"yes\">Contextless<\/jats:italic>\n                    prompt; a\n                    <jats:italic toggle=\"yes\">Signature<\/jats:italic>\n                    prompt that includes a method signature and test cases, and a\n                    <jats:italic toggle=\"yes\">Chain of Thought (CoT)<\/jats:italic>\n                    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\n                    <jats:italic toggle=\"yes\">Contextless<\/jats:italic>\n                    prompt, and even fewer (10%) for the\n                    <jats:italic toggle=\"yes\">Signature<\/jats:italic>\n                    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.\n                  <\/jats:p>\n                  <jats:p>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 \u201cprogrammer\u2019s verification apprentice\u201d, 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 \u2014 generating candidate solutions that are subsequently formally checked for correctness \u2014 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.<\/jats:p>","DOI":"10.1145\/3643763","type":"journal-article","created":{"date-parts":[[2024,7,12]],"date-time":"2024-07-12T10:22:09Z","timestamp":1720779729000},"page":"812-835","source":"Crossref","is-referenced-by-count":45,"title":["Towards AI-Assisted Synthesis of Verified Dafny Methods"],"prefix":"10.1145","volume":"1","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7931-6782","authenticated-orcid":false,"given":"Md Rakib Hossain","family":"Misu","sequence":"first","affiliation":[{"name":"University of California, Irvine, Irvine, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0551-3908","authenticated-orcid":false,"given":"Cristina V.","family":"Lopes","sequence":"additional","affiliation":[{"name":"University of California, Irvine, Irvine, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0003-3699-7981","authenticated-orcid":false,"given":"Iris","family":"Ma","sequence":"additional","affiliation":[{"name":"University of California, Irvine, Irvine, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9036-5692","authenticated-orcid":false,"given":"James","family":"Noble","sequence":"additional","affiliation":[{"name":"Creative Research &amp; Programming, Wellington, New Zealand"},{"name":"Australian National University, Canberra, Australia"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,7,12]]},"reference":[{"key":"e_1_3_1_2_1","unstructured":"Aakanksha Chowdhery et al. 2022. PaLM: Scaling Language Modeling with Pathways. CoRR abs\/2204.02311 (2022)."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3212695"},{"key":"e_1_3_1_4_1","unstructured":"Amazon. 2023. Automated reasoning. https:\/\/www.amazon.science\/research-areas\/automated-reasoning. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_5_1","unstructured":"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"},{"key":"e_1_3_1_6_1","doi-asserted-by":"crossref","first-page":"967","DOI":"10.18653\/v1\/2023.findings-emnlp.68","volume-title":"Findings of the Association for Computational Linguistics: EMNLP 2023","author":"Azaria Amos","year":"2023","unstructured":"Amos Azaria and Tom M. Mitchell. 2023. The Internal State of an LLM Knows When It\u2019s 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\u2013976. https:\/\/aclanthology.org\/2023.findings-emnlp.68"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Stephen H. Bach Victor Sanh Zheng Xin Yong Albert Webson Colin Raffel Nihal V. Nayak Abheesht Sharma Taewoon Kim M. Saiful Bari Thibault F\u00e9vry 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\u2013104. https:\/\/doi.org\/10.18653\/V1\/2022.ACL-DEMO.9 10.18653\/V1\/2022.ACL-DEMO.9","DOI":"10.18653\/V1\/2022.ACL-DEMO.9"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.3233\/FAIA201017"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3591300"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-27481-7_32"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99524-9_23"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE51524.2021.9678559"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2023.acl-industry.32"},{"key":"e_1_3_1_14_1","unstructured":"Amazon CodeWhisperer. 2023 Amazon CodeWhisperer. https:\/\/aws.amazon.com\/codewhisperer. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_15_1","unstructured":"CompCert. 2023. CompCert. https:\/\/github.com\/AbsInt\/CompCert. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-96145-3_3"},{"key":"e_1_3_1_17_1","unstructured":"GitHub Copilot. 2023. GitHub Copilot. https:\/\/github.com\/features\/copilot. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_18_1","doi-asserted-by":"crossref","unstructured":"Garett Cunningham Razvan C. Bunescu and David Juedes. 2022. Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs. (2022) 25\u201332. https:\/\/aclanthology.org\/2022.mathnlp-1.4.pdf","DOI":"10.18653\/v1\/2022.mathnlp-1.4"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/S10817-018-9458-4"},{"key":"e_1_3_1_20_1","unstructured":"Dafny. 2023. dafny-lang. https:\/\/github.com\/dafny-lang\/dafny. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"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 10.48550\/arxiv.2209.01390","DOI":"10.48550\/arxiv.2209.01390"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","unstructured":"Leonardo Mendon\u00e7a de Moura and Nikolaj S. Bj\u00f8rner. 2008. Z3: An Effcient SMT Solver. In TACAS. 337\u2013340. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3576840.3578327"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"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 10.48550\/arXiv.2207.10342","DOI":"10.48550\/arXiv.2207.10342"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3421473.3421477"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-42441-0_3"},{"key":"e_1_3_1_27_1","first-page":"374","article-title":"Validity Threats in Empirical Software Engineering Research - An Initial Survey","author":"Feldt Robert","year":"2010","unstructured":"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\u20192010), Redwood City, San Francisco Bay, CA, USA, July 1 - July 3, 2010. Knowledge Systems Institute Graduate School, 374\u2013379.","journal-title":"Proceedings of the 22nd International Conference on Software Engineering & Knowledge Engineering (SEKE\u20192010), Redwood City, San Francisco Bay, CA, USA, July 1 - July 3, 2010"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510138"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428299"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/3611643.3616243"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASICS.PPES.2011.59"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Simon Frieder Luca Pinchetti Ryan-Rhys Griffths 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 10.48550\/arXiv.2301.13867","DOI":"10.48550\/arXiv.2301.13867"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Boris A. Galitsky. 2023. Truth-O-Meter: Collaborating with LLM in Fighting its Hallucinations. Preprints (2023).https:\/\/doi.org\/10.20944\/preprints202307.1723.v1 10.20944\/preprints202307.1723.v1","DOI":"10.20944\/preprints202307.1723.v1"},{"key":"e_1_3_1_34_1","first-page":"3","volume-title":"InternationalConference on Formal Methods for Industrial Critical Systems","author":"Garavel Hubert","year":"2020","unstructured":"Hubert Garavel, Maurice H Ter Beek, and Jaco Van De Pol. 2020. The 2020 expert survey on formal methods. In InternationalConference on Formal Methods for Industrial Critical Systems. Springer, 3\u201369."},{"key":"e_1_3_1_35_1","unstructured":"GCC. 2023. GCC the GNU Compiler Collection. https:\/\/gcc.gnu.org\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","unstructured":"Claire Le Goues K. Rustan M. Leino and Michal Moskal. 2011. The Boogie Verification Debugger (Tool Paper). 7041 (2011) 407\u2013414.https:\/\/doi.org\/10.1007\/978-3-642-24690-6_28 10.1007\/978-3-642-24690-6_28","DOI":"10.1007\/978-3-642-24690-6_28"},{"key":"e_1_3_1_37_1","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/13937.001.0001","volume-title":"The Internet of Things","author":"Samuel Greengard","year":"2021","unstructured":"Samuel Greengard. 2021. The Internet of Things. MIT press."},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000010"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.20982\/tqmp.08.1.p023"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2815400.2815428"},{"key":"e_1_3_1_41_1","first-page":"165","volume-title":"11th USENIX Symposium on Operating Systems Design and Implementation, OSDI\u201914, Broomfield, CO, USA, October 6-8, 2014","author":"Hawblitzel Chris","year":"2014","unstructured":"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\u201914, Broomfield, CO, USA, October 6-8, 2014, Jason Flinn and Hank Levy (Eds.). USENIX Association, 165\u2013181. https:\/\/www.usenix.org\/conference\/osdi14\/technical-sessions\/presentation\/hawblitzel"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/363235.363259"},{"key":"e_1_3_1_43_1","first-page":"3251","volume-title":"Proceedings of the 29th International Conference on Computational Linguistics, COLING 2022, Gyeongju, Republic of Korea, October 12-17, 2022","author":"Hou Yutai","year":"2022","unstructured":"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, 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\u20133262. https:\/\/aclanthology.org\/2022.coling-1.287"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3533767.3534382"},{"key":"e_1_3_1_45_1","unstructured":"Kevin Jacobs and Benjamin Beurdouche. 2022. Performance Improvements via Formally-Verified Cryptography in Firefox. https:\/\/blog.mozilla.org\/security\/2020\/07\/06\/performance-improvements-viaformally-verified-cryptography-in-firefox\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_46_1","unstructured":"Albert Qiaochu Jiang Wenda Li Szymon Tworkowski Konrad Czechowski Tomasz Odrzyg\u00f3zdz 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 Belgrave K. Cho and A. Oh (Eds.). http:\/\/papers.nips.cc\/paper_files\/paper\/2022\/hash\/377c25312668e48f2e531e2f2c422483-Abstract-Conference.html"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3491101.3503564"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/3477355"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_1_50_1","first-page":"11883","volume-title":"Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, December 8-14, 2019","author":"Kulal Sumith","year":"2019","unstructured":"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\u2019Alch\u00e9-Buc, Emily B. Fox, and Roman Garnett (Eds.). 11883\u201311894."},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","DOI":"10.1109\/MS.2017.4121212"},{"key":"e_1_3_1_52_1","volume-title":"Program Proofs","author":"Rustan K.","year":"2023","unstructured":"K. Rustan M. Leino. 2023. Program Proofs. MIT Press."},{"key":"e_1_3_1_53_1","doi-asserted-by":"crossref","first-page":"302","DOI":"10.1007\/BFb0026441","volume-title":"International Conference on Compiler Construction","author":"Rustan K.","year":"1998","unstructured":"K. Rustan M. Leino and Greg Nelson. 1998. An extended static checker for Modula-3. In International Conference on Compiler Construction. Springer, 302\u2013305."},{"key":"e_1_3_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_1_55_1","unstructured":"Patrick S. H. Lewis Ethan Perez Aleksandra Piktus Fabio Petroni Vladimir Karpukhin Naman Goyal Heinrich K\u00fcttler Mike Lewis Wen-tau Yih Tim Rockt\u00e4schel 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\u2019Aurelio Ranzato Raia Hadsell Maria-Florina Balcan and Hsuan-Tien Lin (Eds.). https:\/\/proceedings.neurips.cc\/paper\/2020\/hash\/6b493230205f780e1bc26945df7481e5-Abstract.html"},{"key":"e_1_3_1_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3540250.3549099"},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","unstructured":"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 https:\/\/doi.org\/10.48550\/arXiv.2211.06411 10.48550\/arXiv.2211.06411","DOI":"10.48550\/arXiv.2211.06411"},{"key":"e_1_3_1_58_1","doi-asserted-by":"publisher","unstructured":"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\u20135333. https:\/\/doi.org\/10.18653\/v1\/2023.acl-long.291 10.18653\/v1\/2023.acl-long.291","DOI":"10.18653\/v1\/2023.acl-long.291"},{"key":"e_1_3_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3491102.3501825"},{"key":"e_1_3_1_60_1","unstructured":"LLVM. 2023. The LLVM Compiler Infrastructure. https:\/\/llvm.org\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_61_1","first-page":"1384","volume-title":"EMNLP","author":"Madaan Aman","year":"2022","unstructured":"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\u20131403."},{"key":"e_1_3_1_62_1","unstructured":"Mark Chen et al. 2021. Evaluating Large Language Models Trained on Code. CoRR abs\/2107.03374 (2021). https:\/\/arxiv.org\/abs\/2107.03374"},{"key":"e_1_3_1_63_1","doi-asserted-by":"publisher","unstructured":"Ehsan Mashhadi and Hadi Hemmati. 2021. Applying CodeBERT for Automated Program Repair of Java Simple Bugs. In MSR. 505\u2013509.https:\/\/doi.org\/10.1109\/MSR52588.2021.00063 10.1109\/MSR52588.2021.00063","DOI":"10.1109\/MSR52588.2021.00063"},{"key":"e_1_3_1_64_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2022.3183297"},{"key":"e_1_3_1_65_1","first-page":"2758","volume-title":"Findings of the Association for Computational Linguistics: EMNLP 2023, Singapore, December 6-10, 2023","author":"McKenna Nick","year":"2023","unstructured":"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\u20132774. https:\/\/aclanthology.org\/2023.findings-emnlp.182"},{"key":"e_1_3_1_66_1","doi-asserted-by":"publisher","unstructured":"Jordan Meadows and Andr\u00e9 Freitas. 2022. A Survey in Mathematical Language Processing. CoRR abs\/2205.15231 (2022).https:\/\/doi.org\/10.48550\/arXiv.2205.15231 10.48550\/arXiv.2205.15231","DOI":"10.48550\/arXiv.2205.15231"},{"key":"e_1_3_1_67_1","doi-asserted-by":"publisher","DOI":"10.1109\/2.161279"},{"key":"e_1_3_1_68_1","unstructured":"Microsoft. 2023a. The Dafny Programming and Verification Language. https:\/\/dafny.org\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_69_1","unstructured":"Microsoft. 2023b. Microsoft Research. https:\/\/www.microsoft.com\/en-us\/research\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_70_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2013.35"},{"key":"e_1_3_1_71_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00205"},{"key":"e_1_3_1_72_1","author":"Nederpelt R.P.","year":"1994","unstructured":"R.P. Nederpelt, J.H. Geuvers, and R.C. de Vrijer (Eds.). 1994. Selected Papers on Automath. North Holland.","journal-title":"Selected Papers on Automath"},{"key":"e_1_3_1_73_1","volume-title":"Dafny Workshop at POPL","author":"Noble James","year":"2024","unstructured":"James Noble 2024. Learn\u2019em Dafny. In Dafny Workshop at POPL (London, England). https:\/\/popl24.sigplan.org\/details\/dafny-2024-papers\/11\/Learn-em-Dafny"},{"key":"e_1_3_1_74_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_23"},{"key":"e_1_3_1_75_1","doi-asserted-by":"publisher","unstructured":"OpenAI. 2023a. GPT-4 Technical Report. CoRR abs\/2303.08774 (2023).https:\/\/doi.org\/10.48550\/arXiv.2303.08774 10.48550\/arXiv.2303.08774","DOI":"10.48550\/arXiv.2303.08774"},{"key":"e_1_3_1_76_1","unstructured":"OpenAI. 2023b. OpenAI. https:\/\/platform.openai.com\/docs\/models. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_77_1","doi-asserted-by":"publisher","DOI":"10.18653\/V1\/2023.ACL-LONG.294"},{"key":"e_1_3_1_78_1","unstructured":"Alec Radford Karthik Narasimhan Tim Salimans Ilya Sutskever et al. 2018. Improving language understanding by generative pre-training. OpenAI.com"},{"key":"e_1_3_1_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3411763.3451760"},{"key":"e_1_3_1_80_1","doi-asserted-by":"publisher","DOI":"10.1561\/2500000045"},{"key":"e_1_3_1_81_1","unstructured":"Rohan Anil et al. 2023. PaLM 2 Technical Report. CoRR abs\/2305.10403 (2023)."},{"key":"e_1_3_1_82_1","article-title":"Code llama: Open foundation models for code","author":"Rozi\u00e8re Baptiste","year":"2023","unstructured":"Baptiste Rozi\u00e8re, Jonas Gehring, Fabian Gloeckle, Sten Sootla, Itai Gat, Xiaoqing Ellen Tan, Yossi Adi, Jingyu Liu, Tal Remez, J\u00e9r\u00e9my Rapin, et al. 2023. Code llama: Open foundation models for code. arXiv preprint arXiv:2308.12950 (2023).","journal-title":"arXiv preprint arXiv:2308.12950"},{"key":"e_1_3_1_83_1","doi-asserted-by":"publisher","DOI":"10.1186\/s13054-023-04473-y"},{"key":"e_1_3_1_84_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_3_1_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593374"},{"key":"e_1_3_1_86_1","unstructured":"seL4 Project. 2023. The seL4\u00ae Microkernel. https:\/\/sel4.systems\/. [Online] [Accessed: 2023-09-20]."},{"key":"e_1_3_1_87_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2015.24"},{"key":"e_1_3_1_88_1","doi-asserted-by":"publisher","DOI":"10.1145\/3579640"},{"key":"e_1_3_1_89_1","doi-asserted-by":"publisher","DOI":"10.1145\/3524842.3528009"},{"key":"e_1_3_1_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3340544"},{"key":"e_1_3_1_91_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510621"},{"key":"e_1_3_1_92_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE48619.2023.00203"},{"issue":"5","key":"e_1_3_1_93_1","first-page":"360","article-title":"Understanding interobserver agreement: the kappa statistic","volume":"37","author":"Viera Anthony J","year":"2005","unstructured":"Anthony J Viera, Joanne M Garrett, et al. 2005. Understanding interobserver agreement: the kappa statistic. Fam med 37, 5 (2005), 360\u2013363. https:\/\/pubmed.ncbi.nlm.nih.gov\/15883903\/","journal-title":"Fam med"},{"key":"e_1_3_1_94_1","doi-asserted-by":"crossref","unstructured":"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\u20131088. https:\/\/aclanthology.org\/2023.emnlp-main.68","DOI":"10.18653\/v1\/2023.emnlp-main.68"},{"key":"e_1_3_1_95_1","doi-asserted-by":"publisher","unstructured":"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 10.18653\/v1\/2021.emnlp-main.685","DOI":"10.18653\/v1\/2021.emnlp-main.685"},{"key":"e_1_3_1_96_1","doi-asserted-by":"publisher","DOI":"10.1145\/3485275"},{"key":"e_1_3_1_97_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4842-3829-5_6"},{"key":"e_1_3_1_98_1","unstructured":"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"},{"key":"e_1_3_1_99_1","volume-title":"Advances in Neural Information Processing Systems 35: Annual Conference on Neural Information Processing Systems 2022, NeurIPS 2022","author":"Wu Yuhuai","year":"2022","unstructured":"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"},{"key":"e_1_3_1_100_1","first-page":"6984","volume-title":"Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97)","author":"Yang Kaiyu","year":"2019","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to Prove Theorems via Interacting with Proof Assistants. In Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, USA (Proceedings of Machine Learning Research, Vol. 97), Kamalika Chaudhuri and Ruslan Salakhutdinov (Eds.). PMLR, 6984\u20136994. http:\/\/proceedings.mlr.press\/v97\/yang19a.html"},{"key":"e_1_3_1_101_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_1_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/3505243"},{"key":"e_1_3_1_103_1","article-title":"Towards A Correct-by-Construction FHE Model","volume":"281","author":"Yang Zhenkun","year":"2023","unstructured":"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","journal-title":"IACR Cryptol. ePrint Arch."},{"key":"e_1_3_1_104_1","first-page":"10799","volume-title":"Proceedings of the 37th International Conference on Machine Learning, ICML 2020, 13-18 July 2020, Virtual Event (Proceedings of Machine Learning Research, Vol. 119)","author":"Yasunaga Michihiro","year":"2020","unstructured":"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\u201310808. http:\/\/proceedings.mlr.press\/v119\/yasunaga20a.html"},{"key":"e_1_3_1_105_1","doi-asserted-by":"publisher","unstructured":"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 10.48550\/arXiv.2211.09066","DOI":"10.48550\/arXiv.2211.09066"}],"container-title":["Proceedings of the ACM on Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643763","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3643763","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:59:30Z","timestamp":1770191970000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3643763"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,7,12]]},"references-count":104,"journal-issue":{"issue":"FSE","published-print":{"date-parts":[[2024,7,12]]}},"alternative-id":["10.1145\/3643763"],"URL":"https:\/\/doi.org\/10.1145\/3643763","relation":{},"ISSN":["2994-970X"],"issn-type":[{"value":"2994-970X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,7,12]]}}}