mlsanityData to 14 Oct 2026

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

arXiv 2303.04910 ↗First posted 8 Mar 2023cs.LG cs.LO cs.SEcited by 119

Not on the map. Why?

Cited by 23 in LLM reasoning, but placed by its own abstract, which didn’t fit.

Abstract (arXiv)

Formally verifying software properties is a highly desirable but labor-intensive task. Recent work has developed methods to automate formal verification using proof assistants, such as Coq and Isabelle/HOL, e.g., by training a model to predict one proof step at a time, and using that model to search through the space of possible proofs. This paper introduces a new method to automate formal verification: We use large language models, trained on natural language text and code and fine-tuned on proofs, to generate whole proofs for theorems at once, rather than one step at a time. We combine this proof generation model with a fine-tuned repair model to repair generated proofs, further increasing proving power. As its main contributions, this paper demonstrates for the first time that: (1) Whole-proof generation using transformers is possible and is as effective as search-based techniques without requiring costly search. (2) Giving the learned model additional context, such as a prior failed proof attempt and the ensuing error message, results in proof repair and further improves automated proof generation. (3) We establish a new state of the art for fully automated proof synthesis. We reify our method in a prototype, Baldur, and evaluate it on a benchmark of 6,336 Isabelle/HOL theorems and their proofs. In addition to empirically showing the effectiveness of whole-proof generation, repair, and added context, we show that Baldur improves on the state-of-the-art tool, Thor, by automatically generating proofs for an additional 8.7% of the theorems. Together, Baldur and Thor can prove 65.7% of the theorems fully automatically. This paper paves the way for new research into using large language models for automating formal verification.

Key facts. Cited by 119 papers in the map (data through 14 Oct 2026). Builds on 53 of its 123 references that are in the map. First posted on arXiv 8 Mar 2023.

Builds on

53 of 123 references.

References · 53

  1. 2017Attention Is All You Needcited by 60,361
  2. 2020Language Models are Few-Shot Learnerscited by 32,419
  3. 2019Exploring the Limits of Transfer Learning with a Unified Text-to-Text Transformercited by 14,599
  4. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,459
  5. 2021Training Verifiers to Solve Math Word Problemscited by 10,109
  6. 2021Evaluating Large Language Models Trained on Codecited by 8,320
  7. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,371
  8. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,326
  9. 2021RoFormer: Enhanced Transformer with Rotary Position Embeddingcited by 4,703
  10. 2016WaveNet: A Generative Model for Raw Audiocited by 1,722
  11. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,392
  12. 2018Hierarchical Neural Story Generationcited by 1,193
38 more
  1. 2021Show Your Work: Scratchpads for Intermediate Computation with Language Modelscited by 886
  2. 2019Fast Transformer Decoding: One Write-Head is All You Needcited by 717
  3. 2022GPT-NeoX-20B: An Open-Source Autoregressive Language Modelcited by 713
  4. 2022Efficiently Scaling Transformer Inferencecited by 539
  5. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
  6. 2020Generative Language Modeling for Automated Theorem Provingcited by 388
  7. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 291
  8. 2022Autoformalization with Large Language Modelscited by 263
  9. 2022HyperTree Proof Search for Neural Theorem Provingcited by 197
  10. 2018SequenceR: Sequence-to-Sequence Learning for End-to-End Program Repaircited by 145
  11. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 132
  12. 2017Fairness Testing: Testing Software for Discriminationcited by 126
  13. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 109
  14. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 98
  15. 2021Break-It-Fix-It: Unsupervised Learning for Program Repaircited by 71
  16. 2021A Syntax-Guided Edit Decoder for Neural Program Repaircited by 57
  17. 2019Graph Representations for Higher-Order Logic and Theorem Provingcited by 55
  18. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  19. 2018TacticToe: Learning to Prove with Tacticscited by 44
  20. 2019Generating Correctness Proofs with Neural Networkscited by 37
  21. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  22. 2022Formal Specifications from Natural Languagecited by 33
  23. 2023Towards Autoformalization of Mathematics and Code Correctness: Experiments with Elementary Proofscited by 27
  24. 2020Evaluating Representation Learning of Code Changes for Predicting Patch Correctness in Program Repaircited by 22
  25. 2016Automated Clustering and Program Repair for Introductory Programming Assignmentscited by 21
  26. 2022Passport: Improving Automated Formal Verification Using Identifierscited by 19
  27. 2021Pretrained Language Models are Symbolic Mathematics Solvers too!cited by 17
  28. 2021Elixir: Effective object-oriented program repaircited by 16
  29. 2019Automated Patch Assessment for Program Repair at Scalecited by 14
  30. 2020QED at Large: A Survey of Engineering of Formally Verified Softwarecited by 13
  31. 2019Harnessing Evolution for Multi-Hunk Program Repaircited by 12
  32. 2019iFixR: Bug Report driven Program Repaircited by 11
  33. 2020Better Automatic Program Repair by Using Bug Reports and Tests Togethercited by 10
  34. 2017Data-Driven Feedback Generation for Introductory Programming Exercisescited by 9
  35. 2022Enforcing Delayed-Impact Fairness Guaranteescited by 8
  36. 2018PaMpeR: Proof Method Recommendation System for Isabelle/HOLcited by 7
  37. 2018Alleviating Patch Overfitting with Automatic Test Generation: A Study of Feasibility and Effectiveness for the Nopol Repair Systemcited by 7
  38. 2020Deep Generation of Coq Lemma Names Using Elaborated Termscited by 6

