PaperlayerView exact revision on arXiv

Source-linked AI summary

LEVER: Adaptive Cost-Aware Proof Search Over AND/OR Graphs

Nihal Jain, Shuangjie Yao, Begum Cicekdag, Zhuo Zhang, Suman Jana

arXiv:2610.11862v1cs.AI

TL;DR

LLM-powered theorem provers largely seek any correct proof, while proof quality and the cost of finding proofs can vary. LEVER guides search with programmable objectives over partial proofs. On PutnamBench, it reduces cost while raising the solve rate against a strong single-conversation agent, and it supports search-time quality optimization.

  • Problem

    LLM-powered theorem provers largely search for any correct proof and improve proof quality only afterward, despite correct proofs varying in quality and computational cost.

    Source: §1 · p. 1

  • Method

    LEVER scores partial proofs over an AND/OR graph using realized objective values and predictions for open goals, guiding search under programmable objectives while Lean checks correctness.

    Source: §1 · p. 2, §3.3 · p. 5

  • Results

    34% lower average cost and a 96.3% solve rate versus 80.0% for a strong single-conversation agent on PutnamBench under a $3 budget.

    Source: §1 · p. 2

  • Takeaways & Limitations

    A single objective weight traces a quality–cost trade-off, letting users choose how much proof quality is worth paying for.

    Source: §5.2 · p. 9, §6 · p. 10

    With exact priors, backed-up values are exact, but real value functions are noisy and their theoretical analysis is left for future work.

    Source: §3.3 · p. 5

Abstract

from arXiv · show

Mathematicians value proofs for more than correctness: among correct proofs, simplicity, purity and the computational cost of finding them vary widely. Yet LLM-powered theorem provers largely search for any correct proof, and improve its quality only after it is found. We propose LEVER, a proof search algorithm that makes the objective over correct proofs programmable and optimizes it during search. LEVER scores partial proofs over an AND/OR proof graph, combining realized objective values with predictions for open subgoals, so the objective guides search before a proof is complete. The same mechanism optimizes computational cost, proof length, topical impurity, and even their weighted combinations, while the Lean kernel enforces correctness. On PutnamBench in Lean 4, under matched budgets, LEVER costs 34% less than a strong single-conversation agent while raising the solve rate from 80% to 96%. On reducing topical impurity, i.e., how far a proof strays from its theorem's subject, it improves over post-hoc refactoring (42% reduction against 33%) at two-thirds of the cost and more reliably; on proof length, the metric refactoring is built for, it approaches refactoring. Varying the objective's weights traces a quality-cost trade-off curve, so the user can choose how much a better proof is worth. Overall, LEVER is a performant, cost-efficient and tunable proof search algorithm for navigating the space of correct proofs.

1 INTRODUCTION

LEVER treats proof quality and search cost as objectives to optimize while finding correct proofs, rather than as concerns to address only after a proof is found. On PutnamBench, it improves solve rate while reducing cost, and supports search-time optimization of proof quality.

1 INTRODUCTION

  • Proofs can differ in simplicity, purity, explanatory value, length, and the computational cost of finding them, making the choice among correct proofs consequential.Current LLM-powered provers largely find any verified proof and leave quality improvement to post-hoc refactoring.Source: §1 · p. 1
  • LEVER scores partial proofs by combining realized values for proved parts with predictions for open goals, then expands the partial proof with the best score.Its AND/OR graph represents alternative decompositions and the subgoals each argument requires; the Lean kernel checks decompositions and the assembled proof.Source: §1 · pp. 1–2
  • On PutnamBench, LEVER raises the solve rate under a $3 budget from 80.0% to 96.3% while reducing average cost from $1.44 to $0.95, a 34% reduction.The comparison uses the same model and budget allocation as a strong single-conversation agent.Source: §1 · p. 2
  • Search-time optimization outperforms refactoring on topical impurity at two-thirds its cost, approaches refactoring on proof length, and traces quality–cost trade-off curves.The curves let users choose how much quality is worth paying for.Source: §1 · p. 2

2 RELATED WORK

