GPT自动证明数学题，结果被专业数据库收录，数学家点赞

机器之心报道

参与：魔王、小舟、杜伟

继 GPT-3 之后，OpenAI 推出用于数学问题的 GPT-f，利用基于 Transformer 语言模型的生成能力进行自动定理证明。由 GPT-f 发现的 23 个简短证明已被 Metamath 主库接收。

大名鼎鼎的 Transformer 架构不仅在 NLP 领域呼风唤雨，还能用于计算机视觉，比如目标检测。但仅仅这样就足够了吗？最近，OpenAI 研究者尝试用基于 Transformer 的语言模型做自动定理证明（ATP）！

论文一作 Stanislas Polu、二作 Ilya Sutskever 在 Twitter 上介绍该研究。

自动定理证明是人工智能研究领域中的一个非常重要的课题，其任务是使用电子计算机程序对数学中提出的定理或猜想寻找一种证明或反证的方法。

与人类相比，自动定理证明的主要局限在于原始数学项（term）的生成，而语言模型恰好具备生成能力。基于此，OpenAI 展开了一项研究。

这项研究使用基于 Transformer 的语言模型，为 Metamath 形式化语言提供了自动证明器和证明助理（proof assistant）GPT-f。GPT-f 能够发现新的简短证明，这些证明已被 Metamath 主库接收。研究者称这是深度学习系统提供的证明首次被形式数学社区采纳。

自动证明器

研究人员向 Metamath 库贡献了 23 个简短证明，这些证明均由 GPT-f 自动证明器生成。

为了发现更短的证明，研究人员从 Metamath 的 set.mm 库中采样命题证明，并对比 GPT-f 模型找出的解与真值的长度，同时还验证了简短证明不依赖于额外的公理。

GPT-f 证明助理

研究人员创建了一个在线证明助理，允许在 GPT-f 模型的帮助下进行交互式定理证明。下图展示了 GPT-f 证明助理的界面：

研究人员使用它对 200 多个定理和练习进行形式化。他们发现，GPT-f 模型尤其适用于生成大部分 Metamath 证明所需的多种低级证明步骤，还能通过将现有定理调整为用户需要的格式进行 Metamath 库搜索并提示待用定理。即使犯错后，模型通常仍能找到正确的定理。

OpenAI 研究人员计划将 GPT-f 扩展到其他形式系统。

在大致了解 OpenAI 这项新研究之后，我们来看这个延续了 GPT 系列之名的方法到底是如何诞生的。

为什么用自动定理证明？

神经网络在过去十年中成绩卓著，在计算机视觉、翻译、语音识别、图像生成、游戏以及机器人领域均取得很大进展。尤其是，近来神经网络的语言理解和生成能力发展迅速。

但是，除了 AlphaGo 和 AlphaZero 具有一定的推理能力，其他研究领域在推理能力上尚不完善。该研究通过将 Transformer 语言模型应用于自动定理证明，缓解了这一现象。

为什么使用自动定理证明呢？

自动定理证明适合探索常规的推理，尤其是语言模型的推理能力，原因如下：

推理方式更广泛：定理证明可能需要通用和灵活推理，因此定理证明的进步也让推理有了更广泛的发展。
搜索：自动定理证明系统可以快速检查证明的正确性，因而成为搜索方法应用与发展的生产级环境。
自动化数据生成：验证证明的能力使自动生成新问题成为可能，并且这些新问题可以用作训练数据。这就在一定程度上缓解了推理任务中收集高质量数据的难题。

学习定理证明在某种程度上类似于学习下围棋（围棋是一个小型的形式系统）：二者都提供了一种自主确定成功的方式，并且都能够通过自我对弈来自动生成新数据。这种相似性以及 AlphaZero 的成功表明，自动定理证明可能会成为神经网络推理研究中富有研究成果的领域，将来可能取得重大进展。

研究贡献

该研究验证了生成式预训练能够大幅提升模型性能，基于数学数据（如 arXiv）的预训练性能超过基于网页通用文本的预训练性能；
研究发现模型大小与性能存在正相关关系，即使在 Metamath 数据集相对较小的情况下；
基于该研究提出的语言模型所生成的命题，迭代式地训练值函数可提升证明器性能，这直接带来了连续自我改进（continuous self improvement）策略：基于证明器生成的证明不断训练；
该研究的最优模型在 Metamath 环境中实现了新的 SOTA 结果，这表明 Transformer 架构可能适用于形式推理。

形式环境

该研究采用 Metamath 作为形式环境。Metamath 的主库叫做 set.mm，包含基于 ZFC 集合论的约 38000 个证明。

数据集

