GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

📄 arXiv: 2510.11769v1 📥 PDF

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

分类: cs.LG, cs.AI

发布日期: 2025-10-13

💡 一句话要点

提出GAR：生成对抗强化学习框架，用于形式化定理证明，提升训练效率和性能。

🎯 匹配领域: 支柱二：RL算法与架构 (RL & Architecture)

关键词: 形式化定理证明 强化学习 生成对抗网络 课程学习 定理证明器

📋 核心要点

  1. 现有形式化定理证明模型依赖固定问题集，导致训练效率低，难以处理复杂问题。
  2. GAR框架通过对抗训练问题生成器和求解器，实现隐式课程学习，匹配任务难度和求解能力。
  3. 实验表明，GAR显著提升了模型在MiniF2F-Test和ProofNet-Test上的性能，验证了其有效性。

📝 摘要（中文）

本文提出了一种生成对抗强化学习（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还为可验证环境下问题生成和求解的协同进化建立了一个通用的强化学习范式。

🔬 方法详解

问题定义：论文旨在解决形式化定理证明中，现有强化学习方法依赖固定问题集，导致训练效率低下，且难以处理复杂定理证明的问题。现有方法的痛点在于无法根据证明器的能力动态调整训练难度，导致训练过程效率不高。

核心思路：论文的核心思路是采用生成对抗网络（GAN）的思想，构建一个问题生成器和一个定理证明器，通过对抗训练的方式，让问题生成器不断生成适合当前证明器能力水平的难题，从而实现隐式的课程学习。这样可以更有效地训练证明器，使其能够处理更复杂的定理。

技术框架：GAR框架包含两个主要模块：问题生成器（Problem Composer）和定理证明器（Theorem Prover）。问题生成器负责生成新的定理证明问题，而定理证明器则负责尝试证明这些问题。这两个模块在一个对抗循环中进行训练：问题生成器试图生成证明器难以解决的问题，而证明器则努力解决这些问题。通过这种对抗过程，问题生成器不断提高问题的难度，而证明器则不断提高自身的证明能力。

关键创新：GAR最重要的技术创新点在于将生成对抗网络与强化学习相结合，用于形式化定理证明。与传统的强化学习方法相比，GAR能够动态地调整训练问题的难度，从而更有效地训练证明器。此外，GAR还引入了一种隐式的课程学习机制，使得训练过程更加高效。

关键设计：问题生成器和定理证明器可以使用不同的神经网络结构。论文中使用了Transformer架构。损失函数方面，定理证明器使用标准的强化学习损失函数，例如策略梯度损失函数。问题生成器的损失函数则旨在生成证明器难以解决的问题，例如可以使用对抗损失函数。具体的参数设置需要根据具体的任务和数据集进行调整。

🖼️ 关键图片

fig_0

📊 实验亮点

实验结果表明，使用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能够有效提升模型处理复杂定理证明问题的能力。

🎯 应用场景

GAR框架不仅适用于形式化定理证明，还可以应用于其他需要智能体在复杂环境中进行学习和决策的领域，例如游戏AI、机器人控制和自动驾驶。通过生成具有挑战性的训练环境，GAR可以帮助智能体更快地学习到有效的策略，从而提高其在实际应用中的性能。

📄 摘要（原文）

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.