主要证据
- Holophrasm: a neural Automated Theorem Prover for higher-order logicS1 · 主要研究来源 · 论文 · 2016-08-08
- Holophrasm neural Metamath prover implementationS1 · 主要研究来源 · 代码仓库
Holophrasm 构建面向 Metamath 的神经端到端定理证明器
Holophrasm 将 Metamath 陈述解析为树结构，训练用于证明步骤生成与证明状态评估的神经模型，并与候选证明树搜索结合。公开版本包含模型训练与证明搜索代码、保存的证明结果，以及通过 Metamath verifier 重放和检查生成证明的说明。
发生了什么？
Daniel Whalen 提出 Holophrasm：一个面向 Metamath 的神经自动定理证明器，使用神经网络增强的 bandit 算法探索部分证明树，并利用序列到序列模型枚举证明动作。论文报告其在 Metamath `set.mm` 留出测试定理上证明了约 14%。
为什么重要？
该项目在 Transformer 时代之前就展示了一条神经证明生成路线：学习模型主动构造形式证明步骤，而不仅仅为前提排序。其 Metamath 数据处理与证明器结构后来被包括 MetaGen 在内的工作继续使用，因此成为神经形式定理证明演化中的重要前序。
重要性说明：Holophrasm 是较早具有代表性的神经定理证明器之一，从前提评分进一步走向在 Metamath 中搜索完整形式证明树。它把学习式证明步骤生成、神经评估与 bandit 风格搜索整合到统一系统中，成为后来 Metamath 神经证明器以及 MetaGen 等合成数据系统的直接历史前序。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 自主主导
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式神经模型负责提出证明动作并评估证明状态，搜索过程组装完整形式证明；成功输出随后可由 Metamath 检查，无需人类逐步构造证明。
- 人类贡献
- 研究者设计 Metamath 解析器、神经模型、搜索算法、训练流程和评测协议，并将生成证明整理为可重放和验证的形式。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- holophrasm, metamath
- 机构
- —
- 数学问题
- metamath-theorem-proving, automated-theorem-proving
- 方法
- neural-theorem-proving, sequence-to-sequence-generation, bandit-search, proof-tree-search, proof-step-generation
全部来源与工件
- Holophrasm: a neural Automated Theorem Prover for higher-order logicS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- Holophrasm neural Metamath prover implementationS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-15
验证历史
- 2016-08-08 · 论文已发布 · E2 · 研究记录
arXiv 研究记录确认了 Holophrasm、其神经证明搜索架构以及论文报告的 Metamath 评测。machine_checked 仅指形式证明可通过 Metamath 重放检查，并不表示论文报告的整体成功率已得到独立复现。
- 2026-09-15 · 论文已发布 · E3 · 可检查工件
公开 Holophrasm 仓库提供训练与搜索代码、保存的证明输出以及明确的 Metamath 验证说明。E3 表示存在可直接检查的研究产物，而不是 Chronicle 已独立重跑完整实验。
更正
当前没有记录的更正。