Technical Summary: Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean

Problem Statement

Large language models (LLMs) have achieved significant progress in automated theorem proving within the Lean proof assistant by employing agentic workflows. These workflows typically decompose complex problems into smaller lemmas, generate numerous proof attempts, and utilize compiler feedback to guide search. While this approach yields high performance on challenging benchmarks like PutnamBench, it suffers from prohibitive computational costs. Current systems often allocate fixed, pre-specified budgets for decomposition and proof generation to every problem, regardless of difficulty. This "fixed-step" policy leads to substantial waste, as agents frequently spend significant compute on infeasible problems or misformalized statements that are unlikely to succeed. The core challenge addressed is the lack of dynamic cost-awareness in existing agents, which fails to optimize the tradeoff between computational expenditure and proof success rates.

Methodology

The authors propose a novel Action Routing Agent architecture designed to replace static policies with dynamic, data-driven routing decisions. The system is conceptually divided into two planes:

1. Data Plane (Proof Generation)

Inspired by prior work (e.g., Chen et al., 2025c; Varambally et al., 2025), the data plane handles the actual generation of proofs. It operates through four modules:

• Breakdown Module: A general-purpose model (GPT-OSS-20B) decomposes the original problem into natural language lemmas and proof sketches.
• Formalizer: The agent formalizes these lemmas into Lean code using GOEDEL-FORMALIZER-V2-8B, selecting the best candidate that compiles without syntax or type errors.
• Formal Breakdown Prover: The system attempts to prove the top-level theorem using the formalized lemmas as axioms, guided by the natural language sketch.
• Lemma Prover: Once the breakdown is proven, the agent recursively attempts to prove the individual lemmas required by the proof, pushing new dependencies onto a stack.

2. Control Plane (Cost-Quality Routing)

The control plane observes the trajectory of failed proof attempts and decides whether to continue attempting the current target or terminate the trajectory to restart with a new breakdown. It utilizes a lightweight routing policy based on a cost-quality tradeoff:

• State ($s$): Summarizes the history of failed attempts, including proof attempts, compilation results, error messages, and output lengths.
• Action Space: $\{ \text{ATTEMPT}, \text{TERMINATE} \}$. The agent either samples another proof for the current target or discards the current breakdown.
• Utility Function: The router calculates a utility score $\tau(s) = \hat{q}(s) - \lambda\hat{c}(s)$, where:
  • $\hat{q}(s)$ is the predicted probability of success for the next attempt (Quality).
  • $\hat{c}(s)$ is the predicted cost of the next attempt (measured in LLM generation tokens/SFLOPs).
  • $\lambda$ is a hyperparameter controlling the penalty for computational cost.
• Decision Rule: If $\tau(s) > 0$, the agent continues; otherwise, it terminates the current trajectory.

Estimators:

• Cost Estimator: Assumes attempt costs are independent and identically distributed, using the average cost of previous attempts in the trajectory.
• Quality Estimator: A logistic regression model trained to predict success probability based on trajectory features, specifically:
  • Proof Similarity: The average pairwise fuzzy string ratio of normalized proofs (low similarity suggests confusion).
  • Error Diversity: The ratio of unique compilation errors to total errors (low diversity suggests a persistent failure mode).
  • Attempt Count: The number of previous attempts.

Key Contributions

1. Identification of Inefficiency: The paper identifies that fixed-step scaling in Lean agents is critically inefficient and that reducing unnecessary attempts is essential for a better cost-quality tradeoff.
2. Novel Architecture: The development of a lemma-style Lean prover equipped with an online, adaptive cost-quality router that dynamically evaluates the marginal value of additional compute.
3. Empirical Validation: Demonstration that the proposed router significantly decreases wasted compute while maintaining competitive accuracy, proving that failed trajectories contain actionable signals for resource allocation.

Experimental Results

The system was evaluated on a subset of 85 problems from PutnamBench, comparing the dynamic routing agent against a fixed-step baseline and an "oracle" agent with access to ground-truth success probabilities.

• Cost Reduction: At parity accuracy, the proposed agent reduced the required budget by 25.8% on average compared to the fixed-step baseline.
• Accuracy Improvement: At parity cost, the agent achieved a 7.8% improvement in solve rate.
• Specific Tradeoffs:
  • To achieve ~43.6% solve rate, the fixed-step baseline required 31.6 M SFLOPs, whereas the routing agent required only 22.6 M SFLOPs (a 28.4% cost reduction).
  • In a medium-budget regime (~41.6% solve rate), the agent reduced costs by 29.6% (17.5 M vs. 24.9 M SFLOPs).
• Ablation Studies:
  • Feature Importance: "Error diversity" was found to be the most critical feature for quality estimation.
  • Data Plane Impact: The lemma-style decomposition architecture itself improved the solve rate by nearly 100% over a whole-proof generation approach using the same 8B model, approaching the performance of a 32B model.
  • Oracle Gap: While the routing agent outperformed the fixed baseline significantly, a gap remains compared to the oracle agent (which achieved a 59.9% cost reduction), suggesting room for improvement in feature engineering and estimator architecture.

Significance and Claims

The paper claims that failed Lean trajectories provide actionable signals for cost-aware resource allocation in agentic theorem proving. By moving away from static, fixed-step policies toward dynamic routing, agents can significantly reduce computational waste without sacrificing performance. The authors position this work as a foundational step toward "cost-aware control" for formal mathematical proving, suggesting that future agents should dynamically allocate computation based on observed progress and failure patterns rather than assigning inference budgets statically. The results indicate that fixed-step policies leave substantial room for efficiency improvements, and that routing strategies can effectively mitigate unnecessary costs.