AI挑战国际数学奥林匹克竞赛，Meta神经定理注明器拿到多项SOTA

数学定理注明一直被视为建立智能机器的关键能力。注明一个特定的猜想是真是假，需要运用符号推理等数学知识，比简单的识别、分类等任务要难得多。

近日，Meta AI 建立了一个神经定理注明器 HyperTree Proof Search（HTPS），已经办理了 10 场国际数学奥林匹克竞赛 (IMO) 中的问题，比以往任何系统都更多。此外，该 AI 模型的性能比数学基准 miniF2F 上的 SOTA 格式高出 20%，比 Metamath 基准上的 SOTA 格式高出 10%。

论文地址：https://arxiv.org/pdf/2205.11491.pdf

在一定意义上，定理注明要比建立 AI 来玩国际象棋等棋盘游玩更具挑战性。当研究者试图注明一个定理时，可能移动的动作空间不仅很大而且有可能是无限的。相比较而言，在国际象棋或围棋中，这些游玩的一系列走法会被预测出来，即使算法没有给出最好的走法也影响不大。而在定理注明中，当算法走入死胡同就没办法办理了，性能再好的求解器也只是白费力气。Meta AI的新格式办理了这个棘手的问题，LeCun也转推称赞。

我们用一个例子来说明 HTPS 的优势：假设 a 和 b 都是质因子为 7 的自然数，并且 7 也是 a + b 的质因子，如果假设 7^7 可以整除(a + b)^7 – a^7 – b^7，那么请注明 a + b 至少是 19。

假如让人类来注明的话，他们大概率会用到二项式。而 HTPS 运用 Contraposition 格式，大大简化了方程，然后再检查多种不同的情况。

如下图为本文模型发现的注明示例，即在 miniF2F 中另一个 IMO 问题的注明：

更接近人类的推理

为了运用计算机编辑正式的数学注明过程，数学家最常用的格式是交互式定理注明器（ITP）。下图 1 是交互式定理注明器 Lean 中的一个注明示例：

相应的注明树如下：

给定一个要自动注明的主要目标 g，注明搜索与学习模型和定理注明情况交互以找到 g 的注明超树。注明搜索从 g 开始逐渐扩展出一个超图。当存在从根到叶子均为空集的超树时，即为注明完成。

以下图 5 注明过程为例，假设战略模型 P_θ 和批评模型 c_θ，以目标为条件，战略模型允许对战略进行抽样，而批评模型估计为该目标找到注明的能力，整个 HTPS 的注明搜索算法以这两个模型为指导。此外，与 MCTS 类似，HTPS 存储访问计数 N(g, t)（在节点 g 处选择战略 t 的次数）和每个战略 t 针对目标 g 的总动作（action）值 W(g, t)。这些统计数据将用于选择阶段。

HTPS 算法迭代地重复图 5 描述的选择、扩展、反向传播三个步骤来增长超图，直到找到注明或者超出扩展预算。

Meta 在三个定理注明情况中开发和测试 HTPS：a）Metamath，b）Lean 和 c）Metamath。Metamath 附带一个名为 set.mm 的数据库，其中包含 30k 个人类编辑的定理。Lean 附带一个由人类编辑的 27k 定理库，称为 Mathlib。最后，由于 Metamath 注明非常难以理解，因而 Meta 开发了自己的情况，称为 Equations，仅限于数学恒等式的注明。

为了模仿人类思维，神经定理注明器需要将特定形态和当前形态（对问题的理解）联系起来。Meta 首先从强化学习开始，该格式与现有的注明助手（proving assistants，例如 Lean）紧密结合。

Meta 将注明的当前形态解释为图中的一个节点，并将每一个新步骤解释为一条边。此外，研究者意识到还需要一种格式来评估注明形态的质量——类似于在棋盘游玩中 AI 需要评估游玩中的特定位置。

受蒙特卡洛树搜索 (MCTS) 启发，Meta 采用在两个任务之间进行循环：在给定注明形态下运用的合理参数的先验估计；给定一定数量的参数后的注明结果。

HTPS 是标准 MCTS 格式的变体，在该格式中，为了探索图，Meta 利用关于图的先验知识来选择一组叶进行展开，然后通过备份修正来改进初始知识。图是逐步探索的，关于图结构的知识随着迭代得到细化。

尝试

每个尝试都在单一情况（例如 Lean、Metamath 或 Equations）上运行，并将模型与 GPT-f 进行比较，它代表了 Metamath 和 Lean 的最新技术。

在 Lean 中，该研究在 A100 GPU 上运用 32 个训练器和 200 个注明器进行尝试。经过 1 天的训练（即 (200 + 32) A100 天的计算），miniF2F 中的每个形态（statement）平均被采样 250 次，在 327 个形态中已经有 110 个被办理。本文的模型在 miniF2F-test 中优于 GPT-f，具有大约 10 倍的训练时间加速。

在 Metamath 中，该研究在 V100 GPU 上训练模型，运用 128 个训练器和 256 个注明器，表 3 报告了监督模型和在线训练模型的结果。