GAR: Generative Adversarial Reinforcement Learning for Formal Theorem Proving

该论文提出了名为 GAR 的生成对抗强化学习框架，通过让问题生成器与求解器在对抗循环中协同进化，实现了隐式课程学习，从而显著提升了 Goedel-Prover-V2 和 DeepSeek-Prover-V2 等模型在 MiniF2F 和 ProofNet 等基准测试上的形式化定理证明性能。

要点

这篇论文介绍了一种名为 GAR（生成式对抗强化学习）的新方法，旨在让 AI 更聪明地解决数学证明问题。

为了让你轻松理解，我们可以把数学证明想象成下棋，把AI 模型想象成棋手。

1. 以前的困境：死记硬背的“题海战术”

在 GAR 出现之前，训练 AI 下棋（证明数学题）通常是这样做的：

• 固定题库：研究人员准备一本固定的“习题集”（比如从简单的加减法到复杂的微积分）。
• 反复刷题：AI 就在这本固定的习题集里不停地做题、犯错、修正。
• 问题所在：
  • 太简单：如果题目太简单，AI 早就做完了，再刷就是浪费时间（就像让大学生反复做 $1+1=2$）。
  • 太难：如果题目太难，AI 完全不会做，怎么练都没用（就像让小学生直接解量子力学）。
  • 缺乏进步：这本习题集是死的，不会随着 AI 变聪明而变难。AI 的能力被锁死在了题库的难度上限上。

2. GAR 的解决方案：一个“魔鬼教练”和一个“天才学生”

GAR 的核心思想是**“对抗训练”。它不再只训练一个 AI，而是同时训练两个 AI，让它们像“出题人”和“解题人”**一样互相“打架”（对抗），从而共同进步。

我们可以用两个角色来比喻：

• 角色 A：解题者（Prover）—— 也就是“学生”

  • 它的任务是：拿到题目，写出正确的数学证明（解题）。
  • 它的目标：做对更多的题，尤其是那些有挑战性的题。

• 角色 B：出题人（Statement Fuser）—— 也就是“魔鬼教练”

  • 它的任务是：从现有的题目库里，把两道题“融合”在一起，创造出一道更难的新题。
  • 它的目标：出题要难到让学生“跳一跳才够得着”，但又不能难到让学生完全放弃（即题目必须是可解的）。

3. 它们是如何“相爱相杀”的？（训练过程）

这个过程就像是一个动态升级的训练营：

1. 融合出题：“魔鬼教练”把两道旧题（比如一道代数题和一道几何题）融合，变成一道全新的、更复杂的综合题。
2. 学生解题：“学生”尝试解这道新题。
   • 如果解对了，学生获得奖励（经验值 +1）。
   • 如果解错了，学生获得反馈，知道自己哪里不行。
3. 互相奖惩（核心机制）：
   • 如果学生做对了：说明题目对现在的学生来说太简单了。于是，“魔鬼教练”会受到惩罚（因为它没出够难度的题），它必须下次出更难一点的。
   • 如果学生完全做不出：说明题目太难了，或者题目本身有问题。于是，“魔鬼教练”也会受到惩罚（因为它出了无解的题），它下次要稍微降低一点难度。
   • 如果学生做对了，但题目很难：这是最理想的状态！“学生”和“教练”都会获得奖励。

这就形成了一个完美的“隐式课程表”（Implicit Curriculum）：
题目难度会自动随着学生的能力提升而动态调整。学生每进步一点，教练出的题就难一点。学生永远不会在简单的题上浪费时间，也永远不会因为题目太难而崩溃。

4. 为什么要用“融合”（Fusion）？

论文里有一个很巧妙的技巧叫**“语句融合”。
想象一下，如果教练只是随机找一道难题，可能这道题刚好超出了学生的能力范围，或者题目本身有逻辑漏洞。
GAR 的做法是：教练从学生已经会做**的题目里，挑出两道，把它们的关键点“缝合”在一起。

