给 AI 补数学课，人工智能可证明数学数据库中 82% 的问题了

图片地址：https://img.ithome.com/newsuploadfiles/2022/5/6a784286-a25e-4c06-8a60-dc552404a65a.png

不得不说，科学家们最近都在痴迷给 AI 补数学课了。这不，脸书团队也来凑热闹，提出了一种新模型，能完全自动化论证定理，并显著优于 SOTA。要知道，随着数学定理愈加复杂，之后再仅凭人力来论证定理只会变得更加困难。因此，用计算机论证数学定理已经成为一个研究焦点。此前 OpenAI 也提出过专攻这一方向的模型 GPT-f，它能论证 Metamath 中 56% 的问题。而这次提出的最新方法，能将这一数字提升到 82.6%。与此同时，研究人员表示该方法使用的时间还更短，与 GPT-f 相比可以将计算消耗缩减到原本的十分之一。难道说这一次 AI 大战数学，是要成功了？还是 Transformer本文提出的方法为一种基于 Transformer 的在线训练程序。大致可以分为三步：第一、在数学证明库中预训练；第二、在有监督数据集上微调策略模型；第三、在线训练策略模型和判断模型。具体来看是利用一种搜索算法，让模型在已有的数学证明库中学习，然后