GAR: Генеративно-состязательное обучение с подкреплением для формального доказательства теорем

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

October 13, 2025

Авторы: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang

cs.AI

Аннотация

Решение математических задач с использованием проверяемых языков, таких как Lean, оказало значительное влияние как на математическое, так и на компьютерное научное сообщество. Современные передовые модели часто обучаются с использованием дорогостоящего онлайн-обучения с подкреплением (Reinforcement Learning, RL) или итераций с участием экспертов. Однако эти подходы опираются на фиксированные наборы задач, что приводит к неэффективному обучению и ограничивает способность модели решать сложные проблемы. Чтобы преодолеть эти ограничения, мы предлагаем GAR: Generative Adversarial Reinforcement learning — комплексную структуру обучения с подкреплением, которая совместно обучает генератор задач и решатель в рамках состязательного цикла. GAR вводит механизм неявного обучения по учебному плану, который согласовывает сложность задач с развивающимися возможностями решателя. Это повышает эффективность обучения и позволяет достичь более высоких результатов в доказательстве сложных теорем. Эксперименты показывают, что при обучении с использованием GAR модели Goedel-Prover-V2-8B и DeepSeek-Prover-V2-7B демонстрируют среднее относительное улучшение в метрике pass@32 на 4,20% на тестовом наборе MiniF2F-Test, в то время как показатель pass@32 для DeepSeek-Prover-V2 на ProofNet-Test увеличивается с 22,58% до 25,81%. Помимо формального доказательства, GAR устанавливает общую парадигму обучения с подкреплением для совместной эволюции генерации задач и их решения в проверяемых средах.

English

Solving math problems through verifiable languages such as Lean has significantly impacted both the mathematics and computer science communities. Current state-of-the-art models are often trained with expensive online Reinforcement Learning (RL) or expert iteration. However, these approaches rely on fixed problem sets, which causes inefficient training and limits the model to tackle complex problems. To overcome these limitations, we propose GAR: Generative Adversarial Reinforcement learning, a comprehensive RL training framework that jointly trains the problem composer and solver in an adversarial loop. GAR introduces an implicit curriculum learning mechanism, which aligns task difficulty with the prover's evolving capability. It thereby improves the training efficiency and enables stronger performance of proving advanced theorems. Experiments show that with GAR training, Goedel-Prover-V2-8B and DeepSeek-Prover-V2-7B achieve an average relative improvement in pass@32 of 4.20% on MiniF2F-Test benchmark, while DeepSeek-Prover-V2's pass@32 on ProofNet-Test increases from 22.58% to 25.81%. Beyond formal proving, GAR establishes a general RL paradigm for co-evolution of problem generation and solving under verifiable environments.