Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
For researchers using LLMs for formal theorem proving, this work provides a cost-aware method to reduce compute waste without sacrificing proof success rates.
The authors address the high computational cost of LLM-based formal theorem proving in Lean by introducing an action routing agent with a control plane that decides whether to continue or restart based on cost and success likelihood. On a subset of PutnamBench, their agent reduces cost by 25.8% on average while maintaining performance.
Large language models (LLMs) are increasingly used in workflows for generating formal proofs in Lean. These workflows often decompose problems into smaller lemmas, sample many proof attempts, and use compiler feedback to guide search. However, they can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail. In this work, we address this problem with an action routing agent that consists of a data plane and a control plane. The data plane generates natural-language lemma decompositions, formalizes them in Lean, and samples proof attempts for the resulting theorem and lemma targets. The control plane observes previous failed Lean attempts, estimates both the likelihood of success and cost of another attempt, and decides whether to continue proving the current target or restart from a new breakdown. On a subset of PutnamBench, our agent decreases the cost by $25.8\%$ over a fixed-step baseline on average, preserving performance while using substantially less compute. These results suggest that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving.