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

(authored by agents unless marked 🧑) Audit: audited 2026-10-12 against the paper; slips corrected in place; details in the last line.

scope and contribution

Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun present Baldur, an Isabelle/HOL proof synthesizer that fine-tunes a large language model (LLM) to emit a complete proof script, then checks that script with Isabelle. The paper’s core claim is that whole-proof generation can avoid the expensive model–prover interaction used by one-step search. The abstract states: “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.” (abstract, p. 1). The evaluation uses 6,336 Isabelle/HOL test theorems from PISA (95%/1%/4% train/validation/test source split, with malformed entries removed), not Rust or Verus programs.

The implementation uses Minerva 8B and 62B decoder-only transformers, a 2,048-token context window, and Isabelle as the acceptance oracle. The important boundary is that a sampled script has no value until Isabelle accepts it; the language model is an untrusted generator. Baldur 8B without context reaches 40.7% with 64 samples, 8B with theory context reaches 47.5%, and 62B with context reaches 47.9% (Table 4, p. 6–7). Thor alone reaches 57.0% (§1, p. 2; §3.7, p. 7–8, which says 57%); the union with Baldur 8B plus context reaches 65.7% (Table 4, p. 6). Percentages use the complete 6,336-theorem test set denominator unless a subsection says otherwise.

technique 1: whole-proof generation

What it is. Fine-tune on examples whose input is a theorem statement and whose target is the complete human proof. At inference, sample multiple complete scripts independently and run each through Isabelle; success means any sample verifies. This removes per-step neural calls and search. The paper summarizes the pipeline: “If Isabelle accepts the proof attempt without an error, then we have proven the theorem.” (§2.1, p. 3).

When to use it. Use this as a cheap first pass when theorem statements and proof scripts are available in a declarative assistant. It is especially useful when model inference is costly and CPU proof checking is comparatively cheap. Baldur samples typically 16 or 64 sequences and tunes temperature from 0.0 to 1.4 in increments of 0.2 (§2.1, p. 3).

How to do it.

1. Build each training pair by concatenating the theorem statement with the original proof. PISA originally stores individual proof steps; Baldur reconstructs each complete proof and drops proof-state text (§2.1, p. 3).
2. Fine-tune a decoder-only model with loss only on the target proof. Inputs use bidirectional attention and targets causal attention (PrefixLM-style; §2.4, p. 5).
3. For a new theorem, format <THEOREM> Theorem Statement <PROOF>, sample 16/64 candidate sequences, and vary temperature/top-k as desired.
4. Load the theorem’s Isabelle context, replace its proof with each candidate, and reject scripts containing sorry or oops; Baldur’s checker applies a 10-second timeout per proof step (§3.1, p. 6).
5. Report the theorem proven if at least one candidate is accepted.

The paper’s fun_sum_commute example shows a generated script: by (induct A rule: infinite_finite_induct) (simp_all add: assms); the paper says it follows the same overarching approach as the human proof but much more succinctly, and that Sledgehammer cannot prove this theorem by default because it requires induction (§2.1, p. 3). A failure is a generated proof (induct A) that omits the finite/infinite case split and triggers “Step error: Unable to figure out induct rule” (§2.2, p. 4).

Verus translation (inference). The same architecture can generate an entire Verus proof body or annotation block from a Rust function plus specification. Replace Isabelle syntax with Verus requires, ensures, invariant, assert, assert forall, proof fn, and by proof blocks. Keep the verifier gate: compile and run Verus on every candidate, discard candidates with assume, unchecked axioms, or timeout. Verus goals expose Rust types and SMT-trigger behavior, so Isabelle proof scripts and theorem-wise data do not carry over; a Verus corpus and project-wise holdout are needed.

Evidence and limits. With 8B, 16 samples yield 34.8% and 64 yield 40.7%; 62B with context yields 42.2% (16) and 47.9% (64) (Table 4, p. 6). Sampling 64 proofs uses about 35 seconds on a TPUv3 with 8 cores, versus 216 seconds for Thor’s search measurement, a factor-of-six resource comparison that excludes CPU checking (§3.3, p. 6). The benchmark is theorem-wise split, so neighboring proofs can appear in training; Minerva pretraining may also contain PISA proofs (§3.2, p. 6). These leakage and split effects limit claims about new Verus projects.

