APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

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

scope and result

APOLLO is a compiler-guided repair pipeline for Lean4 theorem proofs. Its central claim is that a failed whole-proof sample contains useful structure that can be repaired locally, so regeneration of an entire proof is wasteful. The paper says that “Apollo directs a fully automated process in which the LLM generates proofs for theorems, a set of agents analyze the proofs, fix the syntax errors, identify the mistakes in the proofs using Lean, isolate failing sub-lemmas, utilize automated solvers, and invoke an LLM on each remaining goal with a low top-K budget.” The verifier is Lean’s kernel; APOLLO orchestrates repairs around the kernel and does not weaken the final check.

The experiment is miniF2F-test (244 problems from a 488-problem dataset), Lean 4.17.0, eight NVIDIA A5000 GPUs and 128 CPU cores. Goedel-Prover-SFT rises from 64.7% (25,600 samples) to 65.6% with APOLLO (recursion depth 6, 362 samples on average, 179K generated tokens). Kimina-Prover-Preview-Distill-7B rises from 70.8% at 1,024 samples to 75.0% with APOLLO (depth 6, 307 samples, 1.3M tokens). General-purpose o3-mini and o4-mini rise from 3.3% and 7.0% at one sample to 40.2% and 46.7% with APOLLO. PutnamBench gives 11/658 with Kimina+APOLLO versus 10/658 at 192 whole-proof samples. These denominators matter: percentages are problem-level success, and APOLLO’s sample count is an average that depends on recursive subgoals.

technique 1: compiler-guided staged repair

What it is: retain the model’s proof sketch, ask Lean REPL for structured diagnostics, and pass those diagnostics through repair stages. Lean reports syntax errors, nonexistent tactics, unused tactics, open goals, locations, and descriptions. The paper explicitly contrasts this with the usual binary filtering of many independent samples: “all of those information/feedback from the compiler remains unused.”

When to use it: use this when a model has a plausible proof strategy but invalid Lean syntax, an incorrect tactic invocation, or a few unclosed subgoals. It is less suitable when the initial mathematical strategy omits a necessary lemma or is fundamentally wrong; the authors state that APOLLO depends on a coherent initial sketch.

How to do it:

1. Generate one or more complete Lean proofs for the theorem.
2. Compile the file in Lean REPL and collect every diagnostic with its source location.
3. Run Syntax Refiner on superficial syntax errors: missing commas, brackets, or Lean-version keywords such as Lean3 from versus Lean4 := by.
4. Parse nested proof blocks and run Sorrifier (technique 2) until the file compiles with only sorry warnings.
5. Run Auto Solver on each sorry (technique 3).
6. Recursively ask the LLM to prove unresolved blocks, then splice repaired blocks and compile the whole theorem.
7. Stop when there are no sorry or admit commands, or after user-chosen recursion depth r.

Verus form (inference): a Verus agent can use verus diagnostics as the loop’s compiler oracle. Keep the generated Rust function and its requires/ensures shell, parse diagnostics by source span, isolate failing proof blocks or assert chains, and rerun verification after each patch. Lean tactics and theorem names do not carry over; the portable idea is diagnostic localization plus preserving a compilable scaffold. Verus’s assert, assert forall, lemma, broadcast proof, and solver triggers can represent the extracted obligations, while Rust ownership and mutable state make block extraction less syntactically direct.

Evidence and limits: on miniF2F, APOLLO obtains the accuracy and budget changes above; the paper reports that “even r = 5 requires only 300–400 LLM requests on average.” The ablation shows that Syntax Refiner alone changes o4-mini from 7.0% to 7.4%, Auto Solver alone to 7.0%, and LLM re-invocation alone to 8.2%; all three reach 46.7%. This supports synergy rather than attributing gains to syntax cleanup. The study does not test tree-search integration, and it does not establish that an arbitrary bad proof sketch can be repaired.

technique 2: Sorrifier and obligation extraction

What it is: convert an invalid proof into a compilable proof containing explicit placeholders, so each placeholder is a well-defined subproblem. The exact repair choices are: remove one invalid line, remove a malformed nested block, or insert sorry when a block compiles but leaves goals open. The paper says, “At that point, every remaining sorry marks a sub-lemma to be proved in later stages of Apollo.”

When to use it: use it when syntax or local proof failures prevent the verifier from exposing later goals. This stage is scaffolding, never evidence of correctness; APOLLO’s final assembler rejects remaining placeholders.

How to do it: parse the proof tree; compile; locate the first offending line/block; apply the matching one of line removal (single invalid tactic), block removal (malformed sub-proof), or placeholder insertion (block compiles but leaves goals open); repeat until Lean compiles; record each placeholder with its local hypotheses, definitions, and preceding lemmas. Then hand those records to the solver and recursive LLM stage.

Verus form (inference): replace sorry with an assume(false) (or admit()) marker, which lets the rest of the function still verify, while retaining a machine-readable obligation record; a failing assert(false) would not play that role because the file would no longer verify with only warnings. In final Rust, every marker must be replaced by a proved assert, lemma, or invariant and verus must run with no admitted axioms. Unlike Lean’s nested proof syntax, Verus obligations may be generated from failed assertions, loop invariants, or function contracts; preserving source spans and the current environment is therefore essential.

Evidence and limits: Sorrifier and Proof Assembler are excluded from ablation because the authors call them essential to decomposition and assembly. The placeholder stage trusts only Lean’s parser/compiler for structural feedback; it proves nothing until final checking. Inference: deleting a line can change the intended proof context, so the extracted obligation may no longer represent the original argument if the repair is too aggressive.

technique 3: solver-first local closure

What it is: attempt cheap deterministic automation before spending LLM samples. APOLLO invokes Lean’s hint and then tries built-in solvers such as nlinarith, ring, and simp, wrapped in try so failures leave the obligation available for later repair. The paper observes that “Auto Solver, when used in isolation, also produces little accuracy gain,” but its combination with LLM re-invocation gives the strongest Kimina setting (75.0%); for o4-mini the 46.7% also needs Syntax Refiner.

How to do it: for each placeholder, restore its local context; invoke the hint; try the solver sequence; if the goal closes, replace the placeholder with the generated proof; otherwise retain the goal and its updated context for recursive proving. Recompile after substitutions.

Verus form (inference): map this to assert plus the Verus SMT backend, broadcast proof lemmas, and explicit calls to arithmetic lemmas. Try solver-friendly normalizations first (linear arithmetic, nonlinear arithmetic, rewriting, and trigger adjustments); only then ask the model to write a lemma. Verus does not provide Lean’s exact tactic combinators, so the agent should generate Rust proof code and rerun verus rather than emit tactic scripts.

Evidence and limits: in Table 4, Auto Solver alone gives Kimina 63.5% versus its 63.1% baseline, whereas Auto Solver plus LLM re-invocation gives 75.0%; all modules give 75.0%. The solver set is domain dependent and can time out or fail on goals that require a missing helper lemma.

technique 4: recursive sub-lemma proving and assembly

What it is: treat each unresolved placeholder as a new lemma, preserving hypotheses and previously proved facts, and recurse to a bounded depth. “This allows the Apollo to make progress in proving the original theorem by breaking down the incomplete steps further and further until the LLM or Auto Solver can close the goals.” The assembler then splices all repaired blocks and verifies that no sorry or admit remains.

How to do it: extract a block’s local context; prompt the LLM with only that subgoal and context; run syntax repair, placeholder extraction, and solver closure again; accept a closed block, or recurse on its children; after each round assemble and recompile the parent theorem; stop at depth r or full closure. Depth trades cost for accuracy: o4-mini gains most between depths 0 and 1 and then plateaus, while Kimina and Goedel improve through depth 6.

Verus form (inference): create helper proof fn/lemma functions with contracts that state each extracted obligation, prove them under the captured assumptions, and call them from the parent function. Preserve ownership-sensitive preconditions and mutable-state invariants explicitly; a Lean local context cannot simply be copied when Rust borrows or moves values. The final gate remains a clean Verus verification run with no assume or unproved external axiom.

Evidence and limits: repaired proofs are longer (the paper reports at least a twofold increase in mean tactic length for repaired proofs in each model), suggesting decomposition reaches harder structured arguments. The authors’ stated limitation is dependence on the base model’s proof sketch: missing critical lemmas or an irrelevant strategy may remain unrepairable. APOLLO also leaves interaction with BFS/MCTS unexplored.

what is proved, measured, and trusted

Lean’s kernel checks the final theorem; that is the soundness-critical component. APOLLO’s parser, line/block edits, solver selection, LLM prompts, and recursion policy are orchestration code and are trusted only to produce candidates, not to establish truth. Reported measurements are benchmark success, average samples, and generated-token budgets under the stated hardware and model versions. Observation by this study: the paper text gives no confidence intervals, per-problem paired outcomes, or an independent audit of baseline sampling procedures. “A theorem might need 100 lines of proof while a sub-lemma might need only 1 line” explains why sample and token counts do not scale one-to-one; comparisons using only sample counts can therefore mislead.

implications for VeruLaw

Inference: APOLLO is a direct design pattern for VL’s verified-Rust agent: compile early, classify diagnostics, preserve a compilable skeleton, solve local obligations cheaply, and recursively re-invoke the model only on failures. It threatens a product that relies on one-shot code generation because its measured gains come from feedback and decomposition rather than a larger base model. VL should not redo whole-proof sampling as its main strategy; it should instrument Verus diagnostics and measure paired success, tokens, and verification time. APOLLO does not solve specification adequacy, ownership-sensitive decomposition, or bad high-level algorithms, so those remain product risks.

techniques for the catalog

• compiler-guided staged repair — feed verifier diagnostics into syntax cleanup, placeholder extraction, solver attempts, recursive repair, and final reverification

• sorrifier obligation extraction — turn invalid nested proofs into compilable placeholders that expose local sub-lemmas without accepting them as proved

• solver-first local closure — try deterministic arithmetic and rewriting automation on each obligation before invoking an LLM

• recursive sub-lemma proving — recurse on unresolved local contexts, then assemble and reject any proof containing placeholders Audited 2026-10-12 against the paper: checked miniF2F-test setup, Table 1 and 2 rows (64.7 to 65.6 with 362 samples and 179K tokens; 70.8 to 75.0 with 307 samples and 1.3M tokens; o3-mini and o4-mini), Table 3 (10/658 vs 11/658), Table 4 ablation values, the 300-400 request claim, twofold proof length claim, algorithm steps of Syntax Refiner, Sorrifier, Auto Solver, recursion and assembler, limitations, and quotations. Changed: the Verus placeholder form now uses assume(false) or admit() as the sorry analogue instead of a failing assert (which would not verify); the least destructive ordering wording for Sorrifier (the paper gives three repairs by condition, not by destructiveness); marked the line-deletion remark and the absence-of-statistics remark as the study’s inference or observation; clarified that the Auto Solver plus LLM combination is strongest for Kimina, while o4-mini needs all three modules. Not checked: appendix (Algorithm 1, extra budget analysis) and figures beyond text extraction; Verus syntax checked from memory since the local Verus notes do not cover assume or admit.

Last edited: 2026-10-13