Metamath set.mm 使用二进制压缩格式来表示命题的证明。研究者对该库进行了处理，提取了证明步骤数据集，并将其存储为 JSON Blob。对于每个证明步骤，研究者存储了 GOAL、PROOFSTEP 和对父目标的引用（如果有的话），将定理证明的树结构编码为：

该研究所用数据集包含约 300 万个此类证明步骤（约 38000 个定理）。

术语

自动定理证明领域的相关术语参见下图：

模型

架构

研究者使用了类似 GPT-2 和 GPT-3 的纯解码器（decoder-only）Transformer。最大的模型有 36 层、7.74 亿个可训练参数。

训练目标

训练所用的证明步骤（proofstep）目标是一个能够为给定目标（GOAL）生成 PROOFSTEP 的条件语言建模目标。为此，研究者制定了如下数据格式：

数据集中每个 JSON 行都有一个这样的目标。研究者在每段上下文（不分块）中仅训练一个句子，并通过设置损失权重 w_loss = 0 来遮蔽上下文的其余内容。在训练中，研究者在遮蔽目标 query 部分的同时，跟踪验证损失和序列准确率：

研究者在验证损失最低点使用早停法（early-stopping），并将权重衰减设置为 wd = 0.1，来正则化训练。

如下是用于模型训练的一段随机采样上下文：

证明搜索

研究者通过运行证明搜索来查找证明。如下图 1 所示，证明搜索维护了证明树（proof tree）和按照累积对数概率（logprob）排序的开放目标（open goal）队列，并用 root goal 进行了初始化：

预训练

研究者探究了预训练对模型性能的影响。具体来讲，研究者在 GPT-3 的 CommonCrawl 后处理版本以及混合了 GitHub、arXiv 和 Math StackExchange 数据的 WebMath 数据集（更加注重推理）上进行模型训练。WebMath 数据集的数据情况如下表 1 所示：

合成数据集

尽管 Metamath 是最大的形式数学库之一，但它应用于深度学习时规模仍显不足。set.mm 主要集中于著名的高级定理，不包括大量类似于数学练习的引理。而且，Metamath 缺乏高级策略（tactic），例如 HOL Light 定理证明器的 ARITH_RULE、Lean 证明器的 ring，而确保该模型能够证明其他系统的高级策略可以处理的基本定理是非常重要的，这些系统涉及运算、环等式和环不等式等领域。

基于此，研究者设计了合成数据集，允许该模型为这些领域中的任意一个生成证明，并通过调整训练集中证明的增加数量使控制更加精准。

n 位运算

下表 2 展示了当数位为 3、9 和 18 时，合成生成器（synthetic generator）生成的证明步骤平均数：

环代数（Ring Algebra）

该研究开发的环等式生成器主要受 INT 不等式生成器 [45] 的启发。下表 3 为该研究提出的环代数合成生成器所使用的 Metamath 定理：

默认增强数据集

下表 4 为构建增强数据集所附加的证明和证明步骤数目：

值函数

为了实现更好的性能，研究者还迭代地训练值函数来指导证明搜索，从而代替上文中的累积对数概率优先级。

为了获得值函数，研究者只需要训练模型，来预测证明搜索过程中产生的目标能否通过生成以下形式的新数据集得到解决：

实验

该研究所用的基线方法如下表 5 所示：

下表 6 展示了不同模型大小对性能的影响：

这些结果表明，模型大小与性能呈正相关，尽管训练数据集的规模有限（这里只训练了约 18 个 epoch）。

预训练

所有模型均使用 GPT-3 方法在 CommonCrawl 数据集上进行预训练（260B tokens）。在研究基于 WebMath 数据集进行预训练的效果时，同样先从基于 CommonCrawl 进行预训练开始，然后再在 WebMath 上继续预训练（16B additional tokens）。不同模型的性能如下所示：

值函数

随着在样本证明生成的数据上进行迭代训练，模型的性能如下所示：

结果

研究人员尝试将每个证明搜索的扩展数量从 d = 128 增加到 d = 256，将每个证明的尝试数量从 a = 4 增加到 a = 32。

下表展示了，模型在验证集上随每个命题尝试次数的性能变化情况：

总之，OpenAI 提出了 GPT-f 自动定理证明器和证明助理，展示了 Transformer 架构适用于形式推理，且在 Metamath 库中实现了新的 SOTA 结果。此外，该研究展示了预训练和值函数迭代训练的重要性。实验结果表明，将深度学习系统与形式系统紧密结合，将为未来研究提供有趣的方向，其目标是更好地利用深度学习系统的生成能力和形式系统的验证能力。

社区评价

在论文中，研究者指出 Metamath 社区给出了较为积极的反馈，证明的长度是该社区关心的重要指标：