主要证据
- HyperTree Proof Search for Neural Theorem ProvingS1 · 主要研究来源 · 论文 · 2022-05-23
- Evariste code accompanying HyperTree Proof SearchS1 · 主要研究来源 · 代码仓库
HyperTree Proof Search 引入神经定理证明的在线自我改进
系统从自身证明搜索中继续学习，并使用受蒙特卡洛树搜索与 AlphaZero 启发的超树搜索算法。
发生了什么？
HTPS 配合在线训练在留出 Metamath 定理上达到 82.6%，并将 miniF2F-curriculum 的证明率提升到 42%。
为什么重要？
它预示了后来形式推理系统中广泛采用的“验证器反馈 + 自我改进”训练循环。
重要性说明：HTPS 将 AlphaZero 式搜索与在线学习结合，在 Metamath 与 Lean 定理证明上均取得显著提升。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 证明器执行搜索、从成功与失败的轨迹中学习，并迭代改进策略。
- 人类贡献
- 研究者设计 HTPS、训练环境与基准协议。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- htps
- 机构
- meta-ai
- 数学问题
- metamath, minif2f
- 方法
- online-training, tree-search, expert-iteration
全部来源与工件
- HyperTree Proof Search for Neural Theorem ProvingS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- Evariste code accompanying HyperTree Proof SearchS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2022-05-23 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。