Source-linked AI summary
Baldur: Whole-Proof Generation and Repair with Large Language Models
Emily First, Markus N. Rabe, Talia Ringer, Yuriy Brun
TL;DR
Formal verification produces high-quality software but is often prohibitively labor-intensive. Baldur uses fine-tuned large language models to generate whole Isabelle/HOL proofs and repair failed attempts, proving 65.7% of theorems with Thor and 8.7% more than Thor alone.
Problem
Manual formal verification is highly effective but often prohibitively costly because writing proofs is labor-intensive.
Method
Baldur fine-tunes large language models to generate entire proofs from theorem statements and repair failed attempts using proof-assistant error messages and theory-file context.
Results
Baldur proves 47.9% of theorems automatically versus 39.0% for search-based approaches, while Baldur and Thor together prove 65.7%.
Takeaways & Limitations
Whole-proof generation and repair provide an effective, simple approach that complements search-based theorem-proving techniques.
Takeaways & Limitations
The repair model mainly learns to address first-occurring errors, typically located in the first few lines of predicted proofs.
Abstract
from arXiv · showhide
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.
1 INTRODUCTION
Baldur uses fine-tuned large language models to generate and repair complete Isabelle/HOL proofs, avoiding costly stepwise search. On 6,336 theorems, it improves automated proving and complements existing search-based methods.
- Motivation: Formal verification can produce highly reliable software, but manually writing proofs is often prohibitively expensive.The CompCert proof is more than three times as long as the compiler code itself.
- Baldur’s approach: Baldur generates entire formal proofs with LLMs, rather than predicting individual proof steps or using hammers and computationally expensive search.The approach fine-tunes LLMs on proofs and uses the theorem statement as input.
- Results: 47.9% of theorems were proved automatically by Baldur without repair, compared with 39.0% for search-based approaches.The comparison is made on the PISA Isabelle/HOL benchmark, using 6,336 theorems.
- Results: 1.5% more theorems were proved when Baldur received an erroneous proof attempt and the proof assistant’s error messages.The error message was crucial to this improvement, even when controlling for the computational cost of additional inference.
- Results: With theorem context, Baldur proved 47.5% of theorems, compared with 40.7% without context for the same model size.The context consists of text immediately preceding the theorem in its theory file.
- Results: Together, Baldur and Thor proved 65.7% of theorems, versus 57.0% for Thor alone, while Baldur also complements methods that it does not duplicate.The findings indicate that LLM- and search-based methods can work together to improve formal-verification automation.
2 THE BALDUR APPROACH
Baldur replaces stepwise proof search with whole-proof generation by fine-tuned language models, then uses proof repair and contextual information to improve synthesis. The approach separates generation from Isabelle checking and reconstructs training data from complete proofs.
- 2.1 Proof Generation: Baldur fine-tunes language models to generate complete formal proofs instead of predicting individual proof steps during search.The model receives a theorem statement and produces a candidate proof, avoiding hammers and computationally expensive search.
- 2.1 Proof Generation: In an illustrative theorem, Baldur generates a succinct induction proof using infinite_finite_induct, while Sledgehammer cannot prove the theorem by default.The generated proof follows the human proof’s overarching induction strategy but compresses it substantially.
- 2.1 Proof Generation: The proof-generation dataset is created by concatenating the proof steps of existing theorems to reconstruct their original complete proofs.This drops proof states and relies on Isabelle’s declarative, human-readable proof language.
- 2.1 Proof Generation: The proof-generation pipeline samples multiple complete proof candidates and accepts a theorem when Isabelle verifies any candidate.Inference typically samples 16 or 64 sequences, after which the proof assistant checks the sampled proofs.
- 2.2 Proof Repair: Baldur’s proof repair model takes a theorem statement, an incorrect proof, and Isabelle’s error message to generate a revised candidate proof.This adds proof-assistant feedback to the repair process, whereas existing proof-generation methods cannot leverage error messages.
- 2.3 Adding Context: Adding theory-file context exposes preceding lines from the same theory file, but this context contains only a small fraction of available premises and mostly consists of proofs.The paper contrasts this simple text-processing approach with premise selection and emphasizes its limited premise coverage.
3 EVALUATION
The evaluation tests whole-proof generation, repair, contextual inputs, model scale, and complementarity with prior search-based methods on the PISA Isabelle/HOL benchmark. Baldur performs competitively with search, gains from repair and context, improves with scale, and complements Thor.
- Evaluation setup: The experiments evaluate five questions covering whole-proof generation, repair, theorem context, model size, and comparison with state-of-the-art methods.Models are evaluated on the PISA benchmark using results reported in Table 4 and Figure 5.
- Context and repair: Repair adds 1.5% of theorems at controlled inference cost, with the proof assistant’s error message crucial to the improvement.A repair model without the error message does not surpass plain generation when inference cost is normalized.
- Context and repair: The 8b model reaches 40.7% with 64 samples, while adding theory-file context increases the proof rate to 47.5%.Contextual models consistently outperform plain generation, and examples show copying or adapting nearby proofs.
- Model scale: The 62b model reaches 47.9% with 64 samples versus 47.5% for the 8b model with context, although its hyperparameters were less thoroughly tuned.The results indicate improved theorem-proving performance with larger language models.
- Comparison with prior methods: Baldur and Thor together prove 65.7% of theorems, compared with 57.0% for Thor alone, indicating complementary LLM- and search-based methods.Baldur alone solves up to 47.9% of the problems, while the combined union yields a larger gain.
4 DISCUSSION: WHAT’S NEXT?
The discussion proposes extending generate-and-repair into learnable proof search, reconsidering benchmark splits, and evaluating methods across proof assistants. It also identifies repair-data quality and cross-assistant comparability as important boundaries for future work.
- Learnable Proof Search: A learnable proof-search strategy would sample candidate proofs, repair them, and repeatedly repair the repair model’s outputs.This strategy combines proof generation and repair while avoiding the paper’s costly conventional search procedures.
- Learnable Proof Search: A proof-of-concept with generation, first repair, and second repair uses inference cost 3 and shows iterative repair can improve proof synthesis.The setup uses one sample for each of the three stages.
- Learnable Proof Search: At inference cost 2, generate-plus-repair proves 24.9% of theorems; a second repair raises this to 26.2%, versus 25.4% for generation at cost 3.The second repair attempt exceeds generation at the same stated cost by 0.8%.
- Limitations and future work: Future repair search requires training data that better mirrors the changes needed for subsequent repair attempts.Because proof checking reports the first occurring error, current repair training primarily teaches correction of early proof errors.
- Limitations and future work: PISA’s theorem-wise split supports using nearby project context, whereas project-wise splits such as CoqGym target new-project settings.Different splits correspond to different evaluation goals, so benchmark results depend partly on the intended use case.
- Limitations and future work: Direct comparisons across proof assistants remain difficult because their benchmarks, project splits, and user communities differ.The paper calls for porting techniques across assistants and developing cross-proof-assistant benchmark suites.
5 RELATED WORK
Prior formal theorem-proving systems use hammers, search-based neural methods, and related machine-learning tasks to assist proof development. Baldur’s proof-repair task extends this landscape by using error messages to repair proofs and improve synthesis.
- Hammers iteratively apply precomputed mathematical facts, but their tactic limitations prevent them from proving some large theorem classes.
- LISA and GPT-f combine language models with proof search, while other systems use reinforcement learning or Monte Carlo tree search strategies.
- Autoformalization and informal-proof benchmarks connect natural-language specifications or proofs with formal, machine-checkable theorem proving.
- DSP uses informal proof drafts translated into formal sketches and then proven with Sledgehammer, unlike Baldur’s fine-tuned, search-free approach.
- Proof repair with error messages is introduced as a new machine-learning task intended to improve neural theorem-proving performance.
6 CONTRIBUTIONS
Baldur fine-tunes large language models to generate complete proofs without proof search or hammers, then uses repair and complementary tools to improve automated synthesis. The combined approach reaches a new state of the art on an Isabelle/HOL benchmark.
- Baldur is the first approach described here to fine-tune large language models for entire theorem proofs without proof search or hammers.
- Baldur is reported as more effective and efficient than prior one-step-at-a-time search-based generation.
- Together, Baldur and prior search- and hammer-based tools fully automatically synthesize proofs for 65.7% of theorems in a large Isabelle/HOL benchmark.
- The paper identifies future research directions involving LLM-based theorem proving, proof repair, and context such as failed attempts and error messages.
A EXAMPLES OF PROOF GENERATION WITH CONTEXT
The context-based proof-generation examples show models adapting proofs available in context while also producing proofs that use new premises or simpler tactics. These examples illustrate varied ways context can support successful synthesis.
- The examples compare problems solved by a context-aware model but not by the plain proof-generation model.
- In examples 1, 3, and 5, the model copies and adapts proofs present in its context.
- In example 2, the model uses a premise absent from its context, matching the ground-truth proof’s premise but employing a different tactic.
- In example 4, the model finds a simpler proof that was not present in the context.
A.1 Example 1
The example presents Isabelle/HOL context and proof fragments involving interpretation lemmas, including Interp.cases and InterpExprWellDefined. The displayed fragments show proof attempts using rule application with automation.
- The context includes an interpretation lemma named InterpExprWellDefined.
- Several proof fragments apply the rule Interp.cases and finish with automation such as auto or simp.
- The example contains a Bool lemma in the Interpretation locale.
A.2 Example 2
This example presents lemmas about expanding an expression and proves them with transfer-based simplification. The generated proof alternatives use either the expansion lemma directly or simplification with it.
- The example introduces simp lemmas for the zero and increment cases of Aeta_expand.
- The increment case expands Aeta_expand n (App e (fresh_var e)) using inc_def and transfer-based simplification.
- One proof applies subst_eta_expand directly through transfer.
- A second proof combines subst_eta_expand with simp inside transfer.
A.3 Example 3
This example defines stores as functions and assignment as a relation updating a variable with an expression's value. It then proves the assignment relation using relational definitions and simplification.
- Store and Assignment: The Store and Assignment subsection introduces stores as functions from strings to values.
- Store and Assignment: Assignment maps a variable and expression to pairs whose second store updates the variable with the expression evaluated in the first store.
- Store and Assignment: The relational specification uses rel_kat.H with a predicate requiring P after the assignment update.
- Store and Assignment: The proof discharges the specification by automatic simplification using the relational and assignment definitions.
- Store and Assignment: The formal development also includes an implication into rel_kat.H.
A.4 Example 4
This example defines primitive words as words that are not non-trivial powers and proves that every primitive word is non-empty.
- Primitive words: A primitive word is defined as a word that is not a non-trivial power of another word.
- Primitive words: The definition is unfolded directly to prove the corresponding characterization theorem.
- Primitive words: The development proves that primitive u implies u ≠ ε.
- Primitive words: The non-emptiness result follows by considering ε raised to the zeroth power and using zero_neq_one.
- Primitive words: The proof uses primitive_def and force-based reasoning to establish the result.
A.5 Example 5
This example develops list decompositions for non-distinct lists and proves a minimum-prefix decomposition identity. The proofs use induction, case analysis, and list operations such as take and drop.
- A.5 Example 5: The minimum-prefix lemma states drop n (take m xs) @ drop m xs = drop (min n m) xs.
- A.5 Example 5: Its proof splits on whether m < n and uses drop_append, length cases, and min_def.
- A.5 Example 5: The stronger prefix lemma requires distinct xs, y not in xs, and y not in ys.
- A.5 Example 5: For a non-distinct list, one lemma decomposes it as xs @ y # ys @ y # zs while requiring distinct (ys @ [y]).
- A.5 Example 5: The decomposition proof proceeds by induction on ws and by cases on whether the tail is distinct.
- A.5 Example 5: In the distinct-tail case, list membership and distinctness yield a decomposition around the repeated element.
- A.5 Example 5: In the non-distinct-tail case, the induction hypothesis extends the decomposition by prepending the head element.
- A.5 Example 5: A related decomposition obtains y in xs, distinct xs, and then decomposes xs around another occurrence of y.