GAR: Apprendimento per Rinforzo Adversarial Generativo per la Dimostrazione Formale di Teoremi

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

October 13, 2025

Autori: Ruida Wang, Jiarui Yao, Rui Pan, Shizhe Diao, Tong Zhang

cs.AI

Abstract

Risolvere problemi matematici attraverso linguaggi verificabili come Lean ha avuto un impatto significativo sia sulla comunità matematica che su quella informatica. I modelli all'avanguardia attuali sono spesso addestrati con costosi metodi di Reinforcement Learning (RL) online o iterazione esperta. Tuttavia, questi approcci si basano su insiemi di problemi fissi, il che causa un addestramento inefficiente e limita la capacità del modello di affrontare problemi complessi. Per superare queste limitazioni, proponiamo GAR: Generative Adversarial Reinforcement learning, un framework completo di addestramento RL che allena congiuntamente il compositore di problemi e il risolutore in un ciclo avversariale. GAR introduce un meccanismo implicito di curriculum learning, che allinea la difficoltà del compito con l'abilità evolutiva del dimostratore. Ciò migliora l'efficienza dell'addestramento e consente prestazioni più robuste nella dimostrazione di teoremi avanzati. Gli esperimenti mostrano che con l'addestramento GAR, Goedel-Prover-V2-8B e DeepSeek-Prover-V2-7B ottengono un miglioramento relativo medio in pass@32 del 4,20% sul benchmark MiniF2F-Test, mentre il pass@32 di DeepSeek-Prover-V2 su ProofNet-Test aumenta dal 22,58% al 25,81%. Oltre alla dimostrazione formale, GAR stabilisce un paradigma generale di RL per la co-evoluzione della generazione e risoluzione di problemi in ambienti verificabili.

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.