EconProver: Hacia un Escalado más Económico en Tiempo de Prueba para la Demostración 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

Resumen

Los Modelos de Lenguaje de Gran Escala (LLMs, por sus siglas en inglés) han avanzado recientemente el campo de la Demostración Automática de Teoremas (ATP, por sus siglas en inglés), logrando mejoras sustanciales en el rendimiento mediante estrategias de escalado ampliamente adoptadas durante la fase de prueba, destacándose el razonamiento reflexivo de Cadena de Pensamiento (CoT, por sus siglas en inglés) y el aumento de pasadas de muestreo. Sin embargo, ambas estrategias introducen una sobrecarga computacional significativa durante la inferencia. Además, los análisis de costos existentes suelen regular únicamente el número de pasadas de muestreo, pasando por alto las disparidades sustanciales en los costos de muestreo introducidos por diferentes estrategias de escalado. En este artículo, comparamos sistemáticamente la eficiencia de diversas estrategias de escalado durante la prueba para modelos de ATP y demostramos la ineficiencia de los enfoques de código abierto más avanzados (SOTA, por sus siglas en inglés) actuales. Luego, investigamos enfoques para reducir significativamente el uso de tokens y las pasadas de muestreo mientras mantenemos el rendimiento original. Específicamente, proponemos dos métodos complementarios que pueden integrarse en una canalización unificada de EconRL para obtener beneficios amplificados: (1) un mecanismo de conmutación dinámica de Cadena de Pensamiento (CoT) diseñado para mitigar el consumo innecesario de tokens, y (2) Aprendizaje por Refuerzo (RL, por sus siglas en inglés) paralelo-escalado diverso con prefijos entrenables para mejorar las tasas de aprobación bajo pasadas de muestreo restringidas. Los experimentos en miniF2F y ProofNet demuestran que nuestro EconProver alcanza un rendimiento comparable a los métodos de referencia con solo el 12% del costo computacional. Este trabajo proporciona ideas prácticas para implementar modelos de ATP livianos sin sacrificar el rendimiento.

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.