EconProver: Rumo a uma Escalabilidade Mais Econômica em Tempo de Teste para Prova Automática de Teoremas

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

September 16, 2025

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

cs.AI

Resumo

Modelos de Linguagem de Grande Escala (LLMs) avançaram recentemente o campo da Prova Automática de Teoremas (ATP), alcançando ganhos substanciais de desempenho por meio de estratégias amplamente adotadas de escalonamento em tempo de teste, notadamente o raciocínio reflexivo em Cadeia de Pensamento (CoT) e o aumento de passagens de amostragem. No entanto, ambas introduzem uma sobrecarga computacional significativa para inferência. Além disso, as análises de custo existentes geralmente regulam apenas o número de passagens de amostragem, enquanto negligenciam as disparidades substanciais nos custos de amostragem introduzidas por diferentes estratégias de escalonamento. Neste artigo, comparamos sistematicamente a eficiência de diferentes estratégias de escalonamento em tempo de teste para modelos de ATP e demonstramos a ineficiência das abordagens de código aberto atuais de última geração (SOTA). Em seguida, investigamos abordagens para reduzir significativamente o uso de tokens e as passagens de amostragem, mantendo o desempenho original. Especificamente, propomos dois métodos complementares que podem ser integrados em um pipeline unificado de EconRL para benefícios amplificados: (1) um mecanismo de alternância dinâmica de Cadeia de Pensamento (CoT) projetado para mitigar o consumo desnecessário de tokens, e (2) Aprendizado por Reforço (RL) paralelo e escalonado com prefixos treináveis para aumentar as taxas de aprovação sob passagens de amostragem restritas. Experimentos no miniF2F e no ProofNet demonstram que nosso EconProver alcança desempenho comparável aos métodos de linha de base com apenas 12% do custo computacional. Este trabalho fornece insights acionáveis para a implantação de modelos leves de ATP sem sacrificar o desempenho.

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.