PaperlayerView exact revision on arXiv

Source-linked AI summary

EconProver: Towards More Economical Test-Time Scaling for Automated Theorem Proving

Mukai Li, Linfeng Song, Zhenwen Liang, Jiahao Xu, Shansan Gong, Qi Liu, Haitao Mi, Dong Yu

arXiv:2509.12603v1cs.CLcs.AI

TL;DR

ATP test-time scaling can impose substantial token and computational costs, while pass-count-focused analyses do not capture the differences between strategies. EconRL combines dynamic CoT switching with diverse parallel-scaled RL, and ECONPROVER-GD matches its backbone’s performance at 12% of its token consumption.

  • Problem

    Existing ATP cost analyses often regulate sampling-pass counts while neglecting token usage and iterative refinement, leaving computational trade-offs across scaling strategies incompletely characterized.

    Source: §1 · p. 2

  • Method

    EconRL combines preference-trained dynamic CoT/Non-CoT selection with independently PPO-trained proof prefixes for diverse parallel scaling.

    Source: §1 · p. 2, §3.1 · p. 5, §3.2 · p. 6

  • Results

    ECONPROVER-GD matches the backbone SOTA open-source ATP model’s performance while reducing token consumption to 12%.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The paper concludes that substantial test-time efficiency gains are possible without sacrificing proving capability.

    Source: §6 · p. 10

    The switching scheme classifies problems as base-solvable without CoT or CoT-dependent, requiring extended reasoning for successful proof completion.

    Source: §3.1 · p. 5

Abstract

from arXiv · show

Large Language Models (LLMs) have recently advanced the field of Automated Theorem Proving (ATP), attaining substantial performance gains through widely adopted test-time scaling strategies, notably reflective Chain-of-Thought (CoT) reasoning and increased sampling passes. However, they both introduce significant computational overhead for inference. Moreover, existing cost analyses typically regulate only the number of sampling passes, while neglecting the substantial disparities in sampling costs introduced by different scaling strategies. In this paper, we systematically compare the efficiency of different test-time scaling strategies for ATP models and demonstrate the inefficiency of the current state-of-the-art (SOTA) open-source approaches. We then investigate approaches to significantly reduce token usage and sample passes while maintaining the original performance. Specifically, we propose two complementary methods that can be integrated into a unified EconRL pipeline for amplified benefits: (1) a dynamic Chain-of-Thought (CoT) switching mechanism designed to mitigate unnecessary token consumption, and (2) Diverse parallel-scaled reinforcement learning (RL) with trainable prefixes to enhance pass rates under constrained sampling passes. Experiments on miniF2F and ProofNet demonstrate that our EconProver achieves comparable performance to baseline methods with only 12% of the computational cost. This work provides actionable insights for deploying lightweight ATP models without sacrificing performance.

1 Introduction

Current ATP scaling strategies can deliver strong proving performance but incur substantial inference costs that existing pass-count analyses do not fully capture. The paper proposes a token-level cost analysis and a two-stage EconRL pipeline, with ECONPROVER-GD matching backbone performance at 12% of its token consumption.

1 Introduction

  • Sequential scaling can use 10–15 times more tokens than methods without reflective CoT, while some configurations require 8192 attempts with over 10,000 tokens per proof attempt.Existing cost analyses often count sampling passes while overlooking token usage and iterative refinement.Source: §1 · p. 2
  • The authors propose measuring ATP inference cost by total generated tokens rather than sampling-pass count alone.They also report that 83% of miniF2F statements below IMO difficulty can be solved in Non-CoT mode using about one-tenth the CoT token budget, and observe redundancy across sampled outputs.Source: §1 · p. 2
  • EconRL stacks dynamic CoT switching with diverse parallel-scaled RL using specialized reasoning heads trained on difficulty-partitioned data.The first stage supports autonomous CoT/Non-CoT selection; the second targets solution diversity and parallel-scaling efficiency.Source: §1 · pp. 2–3
  • ECONPROVER-GD matches the backbone SOTA open-source ATP model’s performance while reducing token consumption to 12%.The paper presents this as its practical efficiency result.Source: §1 · p. 3

2 Analysis on Test-Time Scaling of ATP models

The analysis evaluates scaling by total generated-token cost, then compares sequential, parallel, and hybrid strategies on miniF2F. It finds distinct inefficiencies in long CoT reasoning and repeated parallel sampling, with their effects varying by problem difficulty and prefix diversity.

2.1 Token-Level Sampling Cost Quantification

  • The token-level sampling-cost metric sums initial generated tokens across passes and tokens generated during all refinement steps.It is proposed as a unified way to compare cost-performance trade-offs.Source: §2.1 · p. 3

2.2 Scaling Efficiency Curves

  • At PS=8, parallel scaling reaches 63.1% accuracy versus 58.6% for sequential scaling, using 443×8 tokens versus 4,488 tokens.Increasing parallel passes to 16 reaches 65.6%, another 2.5% increase, at sampling cost not significantly higher than sequential scaling.Source: §2.2 · p. 3
  • Parallel scaling gains diminish beyond a threshold: accuracy rises 4.9 points from 8 to 32 passes, but only 1.1% when passes double from 64 to 128.The latter increase accompanies exponential computational-cost growth.Source: §2.2 · p. 3
  • A hybrid using PS=32 achieves a 7.5% improvement at around 4% of the computational cost of PS=8192, whose improvement is 7%.Figure 2 compares sampling cost on a log scale with miniF2F-test accuracy across sequential, parallel, and hybrid scaling.Source: §2.2 · p. 3, Figure 2 · p. 3

