EconProver: Auf dem Weg zu einer wirtschaftlicheren Skalierung zur Testzeit für automatisiertes Theorembeweisen

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

September 16, 2025

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

cs.AI

papers.abstract

Große Sprachmodelle (LLMs) haben kürzlich das Feld des automatisierten Theorembeweisens (ATP) vorangetrieben und durch weit verbreitete Skalierungsstrategien zur Testzeit erhebliche Leistungssteigerungen erzielt, insbesondere durch reflektierende Chain-of-Thought (CoT)-Argumentation und erhöhte Sampling-Durchläufe. Beide Ansätze führen jedoch zu einem erheblichen Rechenaufwand für die Inferenz. Darüber hinaus regulieren bestehende Kostenanalysen typischerweise nur die Anzahl der Sampling-Durchläufe, während die erheblichen Unterschiede in den Sampling-Kosten, die durch verschiedene Skalierungsstrategien entstehen, vernachlässigt werden. In diesem Artikel vergleichen wir systematisch die Effizienz verschiedener Skalierungsstrategien zur Testzeit für ATP-Modelle und zeigen die Ineffizienz der derzeitigen State-of-the-Art (SOTA) Open-Source-Ansätze auf. Anschließend untersuchen wir Ansätze, um die Token-Nutzung und die Anzahl der Sampling-Durchläufe erheblich zu reduzieren, während die ursprüngliche Leistung beibehalten wird. Konkret schlagen wir zwei komplementäre Methoden vor, die in eine einheitliche EconRL-Pipeline integriert werden können, um verstärkte Vorteile zu erzielen: (1) einen dynamischen Chain-of-Thought (CoT)-Wechselmechanismus, der entwickelt wurde, um unnötigen Token-Verbrauch zu reduzieren, und (2) diverse parallel skalierte Verstärkungslernen (RL) mit trainierbaren Präfixen, um die Erfolgsrate bei begrenzten Sampling-Durchläufen zu erhöhen. Experimente auf miniF2F und ProofNet zeigen, dass unser EconProver eine vergleichbare Leistung zu Baseline-Methoden mit nur 12 % der Rechenkosten erreicht. Diese Arbeit bietet umsetzbare Erkenntnisse für den Einsatz von leichtgewichtigen ATP-Modellen ohne Leistungseinbußen.

English

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.