TacticToe：学习用策略证明定理
人工智能
2021-12-03 v2 计算机科学中的逻辑
摘要
我们在 HOL4 交互式定理证明器之上实现了自动策略证明器 TacticToe。TacticToe 从人类证明中学习每种证明情境下适用的数学技巧。该知识随后被用于蒙特卡洛树搜索算法，以探索有前景的策略级证明路径。在单 CPU、时限 60 秒下，TacticToe 证明了 HOL4 标准库中 7164 个定理的 66.4%，而带自动调度的 E 证明器解决了 34.5%。结合 TacticToe 与 E 证明器的结果，成功率上升至 69.0%。
引用
@article{arxiv.1804.00596,
title = {TacticToe: Learning to Prove with Tactics},
author = {Thibault Gauthier and Cezary Kaliszyk and Josef Urban and Ramana Kumar and Michael Norrish},
journal= {arXiv preprint arXiv:1804.00596},
year = {2021}
}