Meta AI构建了一个神经定理证明器HyperTree Proof Search（HTPS），已经解决了10场国际数学奥林匹克竞赛（IMO）中的数学问题。数学定理证明一直被视为构建智能机器的关键能力。证明一个特定的猜想是真是假，需要使用符号推理等数学知识，比简单的识别、分类等任务要难得多。
近日，Meta AI构建了一个神经定理证明器HyperTree Proof Search（HTPS），已经解决了10场国际数学奥林匹克竞赛（IMO）中的问题，比以往任何系统都更多。此外，该AI模型的性能比数学基准miniF2F上的SOTA方法高出20%，比Metamath基准上的SOTA方法高出10%。
在一定意义上，定理证明要比构建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方法，大大简化了方程，然后再检查多种不同的情况。
为了使计算机编写正式的数学证明过程，数学家最常用的方法是交互式定理证明器（ITP）。下图1是交互式定理证明器Lean中的一个证明示例。给定一个要自动证明的主要目标g，证明搜索与学习模型和定理证明环境交互以找到g的证明超树。证明搜索从g开始逐渐扩展出一个超图。当存在从根到叶子均为空集的超树时，即为证明完成。
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报告了监督模型和在线训练模型的结果。
在Equations中，该研究使用32个训练器和64个证明器进行实验，在这种环境下，模型很容易学习随机生成器的训练分布，并解决所有综合生成的问题。