• 比喻：就像厨师把两道你爱吃的菜（比如宫保鸡丁和鱼香肉丝）融合成一道新菜（宫保鱼香鸡丝）。因为原材料是你熟悉的，所以新菜虽然味道更丰富（更难），但你依然有办法处理，不会觉得完全陌生。

5. 结果如何？

实验结果显示，这种“对抗训练”非常有效：

• 效率更高：AI 不再浪费时间在简单的题上，训练速度更快。
• 能力更强：经过 GAR 训练的 AI（比如 DeepSeek-Prover 和 Goedel-Prover），在解决高难度数学竞赛题（如 MiniF2F 和 ProofNet 基准测试）时，正确率有了显著提升。
• 通用性：这种方法不仅适用于数学，未来可能用于任何需要“出题”和“解题”配合的领域（比如写代码、设计游戏关卡等）。

总结

GAR 就像是一个拥有“自适应难度”的超级健身房。
以前的训练是让你在一个固定的重量下举铁，要么太轻没效果，要么太重举不起来。
GAR 训练则是：有一个智能教练，时刻盯着你的状态。你举得轻松，它就加重；你举不动，它就微调重量。通过这种**“出题人”和“解题人”的实时对抗与配合**，让 AI 在不知不觉中突破了能力的极限，学会了攻克以前认为不可能解决的复杂数学难题。

技术摘要

这篇论文提出了一种名为 GAR (Generative Adversarial Reinforcement Learning，生成式对抗强化学习) 的新框架，旨在解决形式化定理证明（Formal Theorem Proving）中训练效率低下和模型难以应对复杂问题的挑战。该论文已被 ICLR 2026 接收。

以下是对该论文的详细技术总结：

1. 研究背景与问题 (Problem)

• 现状： 利用可验证语言（如 Lean）解决数学问题对数学和计算机科学产生了深远影响。目前的 SOTA 模型通常依赖昂贵的在线强化学习（RL）或专家迭代（Expert Iteration）。
• 局限性：
  • 固定数据集： 现有方法通常基于固定的问题集进行训练，导致训练效率低下（大量计算浪费在简单或不可解的任务上）。
  • 缺乏自适应难度： 缺乏根据模型能力动态调整问题难度的机制，限制了模型在复杂定理证明上的进步。
  • 单一优化目标： 大多数方法仅优化“证明者（Prover）”，而忽略了“问题生成者（Problem Composer）”的协同进化。

2. 方法论 (Methodology)

GAR 框架通过对抗训练联合优化证明者（Prover）和问题生成器（Statement Fuser），建立了一个隐式的课程学习（Implicit Curriculum Learning）机制。整个训练过程分为两个阶段，并在迭代中循环：

A. 生成阶段 (Generation Stage)

1. 语句融合 (Statement Fusion)：
   • 从基础数据集中采样两个自然语言（NL）数学问题。
   • 利用训练好的“语句融合器（Statement Fuser）”将这两个问题融合，生成一个更具挑战性的新 NL 问题。
   • 关键设计： 融合在自然语言层面进行，而非直接融合形式化语言（FL）语句。这是因为通用 LLM 对 FL 理解有限，直接融合 FL 容易导致语法错误。融合后的 NL 语句再通过自动形式化器（Autoformalizer）转换为 Lean 语句。
   • 思维链优化： 使用带有 <analysis> 标记的提示词重启模型的思维过程，避免过度思考（Overthinking），提高生成质量。
2. 证明编写 (Proof Writing)：
   • 证明者模型尝试为新生成的 NL-FL 语句对生成多个候选证明（例如 16 个）。
   • 使用 Lean 验证器检查证明的正确性，计算通过率（Pass Rate）。

B. 对抗强化学习阶段 (Adversarial RL Stage)

利用 GRPO (Group Relative Policy Optimization) 算法同时更新两个模型：