Related work spans theorem provers that generate tactics, whole proofs, or decompositions, alongside value-guided search and post-hoc proof refactoring. LEVER distinguishes itself by using an explicit objective over computational cost and proof quality to guide search.

2 RELATED WORK

  • The theorem-proving landscape includes tactic generation, whole-proof generation, and decomposition-based systems, while proof-quality work also includes post-hoc refactoring.The systems discussed largely search for any correct proof; refactoring improves a finished proof.Source: §2 · p. 2
  • Value-guided approaches include heuristic search over AND/OR graphs, learned values in tree search and proof search, and learned cost-to-go for retrosynthesis.LEVER uses stochastic expansions, learns priors from paid draws, and composes remaining computational cost with arbitrary proof metrics.Source: §2 · pp. 2–3

3 LEVER

LEVER represents proof search with an AND/OR graph and selects partial proofs using backed-up costs and estimates for open goals. Its iterative search expands goals, updates estimates from realized attempts, and returns the best solution subgraph found within budget.

3.1 BACKGROUND

  • An AND/OR graph represents goals as OR nodes and decompositions as AND nodes; a solution selects one decomposition per goal and includes every subgoal it requires.Solved leaves complete the solution subgraph, which maps to a unique Lean proof.Source: §3.1 · p. 3
  • At AND nodes, costs sum across subgoals, while OR nodes take the cheapest decomposition; the root value gives the cheapest solution cost.Solved leaves have value 0, false goals have value ∞, and the minimizing choices reconstruct the solution.Source: §3.1 · p. 3

3.2 PROOF SEARCH

  • Proof search is modeled as an MDP whose state is the current graph, whose actions expand goals or stop, and whose expansions can produce different decompositions.The policy minimizes expansion spend plus the root’s solution cost; when spend is sunk, it chooses based on expected remaining spend and solution cost.Source: §3.2 · p. 3

3.3 ADAPTIVE PROOF SEARCH WITH LEVER

  • LEVER iteratively selects goals along the current best solution subgraph, expands them, attaches priors to new subgoals, and backpropagates values until it stops or exhausts its budget.The returned proof is the best solution subgraph at the root.Source: §3.3 · p. 4
  • A prior can make an interior goal worth expanding again; selection follows the best path and redraws only when the prior beats the incumbent by factor δ.Figure 2 illustrates a prior beating a realized attempt, which triggers another expansion and updates values up to the root; the earlier attempt remains in the graph.Source: §3.3 · p. 4, Figure 2 · p. 4
  • LEVER updates each goal’s prior from realized decomposition costs, treating the prior as n draws and each observed draw as one; failed attempts instead raise the estimate by σ.The method models log costs around an unknown mean and uses the posterior geometric mean as the updated value estimate.Source: §3.3 · p. 5
  • LEVER combines remaining computational cost with weighted graph-composable metrics, while exact backed-up values require exact priors; noisy-prior theory is left for future work.Computational spend already incurred cannot be optimized, so realized edges add nothing to remaining cost and open goals contribute their prior estimates. When a shared subgoal is charged once, finding the cheapest solution subgraph is NP-hard in general; LEVER assigns each shared subgoal a single owner.Source: §3.3 · p. 5

4 IMPLEMENTING LEVER WITH LEAN

LEVER’s Lean implementation sets up controlled PutnamBench comparisons, expands proofs through an agentic workflow, and scores computational cost and proof-quality objectives using value estimates for open goals.

4.1 SETUP

  • 80 evaluation problems come from PutnamBench ranks 51–150 by NearAI solve cost, with costs repriced at a fixed 90% cache-hit rate.Twenty problems from the same slice calibrate the value functions.Source: §4.1 · p. 5

4.2 AGENTIC SYSTEM DESIGN

  • Each goal expansion is an LLM conversation that can open helper subgoals or submit a complete proof; assembled solutions must compile in Lean without sorry or admit.A planner’s informal proof accompanies expansions, and subgoals inherit compacted parent context; planning cost is included.Source: §4.2 · pp. 5–6

