用对抗式强化学习自动生成难题，让证明模型越练越强。
GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving
- 让题目生成器和解题器互相对抗，动态调整难度。
- 在迷你数学测试集上，解题准确率提升4.20%。
- 适合研究自动推理与智能教育系统的开发者。
通过可验证语言（如 Lean）解决数学问题已对数学和计算机科学领域产生深远影响。当前最先进的模型通常依赖昂贵的在线强化学习或专家迭代训练，但这些方法受限于固定题库，导致训练效率低且难以应对复杂问题。为此，我们提出 **GAR**：生成对抗强化学习，一种联合训练题目生成器与求解器的对抗式强化学习框架。GAR 引入隐式课程学习机制，使任务难度随求解能力动态匹配，显著提升训练效率并增强证明高阶定理的能力。实验表明，在 **GAR** 训练下，Goedel-Prover-V2-8B 和 DeepSeek-Prover-V2-7B 在 MiniF2F-Test 基准上的 pass@32 平均相对提升 4.20%；DeepSeek-Prover-V2 在 ProofNet-Test 上的 pass@32 从 22.58% 提升至 25.81%。GAR 不仅适用于形式化证明，更建立了一个在可验证环境中问题生成与求解协同演化的通用强化学习范式。论文训练代码已在 https://github.com/RickySkywalker/GAR-Official 开源。
原文摘要 · Abstract (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. The training code for this paper is open-sourced in https://github.com/RickySkywalker/GAR-Official
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。