50 most cited of 53 All 53 (JSON)

Built on by

Cited by year (2026 to 14 Oct)

Citing papers per year: 2023: 18; 2024: 30; 2025: 36; 2026: 35.

119 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 427
  2. 2023Llemma: An Open Language Model For Mathematicscited by 388
  3. 2024When Can LLMs Actually Correct Their Own Mistakes? A Critical Survey of Self-Correction of LLMscited by 240
  4. 2023Automatically Correcting Large Language Models: Surveying the landscape of diverse self-correction strategiescited by 238
  5. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
  6. 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
  7. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 133
  8. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 109
  9. 2025Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipelinecited by 82
  10. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 81
  11. 2023Evaluating Language Models for Mathematics through Interactionscited by 70
  12. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 68
38 more
  1. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 58
  2. 2025Aristotle: IMO-level Automated Theorem Provingcited by 58
  3. 2024A Survey on Deep Learning for Theorem Provingcited by 57
  4. 2024The Limits of Inference Scaling Through Resamplingcited by 53
  5. 2023Lemur: Integrating Large Language Models in Automated Program Verificationcited by 49
  6. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 49
  7. 2023Knowledge Transfer from High-Resource to Low-Resource Programming Languages for Code LLMscited by 45
  8. 2025Advancing Reasoning in Large Language Models: Promising Methods and Approachescited by 43
  9. 2023Look Before You Leap: An Exploratory Study of Uncertainty Measurement for Large Language Modelscited by 41
  10. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  11. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 37
  12. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 35
  13. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  14. 2025VERINA: Benchmarking Verifiable Code Generationcited by 34
  15. 2024Automated Proof Generation for Rust Code via Self-Evolutioncited by 33
  16. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 31
  17. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 27
  18. 2024Proving Theorems Recursivelycited by 26
  19. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 25
  20. 2023Mathematical Language Models: A Surveycited by 24
  21. 2024Proof Automation with Large Language Modelscited by 22
  22. 2024Formal Theorem Proving by Rewarding LLMs to Decompose Proofs Hierarchicallycited by 22
  23. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 20
  24. 2023Can Transformers Learn to Solve Problems Recursively?cited by 17
  25. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  26. 2025Generative AI Act II: Test Time Scaling Drives Cognition Engineeringcited by 15
  27. 2024VerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model, and Tree Searchcited by 14
  28. 2025StepFun-Prover Preview: Let's Think and Verify Step by Stepcited by 13
  29. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworkscited by 12
  30. 2023Leveraging Large Language Models for Automated Proof Synthesis in Rustcited by 11
  31. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 11
  32. 2024SubgoalXL: Subgoal-based Expert Learning for Theorem Provingcited by 11
  33. 2024CoqPilot, a plugin for LLM-based generation of proofscited by 11
  34. 2024Data for Mathematical Copilots: Better Ways of Presenting Proofs for Machine Learningcited by 11
  35. 2025HERMES: Towards Efficient and Verifiable Mathematical Reasoning in LLMscited by 11
  36. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 11
  37. 2023AI for Mathematics: A Cognitive Science Perspectivecited by 10
  38. 2025MPS-Prover: Advancing Stepwise Theorem Proving by Multi-Perspective Search and Data Curationcited by 10

50 most cited of 119 All 119 (JSON)