ATPboost swMATH ID: 28626 Software Authors: Piotrowski, Bartosz; Urban, Josef Description: ATPboost: learning premise selection in binary setting with ATP feedback. 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 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 fast state-of-the-art XGBoost gradient boosting algorithm. 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 significant improvement over the multi-label approach. Homepage: https://arxiv.org/abs/1802.03375 Source Code: https://github.com/BartoszPiotrowski/ATPboost Dependencies: Python Related Software: XGBoost; MaLARea; Isabelle/HOL; Mizar; BliStr; BliStrTune; HOList; Flyspeck; TPTP; MPTP 0.2; ENIGMA; TacticToe; FEMaLeCoP; E Theorem Prover; MaLeCoP; HOL; Nitpick; HipSpec; Easychair; Tensor2Tensor Cited in: 6 Documents Standard Articles 1 Publication describing the Software, including 1 Publication in zbMATH Year ATPboost: learning premise selection in binary setting with ATP feedback. Zbl 1511.68257Piotrowski, Bartosz; Urban, Josef 2018 all top 5 Cited by 26 Authors 4 Urban, Josef 2 Piotrowski, Bartosz 1 Balog, Matej 1 Barekatain, Mohammadamin 1 Blaauwbroek, Lasse 1 Černỳ, Prokop 1 Chvalovský, Karel 1 Fawzi, Alhussein 1 Gauthier, Thibault 1 Hassabis, Demis 1 Huang, Aja 1 Hubert, Thomas 1 Jakubův, Jan 1 Kaliszyk, Cezary 1 Kohli, Pushmeet 1 Olšák, Miroslav 1 Proroković, Krsto 1 Romera-Paredes, Bernardino 1 Ruiz, Francisco J. R. 1 Schmidhuber, Jürgen 1 Schrittwieser, Julian 1 Silver, David M. 1 Suda, Martin 1 Świrszcz, Grzegorz M. 1 Wand, Michael 1 Zhang, Liao Cited in 2 Serials 1 International Journal of Approximate Reasoning 1 Nature, London Cited in 4 Fields 6 Computer science (68-XX) 1 Mathematical logic and foundations (03-XX) 1 Number theory (11-XX) 1 Numerical analysis (65-XX) Citations by Year