2.3 Analysis on Scaling methods

  • Long CoT yields modest improvements on moderate-level problems but is more effective on Olympiad-level problems, where its gap over baseline approaches widens.The analysis categorizes miniF2F-dev problems by competition difficulty.Source: §2.3 · p. 4
  • Prefix diversity coverage strongly correlates with proving performance; scaling from 8 to 32 passes gains 6.1% total, while 128 passes add only 0.6% at 4× computational cost.The analysis tracks distinct 3-grams among the first 20 tokens after the formal statement, relative to 512 attempts.Source: §2.3 · p. 4, Figure 3 · p. 4

3 EconRL

EconRL combines dynamic CoT switching with diverse parallel-scaled RL to reduce unnecessary reasoning tokens and improve exploration under a limited pass budget. Its components use preference learning for mode selection and independently trained specialized prefixes for parallel proof attempts.

3 EconRL

  • EconRL combines dynamic CoT switching, which cuts unnecessary tokens on easy problems, with diverse parallel-scaled RL, which seeks more performance from a small pass budget.The authors state that combining the two techniques yields further experimental gains.Source: §3 · pp. 4–5

3.1 Dynamic Chain-of-Thought Switching

  • The switching mechanism distinguishes problems solvable by the base model without CoT from those requiring extended reasoning.Roughly 83% of solved problems below IMO difficulty for Deepseek-Prover-V2-7B are base-solvable; preference pairs favor direct proofs for these and CoT answers for CoT-dependent problems.Source: §3.1 · p. 5
  • Dynamic switching uses a unified prompt to select reasoning mode without explicit complexity indicators, with DPO preferences shaped by whether a problem is base-solvable or CoT-dependent.The preferred response is the direct proof for base-solvable problems and the full CoT answer for CoT-dependent problems.Source: §3.1 · pp. 5–6

3.2 Diverse Parallel-scaled RL

  • Diverse parallel-scaled RL learns specialized lightweight prefix heads to make proof attempts more diverse under limited sampling budgets.Problem difficulty is estimated from 32 base-prover attempts, then used to form bins and training shards paired with dedicated prefixes.Source: §3.2 · p. 6
  • Each prefix is trained independently with PPO, receiving reward 1 for a correct proof and 0 otherwise, and inference allocates sampling evenly across heads.The heads have no joint or coordinated updates; even allocation avoids per-problem head selection.Source: §3.2 · p. 6

4 Experiments

Across miniF2F-test and ProofNet-test, EconRL combines dynamic CoT switching with diverse parallel-scaled RL. The reported experiments show competitive proving performance with reduced sampling costs, including when iterative refinement is used.

4.1 Experimental Setup

  • miniF2F-test and ProofNet-test evaluate the approach on 244 and 186 Lean problems, respectively.The experiments use DeepSeek-Prover-V2 and Goedel-Prover-V2 backbones, with EconRL's dynamic CoT switching followed by diverse parallel-scaled RL.Source: §4.1 · pp. 6–7

4.2 Main Performance and Efficiency

  • 76.2% and 84.0% miniF2F-test accuracy are reported for ECONPROVER-DS and ECONPROVER-GD, respectively, alongside reduced costs and competitive performance across benchmarks.ECONPROVER-DS uses 15% of standard CoT token usage; with iterative refinement, EconRL preserves 86.0% accuracy while reducing token overhead by 75%.Source: Table 1 · p. 7, §4.2 · pp. 7–8

4.3 Ablation on Dynamic CoT Switching

  • Table 2 reports an ablation of dynamic CoT switching on DeepSeek-Prover-V2.Source: Table 2 · p. 8

4.4 Ablation on Diverse Parallel-scaled RL

  • 68.9% Pass@16 is reached with 8 random-grouped parallel heads, with no further gain at 16 heads.Increasing from 4 to 8 heads raises Pass@16 from 66.8% to 68.9%.Source: Table 3 · p. 8, §4.4 · p. 8
  • 70.5% at Pass@16 versus 65.6% for baseline Non-CoT, and 75.0% versus 73.0% with CoT, are reported for diverse parallel-scaled RL.The approach shows stronger benefits at lower pass counts; random heads alone provide minimal benefits.Source: Table 4 · p. 9, §4.4 · p. 9

5 Related Work

Related work covers whole-proof generation, verifier-guided proof search and refinement, and adaptive Chain-of-Thought methods. The paper positions dynamic CoT triggering as a new application of adaptive reasoning to formal theorem proving.

5.1 Formal Theorem Proving via whole proof generation

  • Whole-proof generation produces complete formal proofs in one forward pass, while explicit CoT can lengthen outputs and inflate token use (Ren et al., 2025).Source: §5.1 · p. 9

5.2 Formal Theorem Proving with Verifier Feedback

  • Verifier-feedback approaches include stepwise proof-state search and iterative refinement of complete proofs; exhaustive search and repeated refinement can require substantial computation.Source: §5.2 · pp. 9–10

5.3 Dynamic Chain-of-Thought

6 Conclusion and Future Work

EconRL combines dynamic CoT switching and diverse parallel-scaled reinforcement learning to improve ATP test-time scaling efficiency. The authors report efficiency gains without sacrificing proving capability and plan to extend the approach to iterative refinement.

6 Conclusion and Future Work

  • EconRL combines dynamic CoT switching with diverse parallel-scaled reinforcement learning to improve ATP test-time scaling efficiency.Source: §6 · p. 10
  • The authors report substantial efficiency gains without sacrificing proving capability.Source: §6 · p. 10
  • Future work will integrate both optimizations into iterative proving to reduce inference costs across three dimensions.Source: §6 · p. 10

Related papers

Loading 2509.12603v1…