{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,11]],"date-time":"2026-04-11T02:13:01Z","timestamp":1775873581232,"version":"3.50.1"},"publisher-location":"New York, NY, USA","reference-count":111,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T00:00:00Z","timestamp":1701302400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2210243"],"award-info":[{"award-number":["CCF-2210243"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000185","name":"Defense Advanced Research Projects Agency","doi-asserted-by":"publisher","award":["HR0011-22-9-0063"],"award-info":[{"award-number":["HR0011-22-9-0063"]}],"id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,11,30]]},"DOI":"10.1145\/3611643.3616243","type":"proceedings-article","created":{"date-parts":[[2023,11,30]],"date-time":"2023-11-30T23:14:38Z","timestamp":1701386078000},"page":"1229-1241","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":77,"title":["Baldur: Whole-Proof Generation and Repair with Large Language Models"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2896-2928","authenticated-orcid":false,"given":"Emily","family":"First","sequence":"first","affiliation":[{"name":"University of Massachusetts, Amherst, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-4795-7259","authenticated-orcid":false,"given":"Markus N.","family":"Rabe","sequence":"additional","affiliation":[{"name":"Augment Computing, Palo Alto, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1854-3321","authenticated-orcid":false,"given":"Talia","family":"Ringer","sequence":"additional","affiliation":[{"name":"University of Illinois, Urbana-Champaign, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3027-7986","authenticated-orcid":false,"given":"Yuriy","family":"Brun","sequence":"additional","affiliation":[{"name":"University of Massachusetts, Amherst, USA"}]}],"member":"320","published-online":{"date-parts":[[2023,11,30]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2944914"},{"key":"e_1_3_2_2_2_1","volume-title":"Proofster: Automated Formal Verification. In ICSE Demo.","author":"Agrawal Arpan","year":"2023","unstructured":"Arpan Agrawal, Emily First, Zhanna Kaufman, Tom Reichel, Shizhuo Zhang, Timothy Zhou, Alex Sanchez-Stern, Talia Ringer, and Yuriy Brun. 2023. Proofster: Automated Formal Verification. In ICSE Demo. Melbourne, Australia."},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11219-016-9312-z"},{"key":"e_1_3_2_2_4_1","volume-title":"Workshop MATH-AI: Toward Human-Level Mathematical Reasoning","author":"Azerbayev Zhangir","year":"2022","unstructured":"Zhangir Azerbayev, Bartosz Piotrowski, and Jeremy Avigad. 2022. ProofNet: A benchmark for autoformalizing and formally proving undergraduate-level mathematics problems. In Workshop MATH-AI: Toward Human-Level Mathematical Reasoning. New Orleans, LA, USA."},{"key":"e_1_3_2_2_5_1","first-page":"454","article-title":"HOList","author":"Bansal Kshitij","year":"2019","unstructured":"Kshitij Bansal, Sarah M. Loos, Markus N. Rabe, Christian Szegedy, and Stewart Wilcox. 2019. HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving. In ICML. 97, PMLR, Long Beach, CA, USA. 454\u2013463. http:\/\/proceedings.mlr.press\/v97\/bansal19a.html","journal-title":"In ICML. 97, PMLR, Long Beach, CA, USA."},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/2492061"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"crossref","unstructured":"Lasse Blaauwbroek Josef Urban and Herman Geuvers. 2020. The Tactician. In Intelligent Computer Mathematics. 271\u2013277.","DOI":"10.1007\/978-3-030-53518-6_17"},{"key":"e_1_3_2_2_8_1","doi-asserted-by":"publisher","unstructured":"Sidney Black. 2022. GPT-NeoX-20B: An Open-Source Autoregressive Language Model. In BigScience Episode #5 \u2014 Workshop on Challenges & Perspectives in Creating Large Language Models. 95\u2013136. https:\/\/doi.org\/10.18653\/v1\/2022.bigscience-1.9 10.18653\/v1\/2022.bigscience-1.9","DOI":"10.18653\/v1"},{"key":"e_1_3_2_2_9_1","unstructured":"Tom B. Brown. 2020. Language Models Are Few-Shot Learners. In NeurIPS."},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2017.8115630"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","unstructured":"Ahmet Celik Karl Palmskog and Milos Gligoric. 2018. A Regression Proof Selection Tool for Coq. In ICSE Demo Track. Gothenburg Sweden. 117\u2013120. https:\/\/doi.org\/10.1145\/3183440.3183493 10.1145\/3183440.3183493","DOI":"10.1145\/3183440.3183493"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2019.00057"},{"key":"e_1_3_2_2_13_1","first-page":"637","article-title":"Contract-based program repair without the contracts","author":"Chen Liushan","year":"2017","unstructured":"Liushan Chen, Yu Pei, and Carlo A. Furia. 2017. Contract-based program repair without the contracts. In ASE. Urbana, IL, USA. 637\u2013647.","journal-title":"ASE. Urbana, IL, USA."},{"key":"e_1_3_2_2_14_1","volume-title":"Evaluating Large Language Models Trained on Code. CoRR, abs\/2107.03374","author":"Chen Mark","year":"2021","unstructured":"Mark Chen. 2021. Evaluating Large Language Models Trained on Code. CoRR, abs\/2107.03374 (2021), arxiv:2107.03374"},{"key":"e_1_3_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2019.2940179"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2204.02311"},{"key":"e_1_3_2_2_17_1","volume-title":"Training Verifiers to Solve Math Word Problems. CoRR, abs\/2110.14168","author":"Cobbe Karl","year":"2021","unstructured":"Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Jacob Hilton, Reiichiro Nakano, Christopher Hesse, and John Schulman. 2021. Training Verifiers to Solve Math Word Problems. CoRR, abs\/2110.14168 (2021), arXiv:2110.14168. arxiv:2110.14168"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2301.02195"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-018-9458-4"},{"key":"e_1_3_2_2_20_1","volume-title":"Qlose: Program Repair with Quantitative Objectives. In CAV.","author":"D\u2019Antoni Loris","year":"2016","unstructured":"Loris D\u2019Antoni, Roopsha Samanta, and Rishabh Singh. 2016. Qlose: Program Repair with Quantitative Objectives. In CAV. Toronto, ON, Canada. 383\u2013401."},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3510003.3510138"},{"key":"e_1_3_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428299"},{"key":"e_1_3_2_2_24_1","volume-title":"Baldur: Whole-Proof Generation and Repair with Large Language Models. CoRR, abs\/2303.04910","author":"First Emily","year":"2023","unstructured":"Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. CoRR, abs\/2303.04910 (2023), arxiv:2303.04910"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106277"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-020-09580-x"},{"key":"e_1_3_2_2_27_1","volume-title":"Philip S. Thomas, and Scott Niekum.","author":"Giguere Stephen","year":"2022","unstructured":"Stephen Giguere, Blossom Metevier, Yuriy Brun, Bruno Castro da Silva, Philip S. Thomas, and Scott Niekum. 2022. Fairness Guarantees under Demographic Shift. In ICLR. https:\/\/openreview.net\/forum?id=wbPObLm6ueA"},{"key":"e_1_3_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192387"},{"key":"e_1_3_2_2_29_1","volume-title":"Shevade","author":"Gupta Rahul","year":"2017","unstructured":"Rahul Gupta, Soham Pal, Aditya Kanade, and Shirish K. Shevade. 2017. DeepFix: Fixing Common C Language Errors by Deep Learning. In AAAI. San Francisco, CA, USA. 1345\u20131351."},{"key":"e_1_3_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2206.01962"},{"key":"e_1_3_2_2_31_1","unstructured":"Jesse Michael Han Jason Rute Yuhuai Wu Edward W. Ayers and Stanislas Polu. 2022. Proof Artifact Co-Training for Theorem Proving with Language Models. In ICLR. https:\/\/openreview.net\/forum?id=rpxJc9j04U"},{"key":"e_1_3_2_2_32_1","doi-asserted-by":"publisher","unstructured":"Mark Harman. 2007. The Current State and Future of Search Based Software Engineering. In ICSE. 342\u2013357. https:\/\/doi.org\/10.1109\/FOSE.2007.29 10.1109\/FOSE.2007.29","DOI":"10.1109\/FOSE.2007.29"},{"key":"e_1_3_2_2_33_1","volume-title":"Measuring Mathematical Problem Solving With the MATH Dataset. CoRR, abs\/2103.03874","author":"Hendrycks Dan","year":"2021","unstructured":"Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. 2021. Measuring Mathematical Problem Solving With the MATH Dataset. CoRR, abs\/2103.03874 (2021), arxiv:2103.03874"},{"key":"e_1_3_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.152.5"},{"key":"e_1_3_2_2_35_1","volume-title":"ICLR), year =","author":"Huang Daniel","year":"2019","unstructured":"Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. [n. d.]. GamePad: A Learning Environment for Theorem Proving. In ICLR), year = 2019, url = https:\/\/openreview.net\/forum?id=r1xwKoR9Y7,."},{"key":"e_1_3_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3377812.3382156"},{"key":"e_1_3_2_2_37_1","volume-title":"Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In NeurIPS.","author":"Jiang Albert","year":"2022","unstructured":"Albert Jiang, Konrad Czechowski, Mateja Jamnik, Piotr Milos, Szymon Tworkowski, Wenda Li, and Yuhuai Tony Wu. 2022. Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers. In NeurIPS."},{"key":"e_1_3_2_2_38_1","volume-title":"Conference on Artificial Intelligence and Theorem Proving (AITP)","author":"Jiang Albert Qiaochu","year":"2021","unstructured":"Albert Qiaochu Jiang, Wenda Li, Jesse Michael Han, and Yuhuai Wu. 2021. LISA: Language models of ISAbelle proofs. In Conference on Artificial Intelligence and Theorem Proving (AITP). Aussois, France. 17.1\u201317.3."},{"key":"e_1_3_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2210.12283"},{"key":"e_1_3_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11432-018-1465-6"},{"key":"e_1_3_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213871"},{"key":"e_1_3_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2015.60"},{"key":"e_1_3_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2013.6606626"},{"key":"e_1_3_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1629575.1629596"},{"key":"e_1_3_2_2_45_1","doi-asserted-by":"publisher","unstructured":"Anil Koyuncu Kui Liu Tegawend\u00e9 F Bissyand\u00e9 Dongsun Kim Martin Monperrus Jacques Klein and Yves Le Traon. 2019. iFixR: Bug Report Driven Program Repair. In ESEC\/FSE. 314\u2013325. https:\/\/doi.org\/10.1145\/3338906.3338935 10.1145\/3338906.3338935","DOI":"10.1145\/3338906.3338935"},{"key":"e_1_3_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2205.11491"},{"key":"e_1_3_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158133"},{"key":"e_1_3_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1109\/SANER.2016.76"},{"key":"e_1_3_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2011.104"},{"key":"e_1_3_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/3318162"},{"key":"e_1_3_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_3_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2206.14858"},{"key":"e_1_3_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837617"},{"key":"e_1_3_2_2_54_1","doi-asserted-by":"publisher","unstructured":"Yiling Lou Ali Ghanbari Xia Li Lingming Zhang Haotian Zhang Dan Hao and Lu Zhang. 2020. Can Automated Program Repair Refine Fault Localization? A Unified Debugging Approach. In ISSTA. Virtual Event USA. 75\u201387. https:\/\/doi.org\/10.1145\/3395363.3397351 10.1145\/3395363.3397351","DOI":"10.1145\/3395363.3397351"},{"key":"e_1_3_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-06773-0_44"},{"key":"e_1_3_2_2_56_1","doi-asserted-by":"publisher","unstructured":"Sergey Mechtaev Manh-Dung Nguyen Yannic Noller Lars Grunske and Abhik Roychoudhury. 2018. Semantic Program Repair Using a Reference Implementation. In ICSE. 129\u2013139. isbn:978-1-4503-5638-1 https:\/\/doi.org\/10.1145\/3180155.3180247 10.1145\/3180155.3180247","DOI":"10.1145\/3180155.3180247"},{"key":"e_1_3_2_2_57_1","volume-title":"Thomas","author":"Metevier Blossom","year":"2019","unstructured":"Blossom Metevier, Stephen Giguere, Sarah Brockman, Ari Kobren, Yuriy Brun, Emma Brunskill, and Philip S. Thomas. 2019. Offline Contextual Bandits with High Probability Fairness Guarantees. In NeurIPS. Vancouver, BC, Canada. 14893\u201314904. http:\/\/papers.neurips.cc\/paper\/9630-offline-contextual-bandits-with-high-probability-fairness-guarantees"},{"key":"e_1_3_2_2_58_1","volume-title":"ICSE.","author":"Motwani Manish","unstructured":"Manish Motwani and Yuriy Brun. 2023. Better Automatic Program Repair by Using Bug Reports and Tests Together. In ICSE. Melbourne, Australia."},{"key":"e_1_3_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2020.2998785"},{"key":"e_1_3_2_2_60_1","doi-asserted-by":"publisher","unstructured":"K\u0131van\u00e7 Mu\u015flu Yuriy Brun and Alexandra Meliou. 2013. Data Debugging with Continuous Testing. In ESEC\/FSE New Ideas Track. Saint Petersburg Russia. 631\u2013634. https:\/\/doi.org\/10.1145\/2491411.2494580 10.1145\/2491411.2494580","DOI":"10.1145\/2491411.2494580"},{"key":"e_1_3_2_2_61_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771792"},{"key":"e_1_3_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/3238147.3238210"},{"key":"e_1_3_2_2_63_1","volume-title":"Junyi Jessy Li, and Milos Gligoric","author":"Nie Pengyu","year":"2020","unstructured":"Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2020. Deep Generation of Coq Lemma Names Using Elaborated Terms. In IJCAR. Paris, France. 97\u2013118."},{"key":"e_1_3_2_2_64_1","volume-title":"The Coq Workshop","author":"Nie Pengyu","year":"2020","unstructured":"Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2020. Learning to Format Coq Code Using Language Models. In The Coq Workshop. Aubervilliers, France."},{"key":"e_1_3_2_2_65_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE-Companion52605.2021.00026"},{"key":"e_1_3_2_2_66_1","volume-title":"Experience Report: How Effective is Automated Program Repair for Industrial Software? In SANER. 612\u2013616.","author":"Noda Kunihiro","year":"2020","unstructured":"Kunihiro Noda, Yusuke Nemoto, Keisuke Hotta, Hideo Tanida, and Shinji Kikuchi. 2020. Experience Report: How Effective is Automated Program Repair for Industrial Software? In SANER. 612\u2013616."},{"key":"e_1_3_2_2_67_1","volume-title":"Pretrained Language Models are Symbolic Mathematics Solvers too!. CoRR, abs\/2110.03501","author":"Noorbakhsh Kimia","year":"2021","unstructured":"Kimia Noorbakhsh, Modar Sulaiman, Mahdi Sharifi, Kallol Roy, and Pooyan Jamshidi. 2021. Pretrained Language Models are Symbolic Mathematics Solvers too!. CoRR, abs\/2110.03501 (2021), arxiv:2110.03501"},{"key":"e_1_3_2_2_68_1","volume-title":"Guy Gur-Ari, Henryk Michalewski, Jacob Austin, David Bieber, David Dohan, Aitor Lewkowycz, Maarten Bosma, David Luan, Charles Sutton, and Augustus Odena.","author":"Nye Maxwell I.","year":"2021","unstructured":"Maxwell I. Nye, Anders Johan Andreassen, Guy Gur-Ari, Henryk Michalewski, Jacob Austin, David Bieber, David Dohan, Aitor Lewkowycz, Maarten Bosma, David Luan, Charles Sutton, and Augustus Odena. 2021. Show Your Work: Scratchpads for Intermediate Computation with Language Models. CoRR, abs\/2112.00114 (2021)."},{"key":"e_1_3_2_2_69_1","volume-title":"AAAI and EAAI.","author":"Paliwal Aditya","unstructured":"Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. 2020. Graph Representations for Higher-Order Logic and Theorem Proving. In AAAI and EAAI. New York, NY, USA. 2967\u20132974."},{"key":"e_1_3_2_2_70_1","doi-asserted-by":"publisher","DOI":"10.1145\/3213846.3213877"},{"key":"e_1_3_2_2_71_1","volume-title":"The Sledgehammer: Let Automatic Theorem Provers write your Isabelle scripts!. https:\/\/isabelle.in.tum.de\/website-Isabelle2009-1\/sledgehammer.html","author":"Paulson Larry","year":"2023","unstructured":"Larry Paulson and Tobias Nipkow. 2023. The Sledgehammer: Let Automatic Theorem Provers write your Isabelle scripts!. https:\/\/isabelle.in.tum.de\/website-Isabelle2009-1\/sledgehammer.html"},{"key":"e_1_3_2_2_72_1","doi-asserted-by":"publisher","DOI":"10.1145\/3387940.3392180"},{"key":"e_1_3_2_2_73_1","volume-title":"Generative Language Modeling for Automated Theorem Proving. CoRR, abs\/2009.03393","author":"Polu Stanislas","year":"2020","unstructured":"Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. CoRR, abs\/2009.03393 (2020), arxiv:2009.03393"},{"key":"e_1_3_2_2_74_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2211.05102"},{"key":"e_1_3_2_2_75_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771791"},{"key":"e_1_3_2_2_76_1","article-title":"Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer","volume":"21","author":"Raffel Colin","year":"2020","unstructured":"Colin Raffel, Noam Shazeer, Adam Roberts, Katherine Lee, Sharan Narang, Michael Matena, Yanqi Zhou, Wei Li, and Peter J. Liu. 2020. Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformer. Journal of Machine Learning Research, 21 (2020), 140:1\u2013140:67. http:\/\/jmlr.org\/papers\/v21\/20-074.html","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_3_2_2_77_1","unstructured":"Talia Ringer. 2021. Proof Repair. Ph. D. Dissertation. University of Washington."},{"key":"e_1_3_2_2_78_1","doi-asserted-by":"publisher","DOI":"10.1561\/9781680835953"},{"key":"e_1_3_2_2_79_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373823"},{"key":"e_1_3_2_2_80_1","volume-title":"Prasad","author":"Saha Ripon K.","year":"2017","unstructured":"Ripon K. Saha, Yingjun Lyu, Hiroaki Yoshida, and Mukul R. Prasad. 2017. ELIXIR: Effective object oriented program repair. In ASE. 648\u2013659."},{"key":"e_1_3_2_2_81_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICSE.2019.00020"},{"key":"e_1_3_2_2_82_1","doi-asserted-by":"publisher","DOI":"10.1145\/3394450.3397466"},{"key":"e_1_3_2_2_83_1","doi-asserted-by":"publisher","DOI":"10.1145\/3593374"},{"key":"e_1_3_2_2_84_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1911.02150"},{"key":"e_1_3_2_2_85_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786825"},{"key":"e_1_3_2_2_86_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2104.09864"},{"key":"e_1_3_2_2_87_1","doi-asserted-by":"publisher","DOI":"10.1109\/COMPSAC.2018.00030"},{"key":"e_1_3_2_2_88_1","unstructured":"The Coq Development Team. 2017. Coq v.8.7. https:\/\/coq.inria.fr"},{"key":"e_1_3_2_2_89_1","doi-asserted-by":"publisher","DOI":"10.1126\/science.aag3311"},{"key":"e_1_3_2_2_90_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416532"},{"key":"e_1_3_2_2_91_1","volume-title":"ESEC\/FSE.","author":"Tian Yuchi","unstructured":"Yuchi Tian and Baishakhi Ray. 2017. Automatically diagnosing and repairing error handling bugs in C. In ESEC\/FSE. Paderborn, Germany. 752\u2013762."},{"key":"e_1_3_2_2_92_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.1609.03499"},{"key":"e_1_3_2_2_93_1","volume-title":"\u0141 ukasz Kaiser, and Illia Polosukhin","author":"Vaswani Ashish","year":"2017","unstructured":"Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, \u0141 ukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In NeurIPS."},{"key":"e_1_3_2_2_94_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192384"},{"key":"e_1_3_2_2_95_1","doi-asserted-by":"publisher","DOI":"10.1145\/3324884.3416590"},{"key":"e_1_3_2_2_96_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2208.11744"},{"key":"e_1_3_2_2_97_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2201.11903"},{"key":"e_1_3_2_2_98_1","doi-asserted-by":"publisher","DOI":"10.1109\/ASE.2013.6693094"},{"key":"e_1_3_2_2_99_1","doi-asserted-by":"publisher","unstructured":"Ming Wen Junjie Chen Rongxin Wu Dan Hao and Shing-Chi Cheung. 2018. Context-Aware Patch Generation for Better Automated Program Repair. In ICSE. Gothenburg Sweden. 1\u201311. https:\/\/doi.org\/10.1145\/3180155.3180233 10.1145\/3180155.3180233","DOI":"10.1145\/3180155.3180233"},{"key":"e_1_3_2_2_100_1","unstructured":"Minchao Wu Michael Norrish Christian Walder and Amir Dezfouli. 2021. TacticZero: Learning to Prove Theorems from Scratch with Deep Learning. In NeurIPS. https:\/\/openreview.net\/forum?id=edmYVRkYZv"},{"key":"e_1_3_2_2_101_1","doi-asserted-by":"publisher","DOI":"10.48550\/ARXIV.2205.12615"},{"key":"e_1_3_2_2_102_1","doi-asserted-by":"publisher","DOI":"10.1145\/3092703.3092718"},{"key":"e_1_3_2_2_103_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-04272-1_3"},{"key":"e_1_3_2_2_104_1","doi-asserted-by":"publisher","DOI":"10.1145\/3106237.3106274"},{"key":"e_1_3_2_2_105_1","unstructured":"Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In ICML. 6984\u20136994."},{"key":"e_1_3_2_2_106_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993532"},{"key":"e_1_3_2_2_107_1","volume-title":"Break-it-fix-it: Unsupervised learning for program repair. In ICML. 11941\u201311952.","author":"Yasunaga Michihiro","year":"2021","unstructured":"Michihiro Yasunaga and Percy Liang. 2021. Break-it-fix-it: Unsupervised learning for program repair. In ICML. 11941\u201311952."},{"key":"e_1_3_2_2_108_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-020-09920-w"},{"key":"e_1_3_2_2_109_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10664-018-9619-4"},{"key":"e_1_3_2_2_110_1","volume-title":"Jesse Michael Han, and Stanislas Polu","author":"Zheng Kunhao","year":"2022","unstructured":"Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. In ICLR. https:\/\/openreview.net\/forum?id=9ZPegFuFTFv"},{"key":"e_1_3_2_2_111_1","doi-asserted-by":"publisher","DOI":"10.1145\/3468264.3468544"}],"event":{"name":"ESEC\/FSE '23: 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering","location":"San Francisco CA USA","acronym":"ESEC\/FSE '23","sponsor":["SIGSOFT ACM Special Interest Group on Software Engineering"]},"container-title":["Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3616243","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3611643.3616243","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:36:03Z","timestamp":1750178163000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3611643.3616243"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,30]]},"references-count":111,"alternative-id":["10.1145\/3611643.3616243","10.1145\/3611643"],"URL":"https:\/\/doi.org\/10.1145\/3611643.3616243","relation":{},"subject":[],"published":{"date-parts":[[2023,11,30]]},"assertion":[{"value":"2023-11-30","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}