GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
This is the official model for GAR: Generative Adversarial Reinforcement Learning, a framework that jointly trains a problem composer and solver in an adversarial loop for formal theorem proving.
We introduce GAR: Generative Adversarial Reinforcement Learning, an RL training method that intends to solve inefficiency and suboptimial performance in formal theorem prover training caused by fixed problem sets. GAR jointly trains the problem composer and solver in an adversarial loop, which introduces an implicit curriculum learning mechanism, aligning the task difficulty with the prover's evolving capability to improve training efficiency and enabling stronger model performance.
Experiments indicates that GAR trained models (such as Goedel-Prover-V2-8B and DeepSeek-Prover-V2-7B) achieve an average of 4.20% of enhancement on MiniF2F-Test under pass@32, and improve the DeepSeek-Prover-V2's pass@32 performance on ProofNet-Test from 22.58% to 25.81%.
1@article{wang2025gar,
2 title={GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving},
3 author={Wang, Ruida and Yao, Jiarui and Pan, Rui and Diao, Shizhe and Zhang, Tong},
4 journal={arXiv preprint arXiv:2510.11769},
5 year={2025}
6}
Acknowledgement
This material is based upon work supported partially by NSF under Grant No. 2416897, Grant No. 2505932, and by ORN under Grant No. N000142512318. This research used both Delta (NSF award OAC 2005572) and DeltaAI (NSF award OAC 2320345) advanced computing systems, and computing resources provided by NAIRR Pilot NAIRR250157.
