APOLLO is an automated theorem proving system that combines the Lean compiler and the reasoning power of LLM to prove mathematical theorems. While conventional LLM-based theorem proving methods generate proofs that pass verification systems through numerous (thousands) samplings, APOLLO uses a modular pipeline in which LLM generates proofs, agents correct syntactic errors in the proofs, Lean identifies mistakes, isolates failed sub-theorems, utilizes an automatic solver, and inexpensively calls LLM on the remaining objectives. This process of recombining and re-verifying the corrected sub-proofs is repeated up to a user-controllable maximum number of attempts. On the miniF2F benchmark, it achieves 84.9% accuracy among models with fewer than 8B parameters, while maintaining a sampling cost of less than 100. Furthermore, it improves the accuracy of GoedelProverSFT to 65.6% and reduces the sample complexity from 25,600 to several hundred.
