# ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback

arXiv: https://arxiv.org/abs/1802.03375 · HTML: https://mlsanity.com/paper/1802.03375/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 9 Feb 2018.

## Built on by (most cited first, 12 of 12)

- [Magnushammer: A Transformer-Based Approach to Premise Selection](https://mlsanity.com/paper/2303.04488/) (2023)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Contrastive Reinforcement Learning of Symbolic Reasoning Domains](https://mlsanity.com/paper/2106.09146/) (2021)
- [Machine-Learned Premise Selection for Lean](https://mlsanity.com/paper/2304.00994/) (2023)
- [Alien Coding](https://mlsanity.com/paper/2301.11479/) (2023)
- [The Isabelle ENIGMA](https://mlsanity.com/paper/2205.01981/) (2022)
- [Online Machine Learning Techniques for Coq: A Comparison](https://mlsanity.com/paper/2104.05207/) (2021)
- [Learning Guided Automated Reasoning: A Brief Survey](https://mlsanity.com/paper/2403.04017/) (2024)
- [MizAR 60 for Mizar 50](https://mlsanity.com/paper/2303.06686/) (2023)
- [Learning Conjecturing from Scratch](https://mlsanity.com/paper/2503.01389/) (2025)
- [Learning to Prove Trigonometric Identities](https://mlsanity.com/paper/2207.06679/) (2022)
- [Partial Label Learning for Automated Theorem Proving](https://mlsanity.com/paper/2507.03314/) (2025)

## Abstract (arXiv)

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.