用强化学习实现“氛围证明”：从零构建可验证推理的AI训练流程

“众所周知，数学向更高精度的发展导致了其大部分领域的公理化，因此人们可以仅用几条机械规则来证明任何定理。” —— 库尔特·哥德尔

在系列文章的第一部分中，构建了一个证明检查器，并阐述了为何可以信任大型语言模型生成的证明：只要拥有形式化的推理规则和一个可靠的验证器，所需的就只是“几条机械规则”。那么，如何训练一个大型语言模型来生成有效的证明呢？

正如DeepSeek精彩展示的那样，AI学习围棋游戏背后的直觉同样适用于AI学习如何推理，前提是推理过程可以被检查（而我们现在知道这是可行的）。在这第二部分中，将充分利用之前构建的验证器，搭建一个端到端的强化学习训练循环，对一个开源模型进行微调，使其能够用第一部分介绍的语言生成证明。下图概览了该流程的基本组成部分。

从使用Sonnet生成数据集到在Tinker上运行强化学习循环的完整实现。[ 作者供图 ]

简而言之：首先通过人机协作生成一个数据集（利用证明检查器对LLM生成的示例进行初步校验），然后在Tinker平台上运行一个强化学习循环，对开源模型进行LoRA风格的微调。提供给模型的提示包括：(1) 自定义推理语言的工作原理，(2) 如何应用规则构建证明，(3) 如何格式化答案以便解析。每个生成的证明都会经过证明检查器的检验，奖励信号会回传以提升模型的能力。理想情况下，模型最初会生成大量失败的证明尝试，但随着训练进行，其表现会逐步改善。

需要指出的是，虽然本系列文章主要关注数学推理，但可验证的证明对于在分布式软件系统中建立信任至关重要。正如一些专家所论证的，AI很可能正是大规模证明软件正确性所缺失的关键要素！

准备好，克隆项目仓库，并开始动手实践。如果错过了第一部分，可以在此阅读。

数据集生成

“人们认为数学很复杂。数学是简单的部分。它是我们能理解的东西。猫才是复杂的。” —— 约翰·康威

为了获得改进模型所需的奖励信号，首先需要证明示例。理想情况下，希望获得一个混合了简单和困难证明的数据集，并且这些证明都是用自定义的推理语言书写的。不能仅仅生成随机字符串，因为需要模型尝试证明那些已知可被证明的命题。那么，如何启动这个过程呢？

训练数据集由三个来源组合而成：

• 手动翻译自forallx教材的习题（前提 -> 结论），这些习题被认为是可解的；
• 手动翻译自《语言、证明与逻辑》教材的习题（前提 -> 结论），这些习题也被认为是可解的；
• 由强大LLM（Anthropic的Sonnet）生成的证明语料。由于不能假设LLM生成的前提->结论元组是正确的，因此会提示LLM生成完整的证明，该证明（正如所料！）在加入训练集前会经过证明检查器的校验。

数据集中的单个样本如下所示：

{"premises": ["P", "Q"], "conclusion": "P and Q", "num_steps": 1}

即，一组前提、一个结论以及Sonnet生成有效证明所需的步骤数。前提和结论将在强化学习过程中被放入提示词（因为会要求模型寻找从前提推导出结论的证明），而num_steps则是一个方便的值，用于输出关于训练集感知难度的一些统计数据（此处简化假设证明长度与其难度粗略相关）。

在Tinker上进行强化学习

“获得好主意的最佳方法就是拥有很多主意。” —— 通常归功于莱纳斯·鲍林

现在，可以开始为“氛围证明”训练自己的、规模较小的开源大型语言模型了。虽然网上有许多执行开源模型强化学习的方案和服务，但选择了Tinker，因为它承诺能够抽象掉基础设施和大部分所需的样板代码（它也是该领域的新成员，因此这也是一个测试它的机会！）。

训练循环本身并无太多意外之处：

1. 采样：给定提示词和一个（前提->结论）元组，要求模型生成多个证明尝试。
2. 验证：将每个尝试通过证明检查器运行。
3. 奖励：有效的证明（即可完全解析且逻辑正确的证明）获得奖励1，其他任何结果获得0（正如“要么做，要么不做”）。需要注意的是，还会检查生成的证明是否与请求的（前提->结论）一致，以避免LLM通过总是生成一个微不足道的正确证明来轻易地“欺骗”系统。
4. 更新：调整模型权重，使成功的证明更有可能出现。

