TLDR: GAR (Generative Adversarial Reinforcement Learning) is a new AI training framework that significantly improves formal theorem proving. It works by having an AI problem composer (statement fuser) and an AI problem solver (prover) learn together in an adversarial loop. The composer generates increasingly difficult but solvable mathematical problems, while the prover continuously enhances its ability to solve them. This ‘implicit curriculum learning’ leads to more efficient training and notable performance gains on complex math benchmarks like MiniF2F-Test and ProofNet-Test, demonstrating a novel approach to AI reasoning in verifiable environments.
Formal theorem proving, a field where mathematical problems are solved using verifiable languages like Lean, is a significant area of research in both mathematics and computer science. Traditionally, state-of-the-art models in this domain often rely on expensive online Reinforcement Learning (RL) or expert iteration. However, these methods typically use fixed sets of problems, which can lead to inefficient training and limit the models’ ability to tackle truly complex mathematical challenges.
To overcome these limitations, researchers from the University of Illinois Urbana-Champaign and NVIDIA have introduced a novel framework called GAR: Generative Adversarial Reinforcement Learning. GAR is a comprehensive RL training framework that takes a unique approach: it jointly trains a problem composer and a problem solver in an adversarial loop. This means that as the solver gets better, the composer learns to create more challenging, yet solvable, problems, pushing the solver to continuously improve.
The core innovation of GAR lies in its implicit curriculum learning mechanism. Instead of relying on a static set of problems, GAR dynamically adjusts the difficulty of the tasks to match the evolving capabilities of the prover (the problem solver). This adaptive difficulty ensures that training is more efficient, as the model isn’t wasting time on problems that are too easy or impossibly hard. This approach enables the prover to achieve stronger performance in proving advanced theorems.
The GAR framework operates in two main stages during each iteration. First, in the Generation Stage, a component called the ‘statement fuser’ synthesizes new, harder mathematical statements by combining existing ones. These new statements are then converted into a formal language (like Lean) and given to the prover to attempt to solve. The proofs generated by the prover are then verified, and their correctness rate is recorded.
The second stage is the Adversarial Reinforcement Learning Stage. Here, both the prover and the statement fuser are optimized in a competitive manner. The prover is rewarded for successfully producing correct proofs on problems of medium to high difficulty. Simultaneously, the statement fuser is rewarded for generating problems that are challenging enough to push the prover’s limits but still solvable. This adversarial dynamic ensures that both components continuously evolve, with the fuser creating a progressively more difficult curriculum and the prover enhancing its reasoning abilities to keep pace.
A key technique within GAR is ‘Statement Fusion,’ which allows for the creation of novel formal statements that are better aligned with the model’s current capabilities. This is crucial because directly fusing formal statements can often lead to grammatically incorrect or unsolvable problems. By fusing natural language statements first and then formalizing them, GAR ensures the generated problems are adaptively challenging and well-formed.
The effectiveness of GAR has been demonstrated through extensive experiments. When applied to existing powerful prover models like Goedel-Prover-V2-8B and DeepSeek-Prover-V2-7B, GAR training led to significant improvements. For instance, Goedel-Prover-V2-8B achieved an average relative improvement in pass@32 of 4.20% on the MiniF2F-Test benchmark. DeepSeek-Prover-V2 also saw its pass@32 on the more challenging ProofNet-Test increase from 22.58% to 25.81%. These results highlight GAR’s ability to enhance models that already exhibit outstanding performance.
Also Read:
- Ax-Prover: Advancing Automated Theorem Proving Across Science with LLM Agents
- Adaptive Dual Reasoner: Smarter, More Efficient AI Thinking
Beyond formal theorem proving, GAR establishes a general Reinforcement Learning paradigm for the co-evolution of problem generation and solving in verifiable environments. This opens up new avenues for adversarial co-training in other domains that require intensive reasoning. For those interested in the technical details, the full research paper can be found at arXiv:2510.11769.
