×

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

Citations by Year