主要证据
- Generative language modeling for automated theorem provingS2 · 官方机构来源 · 官方公告 · 2020-09-07
- Generative Language Modeling for Automated Theorem ProvingS1 · 主要研究来源 · 论文 · 2020-09-07
GPT-f 将生成式语言模型引入形式定理证明
OpenAI 研究者 Stanislas Polu 与 Ilya Sutskever 在形式数学文本上训练生成模型，并将其整合进 Metamath 的证明搜索。该工作把定理证明表述为序列生成任务，并展示了学习式生成模型可以向既有形式数学库贡献可用的证明产物。
发生了什么？
GPT-f 使用生成式 Transformer 模型在 Metamath 中搜索证明，并找到被 Metamath 主库接收的新短证明。
为什么重要？
这一结果可视为后来“LLM + 证明助手”AI4Math 路线的重要起点：语言模型提出证明动作，形式系统提供精确反馈。
重要性说明：GPT-f 是较早展示 Transformer 语言模型能够直接生成形式证明步骤、而非仅进行评分或分类的系统之一；作者还报告其找到的新短证明被 Metamath 主库接收。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 新证明
- 接口
- 形式化, 符号
- AI 贡献
- 模型生成候选证明步骤并执行证明搜索；所得证明在被接收前由 Metamath 进行机械检查。
- 人类贡献
- 研究者设计模型与搜索流程、选择形式语料和评测方式；Metamath 社区维护目标证明库并审核贡献。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- gpt-f, metamath
- 机构
- openai, metamath-community
- 数学问题
- —
- 方法
- transformer-language-modeling, formal-theorem-proving, proof-search
全部来源与工件
- Generative language modeling for automated theorem provingS2 · 官方机构来源 · 官方公告 · 访问于 2026-09-10
- Generative Language Modeling for Automated Theorem ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
验证历史
- 2020-09-07 · 论文已发布 · E2 · 研究记录
OpenAI 与 arXiv 论文报告了该 Metamath 证明器，以及生成的更短证明被主库接收的情况。
更正
当前没有记录的更正。