主要证据
- DeepMath - Deep Sequence Models for Premise SelectionS1 · 主要研究来源 · 论文 · 2016-06-14
- DeepMath - Deep Sequence Models for Premise Selection — NIPS 2016S1 · 主要研究来源 · 论文
- TensorFlow Deepmath premise-selection implementationS1 · 主要研究来源 · 代码仓库
DeepMath 将深度序列模型引入大规模前提选择
DeepMath 使用循环与卷积神经架构编码猜想和候选前提，并学习判断某个前提是否有助于目标定理。该工作把大型形式证明语料转化为神经相关性模型的训练数据，使表示学习成为自动定理证明流程中的核心组件之一。
发生了什么？
Alexander A. Alemi、François Chollet、Niklas Eén、Geoffrey Irving、Christian Szegedy 与 Josef Urban 训练神经序列模型，为 Mizar 猜想排序候选前提。论文报告其两阶段架构在大规模前提选择上取得有竞争力的结果，同时避免了此前先进系统所依赖的人工设计特征。
为什么重要？
当自动证明器面对大型数学库时，前提选择是关键瓶颈之一。DeepMath 展示了神经模型能够在这一规模上学习有效的相关性信号，为从早期特征工程式学习走向后来的神经证明搜索引导、图表示与形式数学学习式检索系统提供了方法桥梁。
重要性说明：DeepMath 是较早把深度神经序列模型大规模应用于形式数学前提选择的重要工作。它直接从 Mizar 定理与证明语料中学习，而不再主要依赖此前系统中的人工特征工程，为大型理论定理证明建立了深度学习表示与排序的具体路线，并直接早于后来把神经引导接入证明器内部搜索的工作。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 实质性支持
- 形式保障
- 有形式化工件
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 神经模型为目标猜想排序候选形式前提，为后续自动定理证明提供学习式引导，而不是独立构造完整证明。
- 人类贡献
- 研究者设计前提选择任务、神经序列架构、训练语料构建、评测协议以及与大型理论自动定理证明流程的集成方式。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 有形式化工件
- 最后审阅
- 2026-09-15
技术细节
- 系统
- deepmath, mizar
- 机构
- google-research, czech-technical-university
- 数学问题
- premise-selection, automated-theorem-proving, mizar-theorem-proving
- 方法
- neural-premise-selection, sequence-modeling, convolutional-neural-network, recurrent-neural-network, representation-learning
全部来源与工件
- DeepMath - Deep Sequence Models for Premise SelectionS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- DeepMath - Deep Sequence Models for Premise Selection — NIPS 2016S1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- TensorFlow Deepmath premise-selection implementationS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-15
验证历史
- 2016-06-14 · 论文已发布 · E2 · 研究记录
arXiv 与 NeurIPS 研究记录确认了 DeepMath 的前提选择方法及论文报告的 Mizar 评测。这一记录确认公开研究主张，并不表示论文报告的指标已获得独立复现。
- 2026-09-15 · 论文已发布 · E3 · 可检查工件
TensorFlow 公开 Deepmath 仓库保留 `deepmath/premises` 前提选择实现及相关神经模型。E3 表示存在可直接检查的研究代码，而非论文 benchmark 结果已获独立复现。
更正
当前没有记录的更正。