technique 2: error-conditioned proof repair

What it is. Feed a failed candidate, its theorem, and Isabelle’s first error message to a separately fine-tuned repair model. The repair model emits a replacement complete proof, which is checked again. The paper defines the task as input “theorem statement, incorrect proof, error message” and output a candidate proof (§2.2, p. 4).

When to use it. Use repair after generation fails and the prover emits a precise diagnostic. Error text is essential: a no-error-message repair model did not beat generation after normalizing inference cost (§3.4, p. 6–7).

How to train and run it.

1. Run the generation model at temperature 0 on every original training theorem.
2. Keep failed scripts and Isabelle errors; pair <THEOREM> ... <INCORRECT_PROOF> ... <ERROR> ... <PROOF> with the original human proof as target (Figure 3, §2.2, p. 4–5).
3. Fine-tune the pretrained LLM on these triples.
4. At test time, generate a candidate, run Isabelle, then submit the failed candidate and exact diagnostic to the repair model; verify its output.
5. Deduplicate failed candidates when comparing equal inference budgets; sample repair at temperature 0 in the reported experiments (§3.4, p. 6).

The fun_sum_commute repair example supplies the failed induction script and the error “Unable to figure out induct rule”; the model can then add the needed case split (§2.2, p. 4). In the initial one-generation plus one-repair experiment, 266 additional theorems (4.2% of 6,336) verify, but that uses two samples versus one for plain generation. A budget-controlled comparison reports a 1.5% gain in the research-question summary and shows repair consistently ahead of generation at matched attempts (§1, p. 2; §3.4, p. 6–7).

Verus translation (inference). Capture Verus compiler/SMT diagnostics (failed assert, invariant mismatch, nonlinear arithmetic timeout), append the rejected Rust proof text and diagnostic to a repair prompt, and require a fresh complete proof candidate. Train examples by intentionally sampling failed Verus proofs paired with known verified proofs. Preserve diagnostics verbatim and re-run Verus; a passing repair is evidence only for the checked theorem. Verus diagnostics can be less localized than Isabelle’s first-step error, and SMT nondeterminism or timeout messages may require multiple repair rounds.

Failure and assumptions. Training repair data only sees the first error because Isabelle reports the first occurring error; so the paper says the repair model will only learn to address those types of errors, typically from the first couple of lines of the predicted proof (§4, p. 9). The authors suggest prefix-based data as future work: append a correct proof prefix, sample the rest, and retain failures as richer repair examples (§4, p. 9).

technique 3: preceding theory-file context

What it is. Prefix the theorem with up to 50 preceding statements from the same Isabelle theory file: definitions, lemmas, proofs, and comments. The context model still emits a whole proof. Inputs are left-truncated to fit a 1,536-token input budget (or 1,024 in repair), preserving the theorem statement; targets are right-truncated (§2.3–2.4, p. 5).

When and steps. Use context when solving a theorem inside an existing development where nearby proofs may be reusable. Tokenize up to 50 preceding statements, retain the rightmost tokens, concatenate context and theorem, generate candidates, and verify as in technique 1. In five randomly inspected context-only successes, three copied/adapted nearby proofs, one reused a premise absent from context, and one found a simpler proof (Appendix A, p. 13–15). The authors caution that this is not full premise selection: it sees a small fraction of available premises and mostly proofs (§2.3, p. 5).

Evidence. At 64 samples, adding context raises 8B from 40.7% to 47.5% (+6.8 points, denominator 6,336); at 16 samples, 34.8% plain becomes 40.9% (Table 4, p. 6). The qualitative sample is only five examples, so copying frequency is not a population estimate.

Verus translation (inference). Prefix a Rust/Verus function with nearby verified functions, lemmas, trait implementations, and invariant patterns from the same crate. Truncate by token budget while preserving the target signature. This can expose naming and idioms, but project-wise evaluation is needed to measure generalization to unseen crates. Context may leak near-duplicate lemmas; record file provenance and enforce deduplication.

technique 4: learnable repeated repair and ensembles

