Generative Language Modeling for Automated Theorem Proving
Stanislas Polu OpenAI、Ilya Sutskever OpenAI
Abstract
We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans – the generation of original mathematical terms – might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep learning based system has contributed proofs that were adopted by a formal mathematics community.
中文速览
用变换器语言模型（Transformer-based language model）来做自动定理证明，一直面临一个核心难题：机器很难像人类一样"凭空生成"数学推导中需要的中间项。研究团队将GPT系列模型应用于Metamath形式化语言，构建了一套名为GPT-f的自动证明系统，通过让模型在给定当前证明目标的情况下直接生成下一步证明动作，再配合累积对数概率引导的树搜索，来寻找完整证明。实验表明，在数学文本（如arXiv论文）上预训练、迭代生成新训练数据并训练价值函数，都能持续提升性能，最终模型在测试集上的证明成功率达到56.22%，远超此前最优方法的21.16%。更重要的是，GPT-f发现的若干简短新证明被Metamath官方库正式收录，这是深度学习系统的证明成果首次被形式数学社区采纳，标志着神经网络在严格数学推理领域迈出了实质性的一步。
原文 arXiv:2009.03393;中英对照 + 大白话阅读 https://aha.fim.ai/paper/2009.03393v1