ATPboost：在二分类设定下利用 ATP 反馈学习前提选择
人工智能
2018-02-12 v1 计算机科学中的逻辑
机器学习
摘要
ATPboost 是一个通过交错运行 ATP 与从证明中进行前提选择的最先进机器学习来解决大理论问题集的系统。与许多使用多标签设定的先前方法不同，该学习被实现为估计（定理，前提）对两两相关性的二分类。ATPboost 为此使用 XGBoost 梯度提升算法，该算法快速且在许多任务上具有最先进的性能。然而，二分类设定下的学习需要负例，由于许多替代证明，这一点并非平凡。我们在 ATP/ML 反馈循环的背景下讨论并实现了若干解决方案，并表明采用此类方法的 ATPboost 显著优于 k 近邻多标签分类器。
引用
@article{arxiv.1802.03375,
title = {ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback},
author = {Bartosz Piotrowski and Josef Urban},
journal= {arXiv preprint arXiv:1802.03375},
year = {2018}
}