ETH Zurich Cuts AI Theorem Proving Costs by 26% Without Losing Accuracy
A new routing agent cuts compute costs by 26% in LLM-based Lean theorem provers without sacrificing solve rates, by learning when to give up on a failing proof.
- 26% cheaper proofs: A new routing agent cuts compute costs by 25.8% on PutnamBench while maintaining the same solve rate as fixed-step baselines.
- Smart quitting: The agent reads failure signals from past proof attempts to decide whether to keep trying or restart with a new problem decomposition.
- Two-plane architecture: A data plane handles lemma decomposition and proof generation; a lightweight control plane routes decisions using logistic regression on just three features.
- Key signals: Error diversity, proof similarity across attempts, and attempt count are the three features that predict whether the next proof attempt is worth trying.
- Data plane bonus: The lemma decomposition pipeline nearly doubles the solve rate of Goedel-Prover-V2-8B, matching the much larger 32B model.
- Open source: Code is available at github.com/eth-sri/optimizing-lean-agents.
Automated theorem proving with LLMs has become one of the most exciting frontiers in AI research, but it comes with a dirty secret: it is extraordinarily expensive. State-of-the-art agentic systems that prove theorems in Lean, a formal proof language where every logical step is verified by a compiler, routinely spend tens of dollars per problem. One recent system reportedly spent $50 per problem to achieve a perfect score on Putnam 2025. A new paper from ETH Zurich asks a simple question: what if the agent knew when to quit?
Large language models 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. The problem is that most of those attempts fail, and the system keeps trying anyway. They can be prohibitively expensive, often spending substantial compute on attempts that ultimately fail.
The $40-per-problem problem
Existing agents typically scale compute through fixed policies, where every input receives the same pre-specified budgets for decomposition, proof generation, and self-correction. This can waste significant compute on infeasible problems or on misformalized statements. Think of it like a student who spends equal time on every exam question, regardless of whether they have any idea how to solve it. The smarter move is to recognize a dead end and move on.
To mitigate this, the authors adapt and extend existing works in the routing and cascading literature to the setting of Lean theorem proving with agentic workflows, proposing a novel agent architecture that uses a lightweight router to dynamically evaluate the expected cost and quality of future proof attempts based on the agent's past trajectory. The key insight is that failed proof attempts are not just noise, they are signal.
A two-layer architecture
The system is split into two conceptually distinct layers: a data plane that does the actual proving work, and a control plane that watches the data plane and decides whether to keep going or cut losses.
The data plane follows a lemma decomposition strategy:
This story is for Pro members
You've reached the end of the free preview. Upgrade to AlphaSignal Pro to read the full article - and everything else behind the paywall.
Comments
