主要证据
- Proving Theorems using Incremental Learning and Hindsight Experience ReplayS1 · 主要研究来源 · 论文 · 2021-12-20
- Proving Theorems using Incremental Learning and Hindsight Experience ReplayS1 · 主要研究来源 · 论文 · 2022-06-28
增量学习与 hindsight replay 减少一阶定理证明中的手工搜索启发式
系统把 clause 编码为图并交由基于 Transformer 的模型评分。训练以增量方式推进，同时使用 hindsight replay 将失败搜索中的中间状态转化为额外学习目标，而不是丢弃这些轨迹。
发生了什么？
作者以基础 given-clause 算法构建一阶逻辑证明器，用学习式神经评分器替代手工 clause-scoring 启发式，并利用 hindsight experience replay 从失败证明搜索中提取训练信号；所得证明器在多个源自 TPTP 的基准上达到或超过强传统基线。
为什么重要？
该系统较早展示了如何用证明搜索过程中自产生的经验替代脆弱的手工搜索知识，这一模式后来成为自我改进神经证明器和推理智能体的重要组成部分。
重要性说明：该工作展示了学习式一阶证明器可以用增量训练的神经评分器替代强自动证明器中大量手工 clause-selection 启发式，并借助 hindsight experience replay 从失败搜索中学习，在标准定理证明基准上达到具有竞争力的性能。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E2 · 研究记录
- AI 角色
- AI 主导、人类核验
- 形式保障
- 无形式保障
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式 clause scorer 负责引导证明搜索，并从搜索经验中迭代改进，其中也包括最初未找到证明的轨迹。
- 人类贡献
- 研究者设计 given-clause 环境、图表示、Transformer 评分器、hindsight replay 训练方案与基准评测。
- 验证状态
- 论文已发布 · E2 · 研究记录 · 无形式保障
- 最后审阅
- 2026-09-11
技术细节
- 系统
- her-theorem-prover
- 机构
- deepmind
- 数学问题
- first-order-theorem-proving
- 方法
- incremental-learning, hindsight-experience-replay, learned-clause-selection, transformer, proof-search
全部来源与工件
- Proving Theorems using Incremental Learning and Hindsight Experience ReplayS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
- Proving Theorems using Incremental Learning and Hindsight Experience ReplayS1 · 主要研究来源 · 论文 · 访问于 2026-09-11
验证历史
- 2021-12-20 · 论文已发布 · E2 · 研究记录
Chronicle 根据公开研究论文记录该系统及其报告的定理证明结果；本记录未使用可直接链接的公开代码或独立 replay artifact 来提高证据等级。
更正
当前没有记录的更正。