蒙特卡洛表演算证明搜索
计算机科学中的逻辑
2019-06-18 v2 人工智能
机器学习
摘要
我们研究蒙特卡洛树搜索以指导表演算中的证明搜索。这包括提出若干证明状态评估启发式方法，其中一些从先前的证明中学习。我们给出了基于leanCoP证明器的实现。该系统在来自Mizar证明助手的大量相关问题上进行了训练与评估，表明其能够找到新的且不同的证明。
引用
@article{arxiv.1611.05990,
title = {Monte Carlo Tableau Proof Search},
author = {Michael Färber and Cezary Kaliszyk and Josef Urban},
journal= {arXiv preprint arXiv:1611.05990},
year = {2019}
}