GAR: Generative Adversarial Reinforcement Learning for Formal Theorem
  Proving
Authors: name: Ruida Wang, name: Jiarui Yao, name: Rui Pan, name: Shizhe Diao, name: Tong Zhang

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.