APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning

TL;DR

APOLLO tackles the challenge of generating fully verified formal proofs with LLMs by introducing a modular, compiler-guided agentic framework that tightly couples LLMs with the Lean proof assistant and automated solvers. Through a sequence of components—Syntax Refiner, Sorrifier, Auto Solver, recursive repair, and Proof Assembler—APOLLO converts an initial LLM proof sketch into a complete Lean4 proof, leveraging Lean’s REPL feedback iteratively. Empirical evaluation on miniF2F shows APOLLO achieves new state-of-the-art accuracy for sub‑8B models (e.g., 84.9% on Goedel-V2) while dramatically reducing sampling budgets, and it also yields substantial gains for general-purpose models (up to ~40% accuracy). The results indicate that targeted, compiler-guided repair and recursive proof decomposition offer a scalable path to more reliable automated theorem proving with practical resource footprints.

Abstract

Formal reasoning and automated theorem proving constitute a challenging subfield of machine learning, in which machines are tasked with proving mathematical theorems using formal languages like Lean. A formal verification system can check whether a formal proof is correct or not almost instantaneously, but generating a completely correct formal proof with large language models (LLMs) remains a formidable task. The usual approach in the literature is to prompt the LLM many times (up to several thousands) until one of the generated proofs passes the verification system. In this work, we present APOLLO (Automated PrOof repair viaLLM and Lean cOllaboration), a modular, model-agnostic agentic framework that combines the strengths of the Lean compiler with an LLM's reasoning abilities to achieve better proof-generation results at a low token and sampling budgets. 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 repaired sub-proofs are recombined and reverified, iterating up to a user-controlled maximum number of attempts. On the miniF2F benchmark, we establish a new state-of-the-art accuracy of 84.9% among sub 8B-parameter models (as of August 2025) while keeping the sampling budget below one hundred. Moreover, Apollo raises the state-of-the-art accuracy for Goedel-Prover-SFT to 65.6% while cutting sample complexity from 25,600 to a few hundred. General-purpose models (o3-mini, o4-mini) jump from 3-7% to over 40% accuracy. Our results demonstrate that targeted, compiler-guided repair of LLM outputs yields dramatic gains in both efficiency and correctness, suggesting a general paradigm for scalable automated theorem proving.

Figures (16)

• Figure 1: The summary of whole-proof generation pipeline vs. proposed Apollo agentic pipeline. LLM refers to a chosen formal theorem generator model.
• Figure 2: Overview of the Apollo framework.
• Figure 3: Performance of base models against the Apollo aided models on miniF2F-test dataset at different sample budgets and token length.
• Figure 4: Distribution of proof lengths for selected models before (left) and after (right) applying Apollo. In the “before” plots, proof lengths cover only proofs the base model proved without the help of Apollo; in the “after” plots, proof lengths cover only proofs proved with Apollo’s assistance.
• Figure 5: Performance of Apollo on miniF2F dataset at various recursion depth parameters $r$ on three different models: o4-mini, Kimina‑Prover‑Preview‑Distill‑7B and Goedel‑Prover‑SFT.