4.3 COST OBJECTIVES

  • Correctness is enforced by assigning unsolved goals infinite cost, while computational cost measures LLM-call dollars and search minimizes estimated remaining cost.Each expansion replaces part of the estimate with its realized cost.Source: §4.3 · p. 6
  • Proof length counts added Lean tokens, while topical impurity counts references outside the theorem’s subject and infrastructure directories as a proxy for mathematical purity.The length metric can be gamed by short tactics that do not explain the mathematics.Source: §4.3 · pp. 6–7

4.4 VALUE FUNCTIONS

  • Open-goal cost and length use LLM predictions from seven log2 bins, while impurity uses a constant estimate of four references.Length estimates use 0.2 times the bin center; calibration measures prediction error and outcome spread to set the redraw margin.Source: §4.4 · p. 7

5 EXPERIMENTS

The experiments compare cost-aware proof search and search-time proof-quality optimization under shared model, Lean, and pricing settings. On PutnamBench, LEVER improves solve rate while reducing cost, and quality runs compare metric reductions against NearAI’s proofs.

5.1 OPTIMIZING COMPUTATIONAL COST

  • The cost experiment uses the NearAI single-conversation agent as its baseline, with matched model, prices, and Lean version; LEVER uses a $3 budget and direct-proof rules for sufficiently deep or low-priced goals.Unsolved problems are charged the full budget.Source: §5.1 · p. 7, §5 · p. 7
  • At a $3 budget, LEVER solves 96.3% of problems versus NearAI’s 80.0% and costs 34% less.The comparison covers 80 evaluation problems; from $0.25 on, LEVER solves more problems at almost every budget.Source: §5.1 · p. 7, Table 1 · p. 8, Figure 4 · p. 8
  • LEVER can reject a decomposition predicted to cost more than its goal and try another, but abandoned subgraphs still consume budget.The paper reports such cases are rare, and redraws do not always save cost.Source: §5.1 · p. 8

5.2 PROOF QUALITY OPTIMIZATION

  • Quality optimization tests topical impurity and proof length on 20 problems, using LEVER objectives that combine computation cost with a weighted quality metric.Runs use a $4.5 budget; instruction-guided search and post-hoc refactoring serve as comparison baselines.Source: §5.2 · p. 8
  • 42% impurity reduction at λ = 0.1 costs $1.85 per problem, versus 33% reduction at $2.88 for + Refactor.LEVER’s per-problem reduction standard deviation is 32 points, compared with 101 for + Refactor; + Instruct makes proofs 11% less pure than baseline.Source: Figure 5 · p. 9, Table 2 · p. 9, §5.2 · p. 9
  • At λ = 10−3, LEVER makes proofs 21% shorter at $2.59 per problem, approaching + Refactor’s 31% shortening at $1.83.The paper notes that searching for short proofs may be harder than finding a correct proof and then refactoring it.Source: §5.2 · p. 8, Figure 5 · p. 9, Table 2 · p. 9
  • Raising λ traces a cost-quality trade-off curve; shortening proofs also reduces impurity, while optimizing impurity alone can make proofs longer.The reported changes are +4% to −21% for length alongside +1% to −18% for impurity when shortening, and +1% to −42% for impurity alongside +4% to +10% for length when optimizing impurity.Source: §5.2 · p. 9

6 CONCLUSION

LEVER makes objectives over correct proofs programmable and optimizes them during search, with proof construction organized around helpers and shared subgoals. The conclusion reports lower cost with more solved problems and search-time proof-quality gains on PutnamBench.

6 CONCLUSION

  • LEVER treats correctness as a constraint while optimizing programmable objectives over correct proofs during search.The conclusion reports 34% lower cost and 96% versus 80% solved on PutnamBench, plus impurity gains over refactoring at two-thirds its cost and near-refactoring results on length.Source: §6 · p. 10

