GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

TL;DR

GAR introduces a comprehensive Generative Adversarial Reinforcement Learning framework for formal theorem proving by jointly training a statement fuser (problem composer) and a prover in an adversarial loop. The approach builds an implicit curriculum that scales statement difficulty with the prover’s evolving capability, yielding measurable gains on challenging benchmarks: an average relative improvement of $4.20\%$ on MiniF2F-Test and an increase from $22.58\%$ to $25.81\%$ on ProofNet-Test for DeepSeek-Prover-V2 variants. The methodology combines a Generation Stage (statement fusion, autoformalization, Lean4 verification) with an Adversarial RL stage (GRPO-based training for both fuser and prover), including a soft statement-modification penalty to deter reward hacking. Empirical results, ablations, and fuser-stud ies support the presence of an implicit curriculum and demonstrate GAR’s generality as a co-evolutionary paradigm for reasoning in verifiable environments, with potential applicability beyond formal proving.

Abstract

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.

Figures (2)

• Figure 1: GAR Training Framework: Each iteration of GAR consists two stages. (a) Generation Stage: Pairs of NL statements are sampled from the base repository and combined by the statement fuser to create more challenging problems that fit the current model's capability. Then, these statements are autoformalized and submitted to the prover to write multiple proofs. Subsequently, the proofs are checked by the Lean verifier for reward assignments. (b) Adversarial Reinforcement Learning: The prover is rewarded for producing correct proofs on medium and high-difficulty statements, while the statement fuser is rewarded for generating harder but solvable problems. This adversarial dynamic drives both models to evolve together.
• Figure 2: Prompt for the Statement Fuser to generate harder statements from existing ones and restart thinking using a new indicator in GAR generation stage