不得不说，最近科学家们都痴迷于为AI补数学课。这不，Facebook团队也来凑热闹，提出了一个新模型，可以完全自动化定理证明，并且明显优于SOTA。请注意，随着数学定理变得越来越复杂，以后仅靠人工证明定理只会变得更加困难。因此，用计算机证明数学定理成为研究热点。此前，OpenAI也提出了专门针对这个方向的模型GPT-f，可以演示Metamath中56%的问题。这次提出的最新方法可以将这个数字提高到82.6%。同时，研究人员表示，该方法耗时也更少，与GPT-f相比，计算量减少了十分之一。难道说，这场数学领域的AI大战就要胜利了吗？或者本文中Transformer提出的方法是基于Transformer的在线训练程序。大致可以分为三个步骤：首先，在数学证明库中进行预训练；第二，在监督数据集上微调策略模型；三是政策模型和判断模型的在线训练。具体来说，它是通过一种搜索算法，让模型从已有的数学证明库中学习，进而推动和证明更多的问题。其中，数学证明库分为Metamath、Lean和自研证明环境三种。简单来说，这些证明库就是将普通的数学语言转换成类似于编程语言的形式。Metamath的主要库是set.mm，其中包含大约38,000个基于ZFC集合论的证明。精益更广为人知的是微软的可以参加IMO竞赛的AI算法。精益库的目的是把同名算法教给所有的本科数学，让它学会证明这些定理。本研究的主要目标是构建一个证明器，可以自动生成一系列合适的策略来证明问题。为此，研究人员提出了一种基于MCTS的非平衡超图证明搜索算法。MCTS译为MonteCarloTreeSearch，常用于解决博弈树问题。因为AlphaGo而出名。它通过在搜索空间中随机采样来找到有前途的动作，然后根据这个动作扩展搜索树。本研究采用的思路与此类似。搜索证明过程从目标g开始，向下搜索方法，逐渐发展为超图。当一个分支下出现一个空集时，就意味着找到了一个最优证明。最后，在反向传播时，记下超树的节点值和操作总数。在这个环节中，研究人员假设了一个政策模型和一个判断模型。政策模型允许通过判断模型进行抽样，该模型评估当前政策找到证明其合理性的方法的能力。整个搜索算法都参考了以上两种模型。两个模型都是Transformer模型，权重是共享的。接下来是线上培训阶段。在此过程中，controller会发送语句进行异步HTTPS验证，并收集训练和证明数据。然后验证器将训练样本发送到分布式训练器并定期同步其模型副本。实验结果在测试环节，研究人员将HTPS与GPT-f进行了比较。后者是OpenAI之前提出的数学定理推理模型，也是基于Transformer的。结果表明，在线训练后的模型可以证明Metamath中82%的问题，远超此前GPT-f56.5%的记录。在精益库中，这个模型可以证明43%的定理，比SOTA高出38%。以下是模型证明的IMO试题。但它还不完美。比如下面这道题，就没有用最简单的方法来解题。研究人员表示，这是因为注释中存在错误。OneMoreThing使用计算机来演示数学问题，四色定理的证明是最著名的例子之一。四色定理是现代数学三大问题之一。它提出“任何只使用四种颜色的地图都可以使具有共同边界的国家涂上不同的颜色。”由于这个定理的证明需要大量的计算，所以在它被提出后的100年内没有人能够完全证明它。直到1976年，经过美国伊利诺伊大学两台计算机1200小时100亿次的判断，终于可以证明任何地图只需要4种颜色就可以标注，这也轰动了整个数学界。此外，随着数学问题变得越来越复杂，用人来检验定理是否正确也变得越来越困难。最近，AI界也逐渐将目光投向了数学问题。2020年，OpenAI推出数学定理推理模型GPT-f，可用于自动定理证明。该方法可以完成测试集中56.5%的证明，超过目前SOTA模型MetaGen-IL30%以上。同年，微软还发布了Lean，可以做IMO试题，也就是说AI可以做看不见的题。去年，OpenAI在GPT-3中加入验证器后，做数学题的效果明显好于之前的微调方式，可以达到小学生90%的水平。今年1月，麻省理工+哈佛+哥伦比亚大学+滑铁卢大学的一项联合研究表明，他们提出的模型可以做高数。简而言之，科学家们正在努力使人工智能成为一门既是艺术又是科学的偏科。