A LEVER: SYSTEM DESIGN

  • Proof files can introduce closed helpers proved in place and open helpers left as subgoals for later sessions.The target proof must be complete, and helper declarations follow specified acceptance constraints.Source: A LEVER: SYSTEM DESIGN · p. 16
  • Shared subgoals are represented by common OR nodes and proved once; LEVER assigns each shared subgoal an owner to keep its cost accounting stable.The paper notes that finding the cheapest solution subgraph under shared-subgoal accounting is NP-hard.Source: A LEVER: SYSTEM DESIGN · p. 16
  • A failed attempt incurs its spend and raises the goal’s estimate by one σ, while a reported false goal is closed with infinite value.When the root is solved, the assembled solution is checked by the Lean kernel.Source: A LEVER: SYSTEM DESIGN · p. 16

B TOPICAL IMPURITY

Topical impurity counts library-theorem references outside the theorem’s subject, using Lean’s elaborated proof dependencies and a directory-based subject proxy. The authors illustrate the metric on a Putnam problem and discuss both a helper-lemma gaming risk and limits of the proxy.

B TOPICAL IMPURITY

  • The implementation traces theorem references through local helper proofs, counting eligible Mathlib references while excluding declarations resting on sorry.It reads elaborated declarations and follows helper statements recursively to identify additional library names.Source: B TOPICAL IMPURITY · p. 20
  • The metric counts cited library theorems as impure when their concepts or locations fall outside the subject inferred from the theorem statement.It excludes machinery and treats generic lemmas as root concepts; Mathlib directories help assign subject locations.Source: B TOPICAL IMPURITY · pp. 20–21
  • On putnam 1964 b4, NearAI’s proof cites 44 impure theorems, while LEVER’s proof at λ = 0.1 cites 8.LEVER’s references were mostly from the linear algebra of the circles’ planes, versus NearAI’s topology, convexity, and group actions.Source: B TOPICAL IMPURITY · p. 21
  • At λ = 0.1, charging every off-subject helper as one more impure reference lowers LEVER’s mean impurity reduction by under one point.LEVER uses more helpers at λ = 0.1 than at λ = 0, but only slightly more off-subject helpers.Source: B TOPICAL IMPURITY · p. 21
  • The proxy relies on Mathlib’s organization and a pilot-corpus infrastructure set, counts references equally, and only indirectly charges local re-proofs of off-subject lemmas.An essential cross-field detour therefore counts the same as a routine lemma from another field.Source: B TOPICAL IMPURITY · p. 21

C.1 PROBLEM SELECTION

The controlled evaluation uses a tractable slice of PutnamBench ranked by the published NearAI run’s solving cost. The selected problems are hard for the agent but feasible for repeated method comparisons.

C.1 PROBLEM SELECTION

  • The evaluation draws ranks 51–150, randomly split into 20 calibration problems and 80 evaluation problems.These ranks were selected from PutnamBench ordered by the token cost of NearAI’s cheapest solving attempt.Source: §C.1 · p. 21, Table 3 · p. 21
  • The hardest 50 were excluded because controlled comparisons were impractical; the selected slice had a 1.5-hour median solving time for NearAI.In the top 50, 20 problems needed multiple attempts and one took 5.5 days.Source: §C.1 · p. 21

C.2 VALUE FUNCTIONS

LEVER predicts values for open goals using calibrated value functions, with metric-specific estimates and redraw rules. Held-out calibration results quantify prediction accuracy and variation across repeated draws.

C.2 VALUE FUNCTIONS

  • Table 4 reports ρ as prediction error, σ as draw variation, n = σ2/ρ2 as prediction weight, and δ as the redraw factor.The reported error is measured on held-out calibration goals; its scale is log space for cost and length and references for impurity.Source: Table 4 · p. 22, §C.2 · p. 22
  • For computational cost and length, an LLM assigns open goals to seven log-scale bins and LEVER prices each at its bin’s geometric center.For length, the estimate is scaled to 0.2 times the bin center; impurity instead uses a constant estimate of 4 references.Source: §C.2 · p. 22
  • Cost predictions fall in the right bin 34% of the time and within one bin 75%; length predictions do so 40% and 89%, respectively.Cost predictions are low by a factor of 1.53 on average, while length predictions show no systematic bias.Source: §C.2 · p. 22
  • For cost and length, redraws must promise an improvement of one spread, δ = e^σ; for impurity, δ = 1.72 references.The impurity estimate of 4 references is the calibration goals’ 25th percentile.Source: §C.2 · p. 22

