大名鼎鼎的 Transformer 架构不仅在 NLP 领域呼风唤雨，还能用于计算机视觉，比如目标检测。但仅仅这样就足够了吗？最近，OpenAI 研究者尝试用基于 Transformer 的语言模型做自动定理证明（ATP）！自动定理证明是人工智能研究领域中的一个非常重要的课题，其任务是使用电子计算机程序对数学中提出的定理或猜想寻找一种证明或反证的方法。与人类相比，自动定理证明的主要局限在于原始数学项（term）的生成，而语言模型恰好具备生成能力。基于此，OpenAI 展开了一项研究。这项研究使用基于 Transformer 的语言模型，为 Metamath 形式化语言提供了自动证明器和证明助理（proof assistant）GPT-f。GPT-f 能够发现新的简短证明，这些证明已被 Metamath 主库接收。研究者称这是深度学习系统提供的证明首次被形式数学社区采纳。