用于自动定理证明的生成语言建模

# 生成式语言模型在自动定理证明中的应用 来源：https://openai.com/index/generative-language-modeling-for-automated-theorem-proving/ OpenAI ## 摘要 我们探索了基于 transformer 的语言模型在自动定理证明中的应用。这项工作的动力来自于一种可能性：自动定理证明器相比人类的一个主要限制——生成原创数学项——可能可以通过语言模型的生成来解决。我们为 Metamath 形式化语言呈现了一个自动证明器和证明助手 GPT-f，并分析了其性能。GPT-f 发现的新的简短证明被接纳进了主要的 Metamath 库，据我们所知，这是深度学习系统首次为形式化数学社区贡献了被采纳的证明。