C.3 CACHE-HIT RATES AND ACTUAL COST

The appendix compares LEVER and NearAI under shared and observed cache-hit pricing. LEVER’s solve-rate and cost advantage persists across the reported pricing conditions.

C.3 CACHE-HIT RATES AND ACTUAL COST

  • NearAI’s single long conversation and LEVER’s shorter per-goal contexts produce different cache-hit rates; Table 5 reports per-call and per-token rates.Per-call is the mean fraction of each prompt read from cache; per-token is cached input tokens divided by all input tokens.Source: §C.3 · p. 22, Table 5 · p. 22
  • At common cache-hit rates from 90% to 97%, LEVER solves more problems and costs 29–34% less than NearAI.Table 6 reapplies Table 1’s $3 budget rule to each pricing condition.Source: §C.3 · p. 22, Table 6 · p. 23
  • At each method’s observed per-call rate, LEVER costs 12% less; at actual cache hits, it costs 16% less.Table 6 reports both per-call-rate and actual-cost comparisons.Source: §C.3 · p. 23, Table 6 · p. 23

C.4.1 REJECTING A COSTLY DECOMPOSITION: P U T N A M 1972 A3

LEVER rejects a costly decomposition before attempting its subgoals and keeps a cheaper alternative. The quality baselines use the same agent and objective wording, comparing optimization from the statement with post-hoc rewriting of a finished proof.

C.4.1 REJECTING A COSTLY DECOMPOSITION: P U T N A M 1972 A3

  • $1.54 in first-decomposition subgoals exceeded δ = 1.85 times the $0.72 root prior, so search rejected it before trying any; the $0.91 second decomposition was proved at $1.75 total cost.Figure 6 labels attempt costs on edges and value-function prices on subgoals.Source: §C.4.1 · p. 23, Figure 6 · p. 23

C.5 QUALITY BASELINES

  • Both quality baselines append LEVER’s objective wording to the unchanged NearAI agent, with the same model, prices, and Lean version as §4.1.The impurity prompt uses the theorem subject identified by the same probe as the metric; the length prompt asks for the shortest complete proof under the metric’s Lean-token definition.Source: §C.5 · pp. 23–24
  • Instruct starts from the problem statement and is capped at $4.5.It is asked to solve the problem with the objective in its system prompt.Source: §C.5 · p. 23
  • Refactor starts from NearAI’s finished proof and rewrites it for the objective while preserving a proof of the same theorem.Its cap is $4.5 minus NearAI’s run cost, and its reported cost includes that initial run.Source: §C.5 · pp. 23–24
  • The impurity objective defines staying within the theorem’s subject by avoiding declarations from other fields, while permitting general Mathlib infrastructure.The prompt also asks for helpers to stay within the subject and permits changing the full-proof formalization strategy.Source: §C.5 · p. 24

D THEORETICAL JUSTIFICATION FOR LEVER

The formalization proves that backup values exactly characterize minimum solution-subgraph costs on acyclic AND/OR graphs with nonnegative additive costs. It also specifies how costs and priors are represented in this result.

D THEORETICAL JUSTIFICATION FOR LEVER

  • A solution’s cost sums edge costs over its tree unfolding, counting shared subgoals once per use; an exact prior estimate enters as a childless AND node.The formalization represents ∞ as none : Option Nat.Source: D THEORETICAL JUSTIFICATION FOR LEVER · p. 24
  • The formalization uses a finite-branching AND/OR DAG with natural-number costs and an acyclicity rank that strictly decreases along every edge.The theorem covers any V satisfying the backup equations, and establishes that these equations uniquely determine optimal solution costs.Source: D THEORETICAL JUSTIFICATION FOR LEVER · p. 24
  • For acyclic AND/OR graphs with nonnegative additive costs, V(n) equals the minimum solution-subgraph cost when finite, and V(n) = ∞ exactly when no solution exists.The exactness claim is formalized in Lean 4 without Mathlib.Source: D THEORETICAL JUSTIFICATION FOR LEVER · pp. 24, 27
Loading 2610.11862v1…