EconProver : Vers une mise à l'échelle plus économique au moment des tests pour la démonstration automatique de théorèmes

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

Les modèles de langage de grande taille (LLMs) ont récemment fait progresser le domaine de la démonstration automatique de théorèmes (ATP), obtenant des gains de performance substantiels grâce à des stratégies de mise à l'échelle largement adoptées lors des tests, notamment le raisonnement réflexif en chaîne de pensée (Chain-of-Thought, CoT) et l'augmentation des passes d'échantillonnage. Cependant, ces deux approches introduisent une surcharge computationnelle significative pour l'inférence. De plus, les analyses de coût existantes régulent généralement uniquement le nombre de passes d'échantillonnage, tout en négligeant les disparités substantielles dans les coûts d'échantillonnage introduites par différentes stratégies de mise à l'échelle. Dans cet article, nous comparons systématiquement l'efficacité des différentes stratégies de mise à l'échelle pour les modèles ATP et démontrons l'inefficacité des approches open-source actuelles de pointe (SOTA). Nous explorons ensuite des approches pour réduire significativement l'utilisation de tokens et le nombre de passes d'échantillonnage tout en maintenant la performance originale. Plus précisément, nous proposons deux méthodes complémentaires qui peuvent être intégrées dans un pipeline EconRL unifié pour des bénéfices amplifiés : (1) un mécanisme de commutation dynamique de la chaîne de pensée (CoT) conçu pour atténuer la consommation inutile de tokens, et (2) un apprentissage par renforcement (RL) parallèle et diversifié avec des préfixes entraînables pour améliorer les taux de réussite sous un nombre contraint de passes d'échantillonnage. Les expériences sur miniF2F et ProofNet démontrent que notre EconProver atteint des performances comparables aux méthodes de référence avec seulement 12 % du coût computationnel. Ce travail fournit des insights exploitables pour déployer des modèles ATP légers sans sacrifier la performance.

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.