EconProver: В направлении более экономичного масштабирования на этапе тестирования для автоматического доказательства теорем

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

September 16, 2025

Авторы: Mukai Li, Linfeng Song, Zhenwen Liang, Jiahao Xu, Shansan Gong, Qi Liu, Haitao Mi, Dong Yu

cs.AI

Аннотация

Крупные языковые модели (LLM) недавно продвинули область автоматического доказательства теорем (ATP), достигнув значительного улучшения производительности благодаря широко применяемым стратегиям масштабирования на этапе тестирования, в частности, рефлексивному рассуждению "цепочка мыслей" (CoT) и увеличению количества проходов выборки. Однако обе стратегии вносят существенные вычислительные затраты на этапе вывода. Более того, существующие анализы затрат обычно регулируют только количество проходов выборки, игнорируя значительные различия в стоимости выборки, вносимые разными стратегиями масштабирования. В данной работе мы систематически сравниваем эффективность различных стратегий масштабирования на этапе тестирования для моделей ATP и демонстрируем неэффективность современных (SOTA) подходов с открытым исходным кодом. Затем мы исследуем подходы к значительному сокращению использования токенов и количества проходов выборки при сохранении исходной производительности. В частности, мы предлагаем два взаимодополняющих метода, которые могут быть интегрированы в единый конвейер EconRL для усиления преимуществ: (1) механизм динамического переключения "цепочки мыслей" (CoT), предназначенный для снижения избыточного потребления токенов, и (2) разнообразное параллельное масштабированное обучение с подкреплением (RL) с обучаемыми префиксами для повышения успешности проходов при ограниченном количестве выборок. Эксперименты на наборах данных miniF2F и ProofNet демонстрируют, что наш подход EconProver достигает сопоставимой производительности с базовыми методами при использовании всего 12% вычислительных затрат. Эта работа предоставляет практические рекомендации для развертывания облегченных моделей ATP без ущерба для производительности.

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.