Elamur Research⌕
☰
home / papers / 2023 / Baldur: Whole-Proof Generation and Repair with Large Language Models

Baldur: Whole-Proof Generation and Repair with Large Language Models

Paper · 2023 · Emily First, Markus N. Rabe, Talia Ringer et al.

Summary

Writing machine-checked proofs for software verification is very costly. Earlier neural provers reduce this by predicting one tactic at a time and searching over proof states, which requires constant back-and-forth between a GPU-hosted model and a CPU-bound proof assistant. Baldur takes a simpler route. It fine-tunes the Minerva LLM (8B and 62B parameters, pretrained on mathematical text) to output a complete Isabelle/HOL proof from the theorem statement alone, and Isabelle then checks the result. To build the training data, the authors stitched step-level examples from the PISA dataset back into full proofs and discarded the intermediate proof states. Two extensions are layered on top. A repair model takes a failed attempt plus Isabelle's error message and tries again. Theory-file context adds the lines that precede the theorem in its source file. On 6,336 test theorems, whole-proof generation matches or beats search-based methods without any search, and Baldur proves many theorems that the state-of-the-art tool Thor misses. This suggests that LLMs are a practical, complementary path toward automating formal verification.

Key points

  • Data: Evaluation uses the PISA dataset of 183K Isabelle/HOL theorems, with 6,336 held out for testing. Baldur alone (without repair) proves 47.9% of them, compared with 39.0% for a prior search-based method.
  • Repair: Feeding the model a failed proof together with the error message proves 1.5% more theorems, even at equal compute. The error message is the key ingredient.
  • Context: Adding theory-file context raises the success rate from 40.7% to 47.5% at the same model size. The larger Minerva model also outperforms the 8B one.
  • Ensembles and combination: An ensemble of 10 fine-tuned Baldur models reaches 58.0%. Combined with Thor, Baldur proves 65.7%, compared with 57.0% for Thor alone (+8.7 points).
  • Example: Baldur can find induction-based proofs that Sledgehammer cannot produce by default.

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 Illinois Urbana-ChampaignUrbana · United States209 works · 71,394 citations🎓University of Massachusetts AmherstAmherst Center · United States114 works · 68,731 citations

 Fields, topics and concepts

📚 Shelves 4The field of science this work belongs to (OpenAlex fields).Computer Science · 18,614 worksArtificial Intelligence · 17,965 worksComputational Theory and Mathematics · 321 worksSoftware · 119 works

Cite

Cite as Emily First, Markus N. Rabe, Talia Ringer and Yuriy Brun. 2023. Baldur: Whole-Proof Generation and Repair with Large Language Models. arXiv:2303.04910.

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