遵循Tinker自身的指南，选择尝试几种不同规模的混合专家推理模型：gpt-oss-20b、gpt-oss-120b和Qwen3-30B-A3B-Instruct-2507。训练期间，日志和证明存储在training_logs文件夹中。训练结束后，可以使用（氛围编码的！）应用程序来可视化指标趋势并检查生成的证明。

使用氛围编码应用程序展示20b模型的训练指标。[ 作者截图 ]

如果使用AI助手来监控训练（这是在此项目中首次尝试），一个值得追踪的有趣数据切片是来自教科书的证明，因为它们被设计得具有挑战性。例如，以下是来自Claude Code的状态更新：

AI辅助监控，展示在教科书示例上的性能细分。[ 作者截图 ]

“氛围证明”的效果如何？

经过多次运行和对参数的一些调整，最终得到的模型总是能够证明大部分生成的示例，但在某些教科书证明上会遇到困难。检查生成的证明既具有启发性，也略带趣味性。

在成功的一面，这是一个尝试证明德摩根定律的例子，即展示如何从['not A or not B']推导出not (A and B)，方法是首先假设A and B并推导出矛盾：

1. not A or not B (前提)
2. | A and B (子证明)
3. | A (2)
4. | B (2)
5. || not A (嵌套子证明，来自1)
6. || ~ (3,5)
7. || not B (嵌套子证明)
8. || ~ (4,7)
9. | (1, 5-6, 7-8)
10. QED

在失败的一面，没有模型成功地从'A or B', 'not A or C', 'not B or D'证明出C or D，它们难以妥善管理嵌套子证明并应用爆炸原理，如下面这个追踪所示：

1. A or B (前提)
2. not A or C (前提)
3. not B or D (前提)
4. | A (子证明)
5. || not A (嵌套子证明)
6. || ~ (4,5)
7. | C (5-6) ← 错误
8. ….

Tinker的易用性如何？

这个小规模的概念验证很难成为对规模化训练服务的压力测试，但足以获得对该系统的一些具体印象。

良好的公开示例、对Claude友好的文档以及硬件抽象的结合，使得强化学习的入门过程愉快而平缓，且成本合理（博客文章涉及的所有实验花费大约60美元，包括那些事后看来显然是浪费时间和金钱的初步运行！）。

当熟悉流程并开始并行运行多个任务时，监控和可观测性的缺乏就成了问题：有时运行速度会显著减慢（长时间收到try_again响应，仿佛系统过载），有些任务会因不明原因在某个时刻失败（不过，当然可以从之前的检查点重新启动）。考虑到合理的价格和工作负载的原型性质，这些问题都没有超过其优点，最终对Tinker的体验足够积极，未来项目肯定会再次使用它。

结语：强化学习的探索者们

“我们做这些事不是因为它容易，而是因为我们以为它容易。” —— 佚名

虽然Tinker确实使训练过程（大部分）无缝衔接，但魔鬼仍藏在（强化学习的）细节中：目前仅仅触及了表面，因为目标是从零构建一个“氛围证明”技术栈，而非优化强化学习本身。

好消息是，整个流程是高度模块化的，因此所有组件都可以（某种程度上）独立地进行改进和调整：

• 模型选择：模型类型、模型大小、提供商……
• 训练参数：选择学习率、批次大小、LoRA秩……
• 代码抽象：使用RL Envs重写代码……
• 提示优化：更好的指令、更简单的格式、有用的上下文示例……
• 数据集优化：更多样化的示例、课程学习（不仅仅是改变证明难度，例如从只缺一步的证明开始，然后是缺两步的证明，直到模型需要填充整个证明）……

同样，自定义的证明语言肯定不足以获得有趣的结果：当然可以改进它，但要达到可用的程度实际上需要惊人的工作量。因此，更好的做法是迁移到专门构建的语言，例如Lean。重要的是，既然已经理解了“证明即形式化推理”的心智模型，同样的模型可以迁移到一个（表达能力）强大得多的语言上。此外，Lean在书写证明时具有几乎相同的风格，即引入和消除逻辑算子的规则。

换句话说，一旦掌握了“氛围证明”背后的数学原理并构建了初始的强化学习框架，剩下的就是传统的工程实践了。

致谢

感谢Patrick John Chia, Federico Bianchi, Ethan Rosenthal, Ryan Vilim, Davis Treybig对本文草稿先前版本提供的宝贵反馈。

如果对生成式AI、分布式系统推理和验证的交叉领域感兴趣，也可以查阅Bauplan的研究工作。