EconProver: Verso un Ridimensionamento più Economico al Momento del Test per il Teorema Automatico

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

September 16, 2025

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

cs.AI

Abstract

I Large Language Model (LLM) hanno recentemente fatto progredire il campo del Teorema Automatico (ATP), ottenendo miglioramenti significativi delle prestazioni attraverso strategie di scalatura ampiamente adottate durante il test, in particolare il ragionamento riflessivo a Catena di Pensiero (Chain-of-Thought, CoT) e l'aumento dei passaggi di campionamento. Tuttavia, entrambe introducono un sovraccarico computazionale significativo per l'inferenza. Inoltre, le analisi dei costi esistenti tipicamente regolano solo il numero di passaggi di campionamento, trascurando le sostanziali disparità nei costi di campionamento introdotte da diverse strategie di scalatura. In questo articolo, confrontiamo sistematicamente l'efficienza di diverse strategie di scalatura durante il test per i modelli ATP e dimostriamo l'inefficienza degli approcci open-source allo stato dell'arte (SOTA). Successivamente, indaghiamo approcci per ridurre significativamente l'uso di token e i passaggi di campionamento mantenendo le prestazioni originali. Nello specifico, proponiamo due metodi complementari che possono essere integrati in una pipeline unificata EconRL per benefici amplificati: (1) un meccanismo di commutazione dinamica della Catena di Pensiero (CoT) progettato per mitigare il consumo inutile di token, e (2) un apprendimento per rinforzo (RL) parallelo-scalato diversificato con prefissi addestrabili per migliorare i tassi di successo sotto vincoli di passaggi di campionamento. Gli esperimenti su miniF2F e ProofNet dimostrano che il nostro EconProver raggiunge prestazioni comparabili ai metodi di base con solo il 12% del costo computazionale. Questo lavoro fornisce intuizioni pratiche per il dispiegamento di modelli ATP leggeri senza sacrificare le prestazioni.

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.