@misc{first2023baldur,
  title = {{Baldur: Whole-Proof Generation and Repair with Large Language Models}},
  author = {Emily First, Markus N. Rabe, Talia Ringer and Yuriy Brun},
  year = {2023},
  doi = {10.48550/arxiv.2303.04910},
  eprint = {2303.04910},
  archivePrefix = {arXiv},
  url = {https://doi.org/10.48550/arxiv.2303.04910}
}

References

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

  1. Afsoon Afzal, Manish Motwani, Kathryn T. Stolee, Yuriy Brun, and Claire Le Goues. 2021. SOSRepair: Expressive Semantic Search for Real-World Program Repair. TSE 47, 10 (October 2021), 2162–2181. https://doi.org/10.1109/TSE.2019.2944914 — [doi:10.1109/tse.2019.2944914](https://doi.org/10.1109/tse.2019.2944914) ↗
  2. Fatmah Yousef Assiri and James M Bieman. 2017. Fault Localization for Automated Program Repair: Effectiveness, Performance, Repair Correctness. Software Quality Journal 25, 1 (2017), 171–199. https://doi.org/10.1007/s11219-016-9312-z — [doi:10.1007/s11219-016-9312-z](https://doi.org/10.1007/s11219-016-9312-z) ↗
  3. 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, Louisiana, USA. find
  4. 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 Proceedings of the 36th International Conference on Machine Learning, ICML 2019, 9-15 June 2019, Long Beach, California, U…
  5. Lasse Blaauwbroek, Josef Urban, and Herman Geuvers. 2020. The Tactician. In Intelligent Computer Mathematics, Christoph Benzmüller and Bruce Miller (Eds.). Springer International Publishing, Cham, 271–277. find
  6. Sidney Black, Stella Biderman, Eric Hallahan, Quentin Anthony, Leo Gao, Laurence Golding, Horace He, Connor Leahy, Kyle McDonell, Jason Phang, Michael Pieler, Usvsn Sai Prashanth, Shivanshu Purohit, Laria Reynolds, Jonathan Tow, Ben Wang, and Samuel Weinbach. 2022. GPT-NeoX-20B: An Open-Source Autor…
  7. Tom B. Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared Kaplan, Prafulla Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell, Sandhini Agarwal, Ariel Herbert-Voss, Gretchen Krueger, Tom Henighan, Rewon Child, Aditya Ramesh, Daniel M. Ziegler, Jeffrey Wu, Clemens Winter,… — Language Models are Few-Shot Learners
  8. Ahmet Celik, Karl Palmskog, and Milos Gligoric. 2017. ICoq: Regression proof selection for large-scale verification projects. In IEEE/ACM International Conference on Automated Software Engineering (ASE). Urbana-Champaign, IL, USA, 171–182. https://doi.org/10.1109/ASE.2017.8115630 — [doi:10.1109/ase.2017.8115630](https://doi.org/10.1109/ase.2017.8115630) ↗
  9. Ahmet Celik, Karl Palmskog, and Milos Gligoric. 2018. A Regression Proof Selection Tool for Coq. In International Conference on Software Engineering Demonstrations Track (ICSE DEMO). Gothenburg, Sweden, 117–120. https://doi.org/10.1145/3183440.3183493 — [doi:10.1145/3183440.3183493](https://doi.org/10.1145/3183440.3183493) ↗
  10. Ahmet Celik, Karl Palmskog, Marinela Parovic, Emilio Jesús Gallego Arias, and Milos Gligoric. 2019. Mutation Analysis for Coq. In IEEE/ACM International Conference on Automated Software Engineering (ASE). San Diego, California, 539–551. https://doi.org/10.1109/ASE.2019.00057 — [doi:10.1109/ase.2019.00057](https://doi.org/10.1109/ase.2019.00057) ↗
  11. Liushan Chen, Yu Pei, and Carlo A. Furia. 2017. Contract-based program repair without the contracts. In IEEE/ACM International Conference on Automated Software Engineering (ASE). Urbana, IL, USA, 637–647. find
  12. Mark Chen, Jerry Tworek, Heewoo Jun, Qiming Yuan, Henrique Ponde de Oliveira Pinto, Jared Kaplan, Harrison Edwards, Yuri Burda, Nicholas Joseph, Greg Brockman, Alex Ray, Raul Puri, Gretchen Krueger, Michael Petrov, Heidy Khlaaf, Girish Sastry, Pamela Mishkin, Brooke Chan, Scott Gray, Nick Ryder, Mik… — Evaluating Large Language Models Trained on Code
  13. Zimin Chen, Steve James Kommrusch, Michele Tufano, Louis-Noël Pouchet, Denys Poshyvanyk, and Martin Monperrus. 2019. Sequencer: Sequence-to-sequence learning for end-to-end program repair. TSE 47, 9 (2019), 1943–1959. https://doi.org/10.1109/TSE.2019.2940179 ↗
  14. Aakanksha Chowdhery, Sharan Narang, Jacob Devlin, Maarten Bosma, Gaurav Mishra, Adam Roberts, Paul Barham, Hyung Won Chung, Charles Sutton, Sebastian Gehrmann, Parker Schuh, Kensen Shi, Sasha Tsvyashchenko, Joshua Maynez, Abhishek Rao, Parker Barnes, Yi Tay, Noam Shazeer, Vinodkumar Prabhakaran, Emi… — PaLM: Scaling Language Modeling with Pathways
  15. 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 https://arxiv.org/abs/2110.14168 ↗
  16. Garett Cunningham, Razvan C. Bunescu, and David Juedes. 2023. Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofs. https://doi.org/10.48550/ARXIV.2301.02195 ↗
  17. Łukasz Czajka and Cezary Kaliszyk. 2018. Hammer for Coq: Automation for Dependent Type Theory. Journal of Automated Reasoning 61, 1-4 (2018), 423–453. https://doi.org/10.1007/s10817-018-9458-4 ↗
  18. Loris D’Antoni, Roopsha Samanta, and Rishabh Singh. 2016. Qlose: Program Repair with Quantitative Objectives. In International Conference on Computer Aided Verification (CAV). Toronto, ON, Canada, 383–401. find
  19. Angela Fan, Mike Lewis, and Yann Dauphin. 2018. Hierarchical Neural Story Generation. In Proceedings of the 56th Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers). Association for Computational Linguistics, Melbourne, Australia, 889–898. https://doi.org/10.18653…
  20. Emily First and Yuriy Brun. 2022. Diversity-Driven Automated Formal Verification. In International Conference on Software Engineering (ICSE). Pittsburgh, PA, 749–761. https://doi.org/10.1145/3510003.3510138 — [doi:10.1145/3510003.3510138](https://doi.org/10.1145/3510003.3510138) ↗
  21. Emily First and Yuriy Brun. 2022. Diversity-Driven Automated Formal Verification. In ICSE (22–27). 749–761. https://doi.org/10.1145/3510003.3510138 — [doi:10.1145/3510003.3510138](https://doi.org/10.1145/3510003.3510138) ↗
  22. Emily First, Yuriy Brun, and Arjun Guha. 2020. TacTok: Semantics-Aware Proof Synthesis. PACMPL OOPSLA 4 (November 2020), 231:1–231:31. https://doi.org/10.1145/3428299 — [doi:10.1145/3428299](https://doi.org/10.1145/3428299) ↗
  23. Thibault Gauthier, Cezary Kaliszyk, Josef Urban, Ramana Kumar, and Michael Norrish. 2021. TacticToe: Learning to Prove with Tactics. J. Autom. Reason. 65, 2 (feb 2021), 257–286. https://doi.org/10.1007/s10817-020-09580-x ↗
  24. Sumit Gulwani, Ivan Radiček, and Florian Zuleger. 2018. Automated Clustering and Program Repair for Introductory Programming Assignments. In PLDI. 465– 480. https://doi.org/10.1145/3192366.3192387 — [doi:10.1145/3192366.3192387](https://doi.org/10.1145/3192366.3192387) ↗
  25. Rahul Gupta, Soham Pal, Aditya Kanade, and Shirish K. Shevade. 2017. DeepFix: Fixing Common C Language Errors by Deep Learning. In AAAI. find
  26. Christopher Hahn, Frederik Schmitt, Julia J. Tillman, Niklas Metzger, Julian Siber, and Bernd Finkbeiner. 2022. Formal Specifications from Natural Language. CoRR abs/2206.01962 (2022). https://doi.org/10.48550/arXiv.2206.01962 arXiv:2206.01962 — [doi:10.48550/arxiv.2206.01962](https://doi.org/10.48550/arxiv.2206.01962) ↗
  27. 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 The Tenth International Conference on Learning Representations, ICLR 2022, Virtual Event, April 25-29, 2022. OpenReview.net. https://openreview…
  28. Mark Harman. 2007. The Current State and Future of Search Based Software Engineering. In ACM/IEEE International Conference on Software Engineering (ICSE). 342–357. https://doi.org/10.1109/FOSE.2007.29 — [doi:10.1109/fose.2007.29](https://doi.org/10.1109/fose.2007.29) ↗
  29. 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 https://arxiv.org/abs/2103.03874 ↗
  30. Jónathan Heras and Ekaterina Komendantskaya. 2014. ACL2(ml): Machine-learning for ACL2. Electronic Proceedings in Theoretical Computer Science 152 (04 2014). https://doi.org/10.4204/EPTCS.152.5 — [doi:10.4204/eptcs.152.5](https://doi.org/10.4204/eptcs.152.5) ↗
  31. Daniel Huang, Prafulla Dhariwal, Dawn Song, and Ilya Sutskever. 2019. GamePad: A Learning Environment for Theorem Proving. In 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, May 6-9, 2019. OpenReview.net. https://openreview.net/forum?id=r1xwKoR9Y7 ↗
  32. Kush Jain, Karl Palmskog, Ahmet Celik, Emilio Jesús Gallego Arias, and Milos Gligoric. 2020. MCoq: Mutation Analysis for Coq Verification Projects. In International Conference on Software Engineering Demonstrations Track (ICSE DEMO). Seoul, South Korea, 89–92. https://doi.org/10.1145/3377812.3382156 — [doi:10.1145/3377812.3382156](https://doi.org/10.1145/3377812.3382156) ↗
  33. 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 Neural Information Processing Systems (NeurIPS).
  34. 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–17.3. find
  35. Albert Q. Jiang, Sean Welleck, Jin Peng Zhou, Wenda Li, Jiacheng Liu, Mateja Jamnik, Timothée Lacroix, Yuhuai Wu, and Guillaume Lample. 2022. Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs. CoRR abs/2210.12283 (2022). https://doi.org/10.48550/arXiv.2210.12283 arXiv:221… ↗
  36. Jiajun Jiang, Yingfei Xiong, and Xin Xia. 2019. A manual inspection of Defects4J bugs and its implications for automatic program repair. Science China Information Sciences 62, 10 (2019), 200102. find
  37. Jiajun Jiang, Yingfei Xiong, Hongyu Zhang, Qing Gao, and Xiangqun Chen. 2018. Shaping Program Repair Space with Existing Patches and Similar Code. In ISSTA. https://doi.org/10.1145/3213846.3213871 — [doi:10.1145/3213846.3213871](https://doi.org/10.1145/3213846.3213871) ↗
  38. Yalin Ke, Kathryn T. Stolee, Claire Le Goues, and Yuriy Brun. 2015. Repairing Programs with Semantic Code Search. In ASE (9–13). 295–306. https://doi.org/10.1109/ASE.2015.60 — [doi:10.1109/ase.2015.60](https://doi.org/10.1109/ase.2015.60) ↗
  39. Dongsun Kim, Jaechang Nam, Jaewoo Song, and Sunghun Kim. 2013. Automatic patch generation learned from human-written patches. In ACM/IEEE International Conference on Software Engineering (ICSE). San Francisco, CA, USA, 802–811. http://dl.acm.org/citation.cfm?id=2486788.2486893 ↗
  40. Gerwin Klein, Kevin Elphinstone, Gernot Heiser, June Andronick, David 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 ACM SIGOPS 22nd Symposi… find
  41. Anil Koyuncu, Kui Liu, Tegawendé F Bissyandé, Dongsun Kim, Martin Monperrus, Jacques Klein, and Yves Le Traon. 2019. iFixR: Bug Report Driven Program Repair. In ESEC/FSE. 314–325. https://doi.org/10.1145/3338906.3338935 — [doi:10.1145/3338906.3338935](https://doi.org/10.1145/3338906.3338935) ↗
  42. Guillaume Lample, Marie-Anne Lachaux, Thibaut Lavril, Xavier Martinet, Amaury Hayat, Gabriel Ebner, Aurélien Rodriguez, and Timothée Lacroix. 2022. HyperTree Proof Search for Neural Theorem Proving. CoRR abs/2205.11491 (2022). https://doi.org/10.48550/arXiv.2205.11491 arXiv:2205.11491 ↗
  43. Leonidas Lampropoulos, Zoe Paraskevopoulou, and Benjamin C. Pierce. 2017. Generating Good Generators for Inductive Relations. Proceedings of the ACM on Programming Languages (PACMPL) 2, POPL (Dec. 2017), 45:1–45:30. https://doi.org/10.1145/3158133 — [doi:10.1145/3158133](https://doi.org/10.1145/3158133) ↗
  44. Xuan Bach D. Le, David Lo, and Claire Le Goues. 2016. History Driven Program Repair. In Intl. Conf. on Software Analysis, Evolution, and Reengineering, Vol. 1. 213–224. https://doi.org/10.1109/SANER.2016.76 — [doi:10.1109/saner.2016.76](https://doi.org/10.1109/saner.2016.76) ↗
  45. Claire Le Goues, ThanhVu Nguyen, Stephanie Forrest, and Westley Weimer. 2012. GenProg: A Generic Method for Automatic Software Repair. IEEE Transactions on Software Engineering (TSE) 38 (2012), 54–72. https://doi.org/10.1109/TSE.2011.104 ↗
  46. Claire Le Goues, Michael Pradel, and Abhik Roychoudhury. 2019. Automated Program Repair. CACM 62, 12 (Nov. 2019), 56–65. https://doi.org/10.1145/3318162 — [doi:10.1145/3318162](https://doi.org/10.1145/3318162) ↗
  47. Xavier Leroy. 2009. Formal Verification of a Realistic Compiler. ACM 52, 7 (July 2009), 107–115. https://doi.org/10.1145/1538788.1538814 ↗
  48. Aitor Lewkowycz, Anders Andreassen, David Dohan, Ethan Dyer, Henryk Michalewski, Vinay V. Ramasesh, Ambrose Slone, Cem Anil, Imanol Schlag, Theo Gutman-Solo, Yuhuai Wu, Behnam Neyshabur, Guy Gur-Ari, and Vedant Misra. 2022. Solving Quantitative Reasoning Problems with Language Models. CoRR abs/2206.…
  49. Fan Long and Martin Rinard. 2016. Automatic Patch Generation by Learning Correct Code. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). St. Petersburg, FL, USA, 298–312. https://doi.org/10.1145/2837614.2837617 ↗
  50. 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. 75–87. https://doi.org/10.1145/3395363.3397351 — [doi:10.1145/3395363.3397351](https://doi.org/10.1145/3395363.3397351) ↗
  51. Paolo Masci and Aaron Dutle. 2022. Proof Mate: An Interactive Proof Helper for PVS (Tool Paper). In NASA Formal Methods Symposium. Springer, 809–815. find
  52. Sergey Mechtaev, Manh-Dung Nguyen, Yannic Noller, Lars Grunske, and Abhik Roychoudhury. 2018. Semantic Program Repair Using a Reference Implementation. In ICSE. 129–139. https://doi.org/10.1145/3180155.3180247 — [doi:10.1145/3180155.3180247](https://doi.org/10.1145/3180155.3180247) ↗
  53. Manish Motwani and Yuriy Brun. 2023. Better Automatic Program Repair by Using Bug Reports and Tests Together. In International Conference on Software Engineering (ICSE) (14–20). Melbourne, Australia. find
  54. Manish Motwani, Mauricio Soto, Yuriy Brun, René Just, and Claire Le Goues. 2022. Quality of Automated Program Repair on Real-World Defects. TSE 48, 2 (February 2022), 637–661. https://doi.org/10.1109/TSE.2020.2998785 — [doi:10.1109/tse.2020.2998785](https://doi.org/10.1109/tse.2020.2998785) ↗
  55. Yutaka Nagashima and Yilun He. 2018. PaMpeR: Proof Method Recommendation System for Isabelle/HOL. In International Conference on Automated Software Engineering (ASE). Montpellier, France, 362–372. https://doi.org/10.1145/3238147.3238210 ↗
  56. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2020. Deep Generation of Coq Lemma Names Using Elaborated Terms. In International Joint Conference on Automated Reasoning (IJCAR). Paris, France, 97–118. find
  57. 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. find
  58. Pengyu Nie, Karl Palmskog, Junyi Jessy Li, and Milos Gligoric. 2021. Roosterize: Suggesting Lemma Names for Coq Verification Projects Using Deep Learning. In International Conference on Software Engineering Demonstrations Track (ICSE DEMO). Madrid, Spain, 21–24. https://doi.org/10.1109/ICSE-Companio… — [doi:10.1109/icse-companion52605.2021.00026](https://doi.org/10.1109/icse-companion52605.2021.00026) ↗
  59. 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–616. find
  60. 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). https://arxiv.org/abs/2110.03501 ↗
  61. 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…
  62. Aditya Paliwal, Sarah M. Loos, Markus N. Rabe, Kshitij Bansal, and Christian Szegedy. 2020. Graph Representations for Higher-Order Logic and Theorem Proving. In The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, The Thirty-Second Innovative Applications of Artificial Intelligen… find
  63. Karl Palmskog, Ahmet Celik, and Milos Gligoric. 2018. PiCoq: Parallel Regression Proving for Large-Scale Verification Projects. In ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). Amsterdam, Netherlands, 344–355. https://doi.org/10.1145/3213846.3213877 — [doi:10.1145/3213846.3213877](https://doi.org/10.1145/3213846.3213877) ↗
  64. 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. ↗
  65. Justyna Petke and Aymeric Blot. 2018. Refining Fitness Functions in Test-Based Program Repair. In APR. 13–14. https://doi.org/10.1145/3387940.3392180 — [doi:10.1145/3387940.3392180](https://doi.org/10.1145/3387940.3392180) ↗
  66. Stanislas Polu and Ilya Sutskever. 2020. Generative Language Modeling for Automated Theorem Proving. CoRR abs/2009.03393 (2020). arXiv:2009.03393 https://arxiv.org/abs/2009.03393 ↗
  67. Reiner Pope, Sholto Douglas, Aakanksha Chowdhery, Jacob Devlin, James Bradbury, Anselm Levskaya, Jonathan Heek, Kefan Xiao, Shivani Agrawal, and Jeff Dean. 2022. Efficiently Scaling Transformer Inference. https://doi.org/10.48550/ARXIV.2211.05102 ↗
  68. Zichao Qi, Fan Long, Sara Achour, and Martin Rinard. 2015. An Analysis of Patch Plausibility and Correctness for Generate-and-validate Patch Generation Systems. In ISSTA. 24–36. https://doi.org/10.1145/2771783.2771791 — [doi:10.1145/2771783.2771791](https://doi.org/10.1145/2771783.2771791) ↗
  69. 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. J. Mach. Learn. Res. 21 (2020), 140:1–140:67. http://jmlr.org/papers/v21/20-074.html ↗
  70. Talia Ringer. 2021. Proof Repair. Ph. D. Dissertation. University of Washington. find
  71. Talia Ringer, Karl Palmskog, Ilya Sergey, Milos Gligoric, Zachary Tatlock, et al. 2019. QED at large: A survey of engineering of formally verified software. Foundations and Trends® in Programming Languages 5, 2-3 (2019), 102–281. find
  72. Talia Ringer, Alex Sanchez-Stern, Dan Grossman, and Sorin Lerner. 2020. REPLica: REPL Instrumentation for Coq Analysis. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (New Orleans, LA, USA) (CPP 2020). Association for Computing Machinery, New York, NY… — [doi:10.1145/3372885.3373823](https://doi.org/10.1145/3372885.3373823) find
  73. Ripon K. Saha, Yingjun Lyu, Hiroaki Yoshida, and Mukul R. Prasad. 2017. ELIXIR: Effective object oriented program repair. In ASE. 648–659. find
  74. Seemanta Saha, Ripon K. Saha, and Mukul R. Prasad. 2019. Harnessing Evolution for Multi-Hunk Program Repair. In ACM/IEEE International Conference on Software Engineering (ICSE) (29–31). Montreal, QC, Canada, 13–24. https://doi.org/10.1109/ICSE.2019.00020 — [doi:10.1109/icse.2019.00020](https://doi.org/10.1109/icse.2019.00020) ↗
  75. Alex Sanchez-Stern, Yousef Alhessi, Lawrence 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 (London, UK) (MAPL 2020). Association for Computing Machinery, New… find
  76. Alex Sanchez-Stern, Emily First, Timothy Zhou, Zhanna Kaufman, Yuriy Brun, and Talia Ringer. 2023. Passport: Improving Automated Formal Verification Using Identifiers. ACM TOPLAS (2023). find
  77. Noam Shazeer. 2019. Fast Transformer Decoding: One Write-Head is All You Need. CoRR abs/1911.02150 (2019). arXiv:1911.02150 http://arxiv.org/abs/1911.02150 ↗
  78. Edward K. Smith, Earl Barr, Claire Le Goues, and Yuriy Brun. 2015. Is the Cure Worse than the Disease? Overfitting in Automated Program Repair. In ESEC/FSE. 532–543. https://doi.org/10.1145/2786805.2786825 — [doi:10.1145/2786805.2786825](https://doi.org/10.1145/2786805.2786825) ↗
  79. Jianlin Su, Yu Lu, Shengfeng Pan, Bo Wen, and Yunfeng Liu. 2021. RoFormer: Enhanced Transformer with Rotary Position Embedding. CoRR abs/2104.09864 (2021). arXiv:2104.09864 https://arxiv.org/abs/2104.09864 ↗
  80. Shuyao Sun, Junxia Guo, Ruilian Zhao, and Zheng Li. 2018. Search-Based Efficient Automated Program Repair Using Mutation and Fault Localization. In COMPSAC, Vol. 1. 174–183. https://doi.org/10.1109/COMPSAC.2018.00030 — [doi:10.1109/compsac.2018.00030](https://doi.org/10.1109/compsac.2018.00030) ↗
  81. The Coq Development Team. 2017. Coq, v.8.7. https://coq.inria.fr. ↗
  82. Haoye Tian, Kui Liu, Abdoul Kader Kaboré, Anil Koyuncu, Li Li, Jacques Klein, and Tegawendé F. Bissyandé. 2020. Evaluating Representation Learning of Code Changes for Predicting Patch Correctness in Program Repair. In ASE. https://doi.org/10.1145/3324884.3416532 — [doi:10.1145/3324884.3416532](https://doi.org/10.1145/3324884.3416532) ↗
  83. Yuchi Tian and Baishakhi Ray. 2017. Automatically diagnosing and repairing error handling bugs in C. In European Software Engineering Conference and ACM SIGSOFT International Symposium on Foundations of Software Engineering (ESEC/FSE). Paderborn, Germany, 752–762. find
  84. Aäron van den Oord, Sander Dieleman, Heiga Zen, Karen Simonyan, Oriol Vinyals, Alex Graves, Nal Kalchbrenner, Andrew W. Senior, and Koray Kavukcuoglu. 2016. WaveNet: A Generative Model for Raw Audio. CoRR abs/1609.03499 (2016). arXiv:1609.03499 http://arxiv.org/abs/1609.03499 ↗
  85. Ashish Vaswani, Noam Shazeer, Niki Parmar, Jakob Uszkoreit, Llion Jones, Aidan N Gomez, Łukasz Kaiser, and Illia Polosukhin. 2017. Attention is all you need. In NeurIPS.
  86. Ke Wang, Rishabh Singh, and Zhendong Su. 2018. Search, align, and repair: Data-driven feedback generation for introductory programming exercises. In PLDI. 481–495. https://doi.org/10.1145/3296979.3192384 — [doi:10.1145/3296979.3192384](https://doi.org/10.1145/3296979.3192384) ↗
  87. Shangwen Wang, Ming Wen, Bo Lin, Hongjun Wu, Yihao Qin, Deqing Zou, Xiaoguang Mao, and Hai Jin. 2020. Automated Patch Correctness Assessment: How Far Are We?. In ASE. Association for Computing Machinery, 968–980. https://doi.org/10.1145/3324884.3416590 — [doi:10.1145/3324884.3416590](https://doi.org/10.1145/3324884.3416590) ↗
  88. Jason Wei, Xuezhi Wang, Dale Schuurmans, Maarten Bosma, Ed H. Chi, Quoc Le, and Denny Zhou. 2022. Chain of Thought Prompting Elicits Reasoning in Large Language Models. CoRR abs/2201.11903 (2022). arXiv:2201.11903 https://arxiv.org/abs/2201.11903 ↗
  89. Westley Weimer, Zachary P. Fry, and Stephanie Forrest. 2013. Leveraging Program Equivalence for Adaptive Program Repair: Models and First Results. In IEEE/ACM International Conference on Automated Software Engineering (ASE). Palo Alto, CA, USA, 356–366. find
  90. Ming Wen, Junjie Chen, Rongxin Wu, Dan Hao, and Shing-Chi Cheung. 2018. Context-Aware Patch Generation for Better Automated Program Repair. In ACM/IEEE International Conference on Software Engineering (ICSE). Gothenburg, Sweden, 1–11. https://doi.org/10.1145/3180155.3180233 — [doi:10.1145/3180155.3180233](https://doi.org/10.1145/3180155.3180233) ↗
  91. Minchao Wu, Michael Norrish, Christian Walder, and Amir Dezfouli. 2021. TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning. In Neural Information Processing Systems. https://arxiv.org/abs/2102.09756 ↗
  92. Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. 2022. Autoformalization with Large Language Models. CoRR abs/2205.12615 (2022). https://doi.org/10.48550/ARXIV.2205.12615 ↗
  93. Qi Xin and Steven P. Reiss. 2017. Identifying Test-suite-overfitted Patches through Test Case Generation. In ISSTA. 226–236. https://doi.org/10.1145/3092703.3092718 — [doi:10.1145/3092703.3092718](https://doi.org/10.1145/3092703.3092718) ↗
  94. Deheng Yang, Yuhua Qi, and Xiaoguang Mao. 2018. Evaluating the Strategies of Statement Selection in Automated Program Repair. In SATE. Springer. https://doi.org/10.1007/978-3-030-04272-1_3 — [doi:10.1007/978-3-030-04272-1_3](https://doi.org/10.1007/978-3-030-04272-1_3) ↗
  95. Jinqiu Yang, Alexey Zhikhartsev, Yuefei Liu, and Lin Tan. 2017. Better test cases for better automated program repair. In ESEC/FSE. 831–841. https://doi.org/10.1145/3106237.3106274 — [doi:10.1145/3106237.3106274](https://doi.org/10.1145/3106237.3106274) ↗
  96. Kaiyu Yang and Jia Deng. 2019. Learning to prove theorems via interacting with proof assistants. In International Conference on Machine Learning. PMLR, 6984–6994.
  97. Xuejun Yang, Yang Chen, Eric Eide, and John Regehr. 2011. Finding and understanding bugs in C compilers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). San Jose, CA, USA, 283–294. https://doi.org/10.1145/1993498.1993532 ↗
  98. Michihiro Yasunaga and Percy Liang. 2021. Break-it-fix-it: Unsupervised learning for program repair. In International Conference on Machine Learning (ICML). PMLR, 11941–11952. find
  99. He Ye, Matias Martinez, and Martin Monperrus. 2021. Automated patch assessment for program repair at scale. EMSE 26, 2 (2021). find
  100. Zhongxing Yu, Matias Martinez, Benjamin Danglot, Thomas Durieux, and Martin Monperrus. 2019. Alleviating patch overfitting with automatic test generation: A study of feasibility and effectiveness for the Nopol repair system. EMSE 24, 1 (2019), 33–67. https://doi.org/10.1007/s10664-018-9619-4 — [doi:10.1007/s10664-018-9619-4](https://doi.org/10.1007/s10664-018-9619-4) ↗
  101. Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. 2022. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. In ICLR.
  102. Qihao Zhu, Zeyu Sun, Yuan an Xiao, Wenjie Zhang, Kang Yuan, Yingfei Xiong, and Lu Zhang. 2021. A syntax-guided edit decoder for neural program repair. In ESEC/FSE. 341–353. https://doi.org/10.1145/3468264.3468544 ↗

Updated

↑ back to top

This page in Markdown → https://md.research.elamur.ai/free/en/papers/first-2023-baldur-whole-proof-generation-repair/