GAR : Apprentissage par Renforcement Génératif Adversarial pour la Preuve de Théorèmes Formels

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

October 13, 2025

papers.authors: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang

cs.AI

papers.abstract

La résolution de problèmes mathématiques grâce à des langages vérifiables tels que Lean a eu un impact significatif sur les communautés des mathématiques et de l'informatique. Les modèles actuels de pointe sont souvent entraînés à l'aide d'un apprentissage par renforcement (RL) en ligne coûteux ou d'une itération experte. Cependant, ces approches reposent sur des ensembles de problèmes fixes, ce qui entraîne un entraînement inefficace et limite la capacité du modèle à aborder des problèmes complexes. Pour surmonter ces limitations, nous proposons GAR : Generative Adversarial Reinforcement learning, un cadre d'entraînement RL complet qui forme conjointement le compositeur de problèmes et le solveur dans une boucle antagoniste. GAR introduit un mécanisme implicite d'apprentissage curriculaire, qui aligne la difficulté des tâches avec l'évolution des capacités du prouveur. Cela améliore ainsi l'efficacité de l'entraînement et permet une meilleure performance dans la démonstration de théorèmes avancés. Les expériences montrent qu'avec l'entraînement GAR, Goedel-Prover-V2-8B et DeepSeek-Prover-V2-7B obtiennent une amélioration relative moyenne de 4,20 % en pass@32 sur le benchmark MiniF2F-Test, tandis que le pass@32 de DeepSeek-Prover-V2 sur ProofNet-Test passe de 22,58 % à 25,81 %. Au-delà de la démonstration formelle, GAR établit un paradigme RL général pour la co-évolution de la génération et de la résolution de problèmes dans des environnements vérifiables.

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.