【论文标题】NaturalProofs: Mathematical Theorem Proving in Natural Language 【作者团队】Sean Welleck, Jiacheng Liu, Ronan Le Bras, Hannaneh Hajishirzi, Yejin Choi, Kyunghyun Cho 【发表时间】2021/03/24 【机 构】华盛顿大学，艾伦人工智能研究院，纽约大学 【论文链接】https://arxiv.org/pdf/2104.01112.pdf 【代码链接】https://github.com/ wellecks/naturalproofs 【推荐理由】自然语言预训练的数学领域实践

利用混合了人类使用的符号语言和自然语言的自然数学语言去了解和创造数学，是推动机器学习发展的一个具有挑战性的重要问题。作为在此方向的一小步，作者开发了NATURALPROOFS，一个用自然数学语言书写的大规模的数学语句数据集以及对应的证明。利用NATURALPROOFS，我们提出了一个数学检索任务，测试系统发掘证明中的关键结果的能力。与经典信息检索技术相比，使用语言预训练的长序列模型在这项任务中表现出色。

一个通过NATURALPROOFS证明的定理demo，所有划线部分通过reference图进行信息检索。

上图为reference图，点为陈述（定理/定义等）边为reference间链接。陈述A和定理B间边相连意味着2者相关,边可从任意陈述点出发但是永远终结于定理。在信息检索任务中数据被切分，所有的在验证/测试集中的定理均为reference图中的叶节点。上图中训练集的定理为红色，其他定理为蓝色。

借助与其他经典方法的比较实验，本文最终发现预训练语言模型时一个很好的解决数学任务的起始点。上图左侧空间为微调前TSNE隐变量空间，右侧为微调后隐变量空间，展示了预训练+微调为数学定理空间带来的聚集作用，不同数据理论都得以靠近。