Skip to content

APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

🕒 Published (v1): 2025-01-01 · Source: NeurIPS · Venue: NeurIPS 2025 · link

Ask a follow-up

Open an assistant pre-loaded with this paper's context.

💬 Ask ChatGPT✦ Ask Claude

TL;DR

APOLLO is a modular, model-agnostic agentic framework that closes the loop between an LLM and the Lean4 proof assistant to repair failing formal proofs rather than regenerating them wholesale. By decomposing failed proofs into sub-lemmas, fixing syntax errors, invoking built-in solvers, and recursively re-prompting the LLM on isolated sub-goals, APOLLO achieves state-of-the-art 84.9% on miniF2F-test among sub-8B models while keeping sampling budgets under 100.

Problem

Standard automated theorem proving with LLMs relies on brute-force resampling (up to 25,600 attempts) and discards all compiler feedback, treating Lean's error output as a binary pass/fail signal. This wastes the rich diagnostic information the Lean REPL provides and is computationally expensive; general-purpose LLMs (o3-mini, o4-mini) additionally fail on syntax differences between Lean3 and Lean4, despite often producing structurally sound mathematical reasoning.

Method

APOLLO wraps any whole-proof LLM generator in a staged repair loop with four components:

  1. Syntax Refiner: corrects superficial Lean3→Lean4 syntax errors (keywords, brackets) using rule-based normalization before deeper analysis.
  2. Sorrifier: parses the proof into a tree of nested sub-proof blocks, compiles with Lean REPL, and replaces each failing block with a sorry placeholder (via line removal, block removal, or explicit sorry insertion), yielding a compilable skeleton with marked sub-goals.
  3. Auto Solver: attempts to close each sorry sub-goal using Lean's hint tactic and built-in solvers (nlinarith, ring, simp, etc.) with try wrappers.
  4. Recursive LLM Re-invocation: for remaining sorry blocks, extracts local context (hypotheses, intermediate lemmas) and re-prompts the LLM at a fixed top-32 budget, then recurses through all four stages up to user-specified depth r.

The Proof Assembler stitches repaired sub-proofs back into a single file and re-verifies via REPL. The entire pipeline iterates up to r rounds.

Key Contributions

  • Fully automated compiler-guided proof repair loop that replaces brute-force resampling with targeted sub-lemma decomposition and repair.
  • Syntax Refiner enabling general-purpose LLMs (o3-mini, o4-mini) to produce valid Lean4 from Lean3-biased outputs.
  • SOTA on miniF2F-test at 84.9% among sub-8B models (Goedel-V2-8B + Apollo, sampling budget 32, as of August 2025).
  • Demonstrated 1–2 orders-of-magnitude reduction in sampling and token budgets across five models spanning general-purpose and specialized provers.
  • Empirical analysis showing Apollo-repaired proofs are systematically longer (2×+ mean tactic count) than base-model proofs, indicating harder theorems solved.

Results

  • Goedel-V2-8B + Apollo: 84.9% on miniF2F-test at budget 32 (vs. 84.9% for base at budget 128, matching accuracy at one-quarter the samples); 0.9% absolute gain over Goedel-V2 baseline at same budget.
  • Goedel-Prover-SFT + Apollo: 65.6% (vs. 64.7% baseline at 25,600 samples) using only ~362 samples — a ~70× reduction in sample complexity.
  • Kimina-Prover-Preview-Distill-7B + Apollo: 75.0% at 1.3M tokens (vs. 70.8% at 4.5M tokens), +4.2% accuracy with <1/3 the token budget.
  • o3-mini + Apollo: 40.2% (up from 3.3% baseline, +36.9%); o4-mini + Apollo: 46.7% (up from 7.0%, +39.7%).
  • PutnamBench (Kimina-7B): 11/658 solved with Apollo vs. 10/658 at 192 samples, using only 108 samples and 579K tokens (vs. 1.1M).
  • Ablation: full Apollo (Syntax Refiner + Auto Solver + LLM Re-invoker) is necessary; individual modules alone contribute negligibly for specialized provers; LLM Re-invoker combined with Auto Solver drives most gains.

Limitations

  • Apollo does not integrate with tree-search methods (BFS, MCTS); interaction between sub-lemma decomposition and search-guided provers is unexplored.
  • Performance depends heavily on the base model's initial proof sketch quality; when the base model adopts an incorrect proof strategy (wrong approach, missing critical lemmas), Apollo cannot repair it.
  • Sampling overhead grows recursively with depth r and is problem-dependent, making fixed-budget comparisons difficult to state precisely.

Relevance to Agentic AI / LLM Agents

APOLLO is a concrete instance of a compiler-in-the-loop agentic architecture: rather than a single LLM call followed by binary evaluation, it constructs a multi-agent pipeline where specialized agents (syntax refiner, sorrifier, solver, recursive LLM invocator) each act on structured feedback from an external verifier. This exemplifies the broader principle of grounding LLM generation in formal tool feedback—replacing stochastic resampling with iterative, targeted repair—which is directly applicable to any agentic setting where a verifier (compiler, test suite, type checker) can provide structured error signals. The dramatic efficiency gains (1–2 OOM fewer samples for equivalent or higher accuracy) demonstrate that feedback-driven decomposition is a powerful design pattern for agentic systems operating in verifiable domains.