AI4Math ChronicleAI4Math 大事记

深度网络被直接接入自动定理证明器的内部搜索

该系统从成功自动证明的 clause-level 轨迹中学习，并在 saturation-style proof search 中对生成的 clauses 进行排序。由于神经网络评估慢于人工设计启发式，作者采用混合引导与 two-phase search：先利用学习模型改善搜索轨迹，再由更快的传统启发式完成后续证明尝试。

发生了什么？

Sarah Loos、Geoffrey Irving、Christian Szegedy 与 Cezary Kaliszyk 使用既有 Mizar 自动证明轨迹训练深度神经网络，并将其用于引导 E prover 内部的 processed-clause selection。论文报告称，该方法为一部分此前没有 ATP 证明的 Mizar 翻译定理找到了新的 first-order proofs，使语料中具有 ATP 证明的覆盖率从约 56% 提升到 59%。

为什么重要？

该工作展示了神经模型不仅可以作为上游过滤器，还可以直接影响成熟自动定理证明器的内部搜索循环。这一区别后来成为学习式 clause guidance、强化学习证明搜索以及 search-in-the-loop theorem proving 的重要技术前史。

重要性说明：Deep Network Guided Proof Search 是从“学习式前提选择”进一步走向“直接学习证明器内部搜索控制”的重要早期节点。该工作从 Mizar 衍生的证明轨迹训练神经模型，并把预测直接接入 E prover 的 processed-clause selection，在后来的强化学习与证明助手原生系统出现之前，建立了深度学习引导自动定理证明内部搜索的具体路线。

历史脉络

更早进展
后续进展
相关里程碑

—

主要证据

证据与状态一览

重要性
H2 · 领域里程碑
验证状态
论文已发布
证据等级
E2 · 研究记录
AI 角色
AI 自主主导
形式保障
无形式保障

如何理解这些标签？ →

贡献与验证

数学新颖性
工具性进展
接口
形式化, 符号
AI 贡献
学习式神经模型在自动证明搜索中排序 processed clauses，由 E prover 执行符号推理并构造成功的一阶逻辑证明，不需要人类逐步干预证明动作。
人类贡献
研究者设计神经 clause-guidance 模型、证明轨迹训练数据、混合与两阶段搜索策略、E prover 集成以及基于 Mizar 衍生问题的评测方案。
验证状态
论文已发布 · E2 · 研究记录 · 无形式保障
最后审阅
2026-09-15

技术细节

系统
e-prover, deep-network-guided-proof-search
机构
google-research, university-of-innsbruck
数学问题
automated-theorem-proving, mizar-theorem-proving
方法
deep-learning, clause-selection, proof-search, saturation-based-theorem-proving, supervised-learning

全部来源与工件

验证历史

  • 2017-01-24 · 论文已发布 · E2 · 研究记录

    arXiv 与 LPAR 研究记录确认了神经证明搜索引导方法及论文报告的 Mizar 衍生定理证明结果。Chronicle 当前未记录可直接检查的证明 artifact 或独立 replay，因此 formal assurance 保持为 `none`。

更正

当前没有记录的更正。