主要证据
- TacticToe: Learning to Reason with HOL4 Tactics — LPAR-21S1 · 主要研究来源 · 论文 · 2017-05-04
- TacticToe: Learning to Prove with TacticsS1 · 主要研究来源 · 论文 · 2018-04-02
- HOL4 TacticToe implementationS1 · 主要研究来源 · 代码仓库
TacticToe 从人工 HOL4 证明中学习 tactic 级证明搜索
TacticToe 从 HOL4 中记录 tactic 级证明信息，学习在新目标状态下哪些证明动作更有希望，并直接在高阶逻辑环境中搜索完整 tactic 序列，而不是把每个问题都翻译到一阶逻辑。
发生了什么？
Thibault Gauthier、Cezary Kaliszyk 与 Josef Urban 在 2017 年 5 月 4 日发布的 LPAR-21 proceedings 中提出 TacticToe。系统从既有 HOL4 证明中学习 tactic 与前提选择，并使用改进 A* 搜索探索 tactic 级证明路径；论文报告在五秒限制下重新证明了 7,902 个 HOL4 定理中的 39%。2018 年发布的扩展研究进一步把搜索机制发展为蒙特卡洛树搜索，并在 HOL4 标准库上报告了更强结果。
TacticToe 从 HOL4 中记录 tactic 级证明信息，学习在新目标状态下哪些证明动作更有希望，并直接在高阶逻辑环境中搜索完整 tactic 序列，而不是把每个问题都翻译到一阶逻辑。2017 年系统采用改进 A* 风格搜索并结合 tactic prediction 与小规模 hammering；后续扩展实现进一步发展搜索机制，相关代码至今仍可在 HOL4 仓库中检查。
为什么重要？
该工作展示了机器学习可以直接引导证明助手原生的 tactic 搜索，而不仅仅为外部自动证明器筛选前提。“学习式动作预测 + 搜索 + 内核检查证明”的组合后来成为神经交互式定理证明中反复出现的设计范式。
重要性说明：TacticToe 是较早具有代表性的证明助手原生学习系统之一，利用既有人工 HOL4 证明，在成熟交互式定理证明器内部直接引导 tactic 级证明搜索。LPAR-21 的初始版本将学习式 tactic / premise selection 与改进 A* 搜索结合，2018 年扩展研究又进一步以蒙特卡洛树搜索发展同一系统；这一路线后来由 TacticZero 等强化学习系统继续推进。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 工具性进展
- 接口
- 形式化, 符号
- AI 贡献
- 学习式预测器负责排序 tactics 与支持前提，搜索算法负责探索证明路径；成功的证明脚本最终在 HOL4 内构造并接受检查。
- 人类贡献
- 研究者设计证明轨迹记录、学习式预测器、tactic 级搜索机制、HOL4 集成与评测协议；学习信号来自既有人工编写的 HOL4 证明。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-15
技术细节
- 系统
- tactictoe, hol4
- 机构
- —
- 数学问题
- hol4-theorem-proving
- 方法
- tactic-prediction, premise-selection, a-star-search, monte-carlo-tree-search, proof-search
全部来源与工件
- TacticToe: Learning to Reason with HOL4 Tactics — LPAR-21S1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- TacticToe: Learning to Prove with TacticsS1 · 主要研究来源 · 论文 · 访问于 2026-09-15
- HOL4 TacticToe implementationS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-15
验证历史
- 2017-05-04 · 论文已发布 · E2 · 研究记录
LPAR-21 proceedings 确认了首次公开的 TacticToe 系统、其学习式 tactic 级证明搜索以及论文报告的 HOL4 评测。machine_checked 仅指证明脚本通过 HOL4 检查，并不表示论文报告的成功率已获得独立复现。
- 2018-04-02 · 论文已发布 · E2 · 研究记录
2018 年扩展研究记录描述了后续蒙特卡洛树搜索版本及更强的 HOL4 标准库评测，但并未构成另一个独立的 TacticToe 历史事件。
- 2026-09-15 · 论文已发布 · E3 · 可检查工件
持续维护的 HOL4 公开仓库包含 TacticToe 实现、证明记录流程、评测支持与使用说明。E3 表示存在可直接检查的 artifacts，而非对全部实验结论的独立验证。
更正
- 2026-09-15
在确认 LPAR-21 proceedings 已于 2017-05-04 公开初始 TacticToe 系统后，将 canonical event date 从 2018-04-02 纠正为 2017-05-04，并区分 2017 年 A* 引导版本与 2018 年蒙特卡洛树搜索扩展研究，同时保留稳定 Event ID。