GAR: Generatives Adversarielles Verstärkungslernen für Formales Theorembeweisen

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

Das Lösen mathematischer Probleme durch verifizierbare Sprachen wie Lean hat sowohl die Mathematik- als auch die Informatikgemeinschaft erheblich beeinflusst. Aktuelle State-of-the-Art-Modelle werden oft mit kostspieligem Online-Reinforcement-Learning (RL) oder Experteniteration trainiert. Diese Ansätze stützen sich jedoch auf feste Problemsätze, was zu ineffizientem Training führt und die Fähigkeit des Modells einschränkt, komplexe Probleme zu bewältigen. Um diese Einschränkungen zu überwinden, schlagen wir GAR vor: Generative Adversarial Reinforcement Learning, ein umfassendes RL-Trainingsframework, das den Problemkomponisten und den Löser gemeinsam in einer adversarischen Schleife trainiert. GAR führt einen impliziten Mechanismus für Curriculum-Learning ein, der die Schwierigkeit der Aufgaben mit der sich entwickelnden Fähigkeit des Beweisers abstimmt. Dadurch wird die Trainingseffizienz verbessert und die Leistung bei der Bewältigung fortgeschrittener Theoreme gesteigert. Experimente zeigen, dass mit GAR-Training Goedel-Prover-V2-8B und DeepSeek-Prover-V2-7B eine durchschnittliche relative Verbesserung in pass@32 von 4,20 % auf dem MiniF2F-Test-Benchmark erreichen, während der pass@32-Wert von DeepSeek-Prover-V2 auf ProofNet-Test von 22,58 % auf 25,81 % steigt. Über die formale Beweisführung hinaus etabliert GAR ein allgemeines RL-Paradigma für die Ko-Evolution von Problemgenerierung und -lösung in verifizierbaren Umgebungen.

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.