GAR: Aprendizaje por Refuerzo Generativo Adversarial para la Demostración de Teoremas Formales

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

Resumen

Resolver problemas matemáticos mediante lenguajes verificables como Lean ha tenido un impacto significativo tanto en las comunidades de matemáticas como en las de ciencias de la computación. Los modelos actuales de vanguardia suelen entrenarse con costosos métodos de Aprendizaje por Refuerzo (RL, por sus siglas en inglés) en línea o iteración experta. Sin embargo, estos enfoques dependen de conjuntos de problemas fijos, lo que provoca un entrenamiento ineficiente y limita la capacidad del modelo para abordar problemas complejos. Para superar estas limitaciones, proponemos GAR: Aprendizaje por Refuerzo Generativo Adversarial, un marco de entrenamiento de RL integral que entrena conjuntamente al compositor de problemas y al resolvedor en un bucle adversarial. GAR introduce un mecanismo implícito de aprendizaje curricular, que alinea la dificultad de las tareas con la capacidad evolutiva del demostrador. Esto mejora la eficiencia del entrenamiento y permite un mejor rendimiento al demostrar teoremas avanzados. Los experimentos muestran que, con el entrenamiento de GAR, Goedel-Prover-V2-8B y DeepSeek-Prover-V2-7B logran una mejora relativa promedio en pass@32 del 4.20% en el benchmark MiniF2F-Test, mientras que el pass@32 de DeepSeek-Prover-V2 en ProofNet-Test aumenta del 22.58% al 25.81%. Más allá de la demostración formal, GAR establece un paradigma general de RL para la coevolución de la generación y resolución de problemas en entornos verificables.

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.