OpenAI推出数学推理证明模型

前不久，OpenAI的研究人员发布了一篇论文，推出了一款用于自动定理证明(ATP) 的GPT-f模型。GPT-f基于Transformer语言模型，可以为Metamath形式化语言提供自动证明器和证明助手。

• 论文名称：Generative Language Modeling for Automated Theorem Proving
• 论文地址： https://arxiv.org/pdf/2009.03393.pdf

论文一作Stanislas Polu在推特上进行了介绍，他们在实验中发现，GPT-f比现有自动定理证明器还要优秀，可完成测试集中56.22%的证明，而现有的SOTA模型MetaGen-IL也只能证明21.16%的定理。

此外，GPT-f还发现了新的简短证明，已有23个简短证明被收入Metamath函式库中。这是深度学习模型的定理生成证明首次被数学家接受。

内容中包含的图片若涉及版权问题，请及时与我们联系删除