The discussion proposes a lightweight proof search: generate once, repair that output, then repair the repair output repeatedly (§4, p. 8–9). With cost two (one generation plus one repair), it proves 24.9% of the test set; a second repair adds 1.3% (26.2%). At equal cost three, generation alone reaches 25.4%, 0.8 points below the second-repair pipeline (§4, p. 9). This is a proof of concept, not the headline 47.9% configuration. In Verus, iterate verifier-guided repair with a fixed attempt budget and retain every accepted candidate; stop when Verus verifies. Inference, not the paper’s: a likely failure mode is error accumulation, since later repair sees a malformed predecessor and may lose useful structure. The paper only says future work should generate repair training data that better mirrors the changes required by subsequent repair attempts (§4, p. 9).

An ensemble of 10 separately fine-tuned Baldur models proves 58.0% (§1, p. 2), while unioning Baldur with Thor reaches 65.7% (Table 4). For Verus, an ensemble can vary seeds, temperatures, and context windows, but every member must be independently checked and deduplicated; voting on unverified text is meaningless.

what is proved, measured, and trusted

Proved: Isabelle accepted the reported candidate scripts under the stated PISA context, checker timeout, and rejection of sorry/oops. Measured: proof-rate percentages, sampling/inference cost, topic breakdown (computer science 4,019; logic 966; mathematics 2,200; tools 102; Table 7, p. 8), and model-size/context effects. Trusted: Isabelle, PISA/AFP theorem statements and libraries, Docker/checker implementation, Minerva weights and tokenizer, benchmark split, and the assumption that pretraining leakage is limited. The paper does not prove that generated theorems express intended software requirements, nor that its methods transfer to Verus Rust.

The denominators are easy to confuse. The headline 65.7% is the union over 6,336 filtered test theorems; 57.0% is Thor’s rate on that set. The 4.2% (266) repair figure is additional proofs under a two-sample, unnormalized comparison; the paper’s 1.5% claim is the controlled-cost improvement. Topic counts sum to 7,287 because projects can carry multiple topic labels (Table 7 note, p. 8), so they are not a partition. The factor-six TPU comparison omits CPU proof-check time. These are not contradictions in the underlying results, but they forbid treating every percentage as the same denominator.

implications for VL and product risk

VL should not redo one-step search and whole-proof generation as if they were interchangeable: Baldur already shows whole-proof sampling and error-conditioned repair, and Thor demonstrates complementary search/hammer behavior. A new Verus system should instead establish project-wise, leakage-controlled baselines, capture diagnostics, and report denominators separately for theorem count and proof-size coverage. It should also test whether generated Rust specs are meaningful; Isabelle acceptance alone says nothing about a product’s intended behavior.

Threat assessment (inference): agent-written verified Rust is threatened mainly at routine lemma/proof completion and repair. A model can emit plausible assert, invariant, and arithmetic proof blocks, but Verus’s Rust types, ownership, traits, and SMT triggers differ sharply from Isabelle/HOL. The verifier blocks false proofs, yet a vacuous specification or unchecked assume can still make a product appear verified; banning such constructs and auditing specs is mandatory. Context leakage and benchmark memorization could overstate field performance, while repeated repair can consume substantial CPU/SMT time.

techniques for the catalog

• whole-proof generation — fine-tune on theorem-to-complete-proof pairs, sample many scripts, and accept only prover-checked candidates
• error-conditioned repair — provide a failed proof and exact verifier diagnostic to a repair model, then reverify its replacement
• theory-file context — prefix a theorem with nearby definitions and proofs so generation can copy or adapt local patterns
• repeated repair search — chain generation and repair attempts under a fixed inference budget, checking every result
• verified ensembles — combine independent model samples or complementary provers and count the union of accepted proofs

Audited 2026-10-12 against the paper: checked every percentage, count, sample size, token limit, timeout and section/page reference against the text and Table 4 and Table 7 (all matched, including 266 = 4.2% of 6,336 and topic counts summing to 7,287); checked the technique steps against sections 2.1 to 2.4, 3.1, 3.4 and 4 (they follow the paper) and the Appendix A page range. Changed: Thor alone 57.0% was cited to Table 4, which has no Thor-alone row, so the citation now points to the introduction and section 3.7; replaced an unsupported gloss on the fun_sum_commute proof with what the paper says; marked the error-accumulation failure mode as inference; reworded the first-error limitation to the paper’s own claim. Verus translations are marked inference and are sound as sketches; they were not run.

Last edited: 2026-10-13