ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback
This work addresses premise selection for automated theorem proving, an incremental advance in combining ATP and ML for mathematical reasoning.
ATPboost tackles the problem of premise selection in large-theory automated theorem proving by using binary classification with ATP feedback, resulting in significant performance improvements over a k-nearest neighbors multilabel classifier.
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.