1. 证明者训练 (Prover Training)：
   • 目标： 最大化在生成语句上的证明通过率。
   • 奖励机制： 仅对中等和高等难度的问题（通过率在 0 到 0.5 之间）进行奖励。如果问题太简单（通过率>0.5）或太难/不可解（通过率=0），则被过滤掉。
   • 防奖励黑客（Reward Hacking）： 引入软惩罚项，如果证明者在证明过程中修改了原始语句（Statement Modification），会降低奖励，防止模型通过简化问题来骗取奖励。
2. 语句融合器训练 (Statement Fuser Training)：
   • 目标： 生成比当前证明者能力稍难但可解的问题，从而降低证明者的通过率。
   • 奖励机制： 奖励那些能生成“困难但可解”问题的融合器。如果生成的问题太难导致无法解决（通过率=0），则不给奖励。
   • 对抗动态： 融合器试图增加难度，证明者试图提升能力，两者相互促进，形成隐式课程。

3. 关键贡献 (Key Contributions)

1. GAR 框架： 提出了一种综合性的 RL 训练框架，通过对抗训练联合优化问题生成和求解，实现了隐式课程学习，避免了在简单或不可解问题上的无效计算。
2. 语句融合技术 (Statement Fusion)： 提出了一种在自然语言层面融合多个问题以生成新挑战的方法。这种方法生成的定理比直接形式化单一问题更能匹配模型的能力边界，且比直接融合形式化语句更稳健。
3. 通用范式： 建立了一种在可验证环境中问题生成与求解协同进化的通用 RL 范式，可推广到其他推理密集型领域。

4. 实验结果 (Results)

作者在 MiniF2F-Test 和 ProofNet-Test 基准上进行了广泛实验，基线模型包括 DeepSeek-Prover-V2-7B 和 Goedel-Prover-V2-8B。

• 性能提升：
  • MiniF2F-Test: 经过 GAR 训练后，DeepSeek-Prover-V2-7B 的 Pass@32 从 70.49% 提升至 74.18%；Goedel-Prover-V2-8B 从 77.87% 提升至 80.33%。平均相对提升约为 4.20%。
  • ProofNet-Test (更难的本科级数学): DeepSeek-Prover-V2-7B 的 Pass@32 从 22.58% 提升至 25.81%。
• 消融实验 (Ablation Studies)：
  • 语句修改惩罚： 证明了软惩罚机制有效防止了模型通过简化问题（Reward Hacking）来骗取奖励。
  • 冻结融合器： 如果冻结融合器（不训练），模型性能无法提升，证明了协同进化的必要性。
  • 对比直接 RL： 在静态数据集上直接进行 GRPO 训练会导致性能下降（因为基线模型已经过大量 RL 训练），而 GAR 通过动态增加难度实现了性能提升。
• 效率： GAR 仅需 3-5 次迭代即可在已高度优化的 RL 基线模型上取得显著收益，而传统方法（如 Kimina-Prover）需要 25 次迭代仅获得约 2% 的提升，显示了 GAR 的高样本效率。

5. 意义与影响 (Significance)

• 解决训练瓶颈： 解决了传统专家迭代和在线 RL 中因固定数据集导致的训练效率低下和模型能力上限问题。
• 隐式课程学习： 通过对抗机制自动调整问题难度，使模型能够循序渐进地探索更深层的推理策略，解决更复杂的定理。
• 通用性： 该框架不仅适用于形式化定理证明，也为其他需要“生成 - 验证”闭环的推理任务（如代码生成、科学发现）提供了新的对抗协同训练范式。
• 开源： 论文计划开源训练和推理代码，推动领域发展。

总结： GAR 通过让“出题人”和“解题人”在对抗中共同进化，成功克服了固定数据集的局限，显著提升了大语言模型在形式化数学推理领域的表现，是形式化定理证明领域的一项重要进展。