GAR: Generatief Adversariaal Versterkend Leren voor Formeel Theorema Bewijzen

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

October 13, 2025

Auteurs: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang

cs.AI

Samenvatting

Het oplossen van wiskundige problemen via verifieerbare talen zoals Lean heeft een aanzienlijke impact gehad op zowel de wiskundige als de informatica-gemeenschappen. State-of-the-art modellen worden vaak getraind met kostbare online Reinforcement Learning (RL) of expertiteratie. Deze benaderingen zijn echter afhankelijk van vaste problemensets, wat leidt tot inefficiënte training en beperkt het model in het aanpakken van complexe problemen. Om deze beperkingen te overwinnen, stellen we GAR voor: Generative Adversarial Reinforcement Learning, een uitgebreid RL-trainingsraamwerk dat de probleemcomponist en -oplosser gezamenlijk traint in een adversariaal proces. GAR introduceert een impliciet curriculumlerenmechanisme, dat de moeilijkheidsgraad van taken afstemt op de evoluerende capaciteit van de bewijzer. Hierdoor verbetert het de trainings efficiëntie en maakt het betere prestaties mogelijk bij het bewijzen van geavanceerde stellingen. Experimenten tonen aan dat met GAR-training Goedel-Prover-V2-8B en DeepSeek-Prover-V2-7B een gemiddelde relatieve verbetering in pass@32 van 4,20% behalen op de MiniF2F-Test benchmark, terwijl DeepSeek-Prover-V2's pass@32 op ProofNet-Test stijgt van 22,58% naar 25,81%. Naast formeel bewijzen, vestigt GAR een algemeen RL-paradigma voor de co-evolutie van probleemgeneratie en -oplossing in verifieerbare omgevingen.

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.