GAR: Aprendizado por Reforço Adversarial Generativo para Prova de Teoremas Formais

GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

October 13, 2025

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

cs.AI

Resumo

A resolução de problemas matemáticos por meio de linguagens verificáveis, como o Lean, teve um impacto significativo tanto nas comunidades de matemática quanto de ciência da computação. Os modelos de última geração atuais são frequentemente treinados com Aprendizado por Reforço (RL) online de alto custo ou iteração de especialistas. No entanto, essas abordagens dependem de conjuntos de problemas fixos, o que causa treinamento ineficiente e limita a capacidade do modelo de lidar com problemas complexos. Para superar essas limitações, propomos o GAR: Aprendizado por Reforço Generativo Adversarial, um framework abrangente de treinamento de RL que treina conjuntamente o compositor de problemas e o resolvedor em um loop adversário. O GAR introduz um mecanismo implícito de aprendizado curricular, que alinha a dificuldade da tarefa com a capacidade evolutiva do provador. Isso, por sua vez, melhora a eficiência do treinamento e permite um desempenho mais forte na prova de teoremas avançados. Experimentos mostram que, com o treinamento GAR, o Goedel-Prover-V2-8B e o DeepSeek-Prover-V2-7B alcançam uma melhoria relativa média em pass@32 de 4,20% no benchmark MiniF2F-Test, enquanto o pass@32 do DeepSeek-Prover-V2 no ProofNet-Test aumenta de 22,58% para 25,81%. Além da prova formal, o GAR estabelece um paradigma geral de RL para a coevolução da geração e resolução de problemas em ambientes verificáveis.

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.