ATPboost：基于ATP反馈的二进制学习优先级选择
ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
摘要：
ATPboost是一个通过将ATP运行与最先进的机器学习从证明中选择前提来解决大型理论问题的系统。与许多以前使用多标签设置的方法不同，学习被实现为二进制分类，估计（定理，前提）对的成对相关性。ATPboost为此使用XGBoost梯度提升算法，该算法速度快，在许多任务上具有最先进的性能。然而，在二进制设置中学习需要反例，由于许多替代证明，这是不平凡的。我们讨论并实现了ATP/ML反馈回路的上下文中的几个解决方案，并表明ATPboost与这些方法显着优于k-最近邻多标签分类器。
英文摘要：
ATPboost is a system for solving sets of large-theory problems by interleaving ATP runs with state-of-the-art machine learning of premise selection from the proofs. Unlike many previous approaches that use multi-label setting, the learning is implemented as binary classification that estimates the pairwise-relevance of (theorem, premise) pairs. ATPboost uses for this the XGBoost gradient boosting algorithm, which is fast and has state-of-the-art performance on many tasks. Learning in the binary setting however requires negative examples, which is nontrivial due to many alternative proofs. We discuss and implement several solutions in the context of the ATP/ML feedback loop, and show that ATPboost with such methods significantly outperforms the k-nearest neighbors multilabel classifier.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
