ATPboost: Learning Premise Selection
in Binary Setting with ATP Feedback
Bartosz Piotrowski1,2 and Josef Urban1?
1

arXiv:1802.03375v1 [] 9 Feb 2018

2

Czech Institute of Informatics, Robotics and Cybernetics, Prague, Czech Republic
Faculty of Mathematics, Informatics and Mechanics, University of Warsaw, Poland

Abstract. 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.
Keywords: automated theorem proving · machine learning · formalized
mathematics

1

Introduction: Machine Learning for Premise Selection

Assume that c is a conjecture which is a logical consequence of a large set of
premises P . The chance of finding a proof of c by an automated theorem prover
(ATP) often depends on choosing a small subset of P relevant for proving c.
This is known as the premise selection task [1]. This task is crucial to make
ATPs usable for proof automation over large formal corpora created with systems such as Mizar, Isabelle, HOL, and Coq [4]. Good methods for premise
selection typically also transfer to related tasks, such as internal proof guidance
of ATPs [8,10,13,17] and tactical guidance of ITPs [7].
The most efficient premise selection methods use data-driven/machine-learning
approaches. Such methods work as follows. Let T be a set of theorems with their
proofs. Let C be a set of conjectures without proofs, each associated with a
set of available premises that can be used to prove them. We want to learn a
(statistical) model from T , which for each conjecture c ∈ C will rank its available premises according to their relevance for producing an ATP proof of c. Two
different machine learning settings can be used for this task:
?

Supported by the AI4REASON ERC Consolidator grant number 649043, and by
the Czech project AI&Reasoning CZ.02.1.01/0.0/0.0/15_003/0000466 and the European Regional Development Fund.

2

1. multilabel classification: we treat premises used in the proofs as opaque labels
and we create a model capable of labeling conjectures based on their features,
2. binary classification: here the aim of the learning model is to recognize
pairwise-relevance of the (conjecture, premise) pairs, i.e. to decide what is
the chance of a premise being relevant for proving the conjecture based on
the features of both the conjecture and the premise.
Most of the machine learning methods for premise selection have so far used
the first setting [3,9,11]. This includes fast and robust machine learning algorithms such as naive Bayes and K nearest neighbors (k-NN) capable of multilabel classification with many examples and labels. This is needed for large
formal libraries with many facts and proofs. There are however several reasons
why the second approach may be better:
1. Generality: in binary classification it is easier to estimate the relevance of
(conjecture, premise) pairs where the premise was so far unseen (i.e., not in
the training data).
2. State-of-the-art ML algorithms are often capable of learning subtle aspects of
complicated problems based on the features. The multilabel approach trades
the rich feature representation of the premise for its opaque label.
3. Many state-of-the-art ML algorithms are binary classifiers or they struggle
when performing multilabel classification for a large number of labels.
Recently, substantial work [2] has been done in the binary setting. In particular,
applying deep learning to premise selection has improved state of the art in
the field. There are however modern and efficient learning algorithms such as
XGBoost [5] that are much less computationally-intensive then deep learning
methods. Also, obtaining negative examples for training the binary classifiers is
a very interesting problem in the context of many alternative ATP proofs and a
feedback loop between the ATP and the learning system.
1.1

Premise Selection in Binary Setting with Multiple Proofs

The existence of multiple ATP proofs makes premise selection different from
conventional machine learning applications. This is evident especially in the binary classification setting. The ML algorithms for recognizing pairwise relevance
of (conjecture, premise) pairs require good data consisting of two (typically balanced) classes of positive and negative examples. But there is no conventional
way how to construct such data in our domain. For every true conjecture there
are infinitely many mathematical proofs. The ATP proofs are often based on
many different sets of premises. The notions of useful or superfluous premise are
only approximations of their counterparts defined for sets of premises.
As an example, consider the following frequent situation: a conjecture c can
be ATP-proved with two sets of axioms: {p1 , p2 } and {p3 , p4 , p5 }. Learning only
from one of the sets as positives and presenting the other as negative (conjecture,
premise) pairs may considerably distort the learned notion of a useful premise.
This differs from the multilabel setting, where negative data are typically not
used by the fast ML algorithms such as naive Bayes and k-NN. They just aggregate different positive examples into the final ranking.

3

Therefore, to further improve the premise selection algorithms it seems useful
to consider learning from multiple proofs and to develop methods producing
good negative data. The most suitable way how to do that is to allow multiple
interactions of the machine learner with the ATP system. In the following section
we present the ATPboost system, which implements several such algorithms.

2

ATPboost: Setting, Algorithms and Components

ATPboost3 is a system for solving sets of large-theory problems by interleaving
ATP runs with learning of premise selection from the proofs using the stateof-the-art XGBoost algorithm. The system implements several algorithms and
consists of several components described in the following sections. Its setting
is a large theory T , extracted from a large ITP library where facts appear in a
chronological order. In more detail, we assume the following inputs and notation:
1. T – names of theorems (and problems) in a large theory T .
2. P – names of all facts (premises) in T . We require P ⊇ T .
3. StatementsP of all p ∈ P in the TPTP format [15] .
4. FeaturesP – characterizing each p ∈ P . Here we use the same features as
in [11] and write fp for the (sparse) vector of features of p.
5. OrderP (<P ) – total order on P ; p may be used to prove t iff p <P t. We
write At for {p : p <P t}, i.e. the set of premises allowed for t.
6. ProofsT 0 for a subset T 0 ⊆ T . Each t ∈ T 0 may have many proofs – denoted
by Pt . Pt denotes the premises needed for at least one proof in Pt .
2.1

Algorithms

We first give a high-level overview and pseudocode of the algorithms implemented in ATPboost. Section 2.2 then describes the used components in detail.
Algorithm 1 is the simplest setting. Problems are split into the train/test
sets, XGBoost learns from the training proofs, and its predictions are ATPevaluated on the test set. This is used mainly for parameter optimization.
Algorithm 2 evaluates the trained XGBoost also on the training part, possibly
finding new proofs that are used to update the training data for the next
iteration. The test problems and proofs are never used for training. Negative mining may be used to find the worst misclassified premises and to
correspondingly update the training data in the next iteration.
Algorithm 3 begins with no training set, starting with ATP runs on random
rankings. XGBoost is trained on the ATP proofs from the previous iteration,
producing new ranking for all problems for the next iteration. This is a
MaLARea-style [16] feedback loop between the ATP and the learner.
2.2

Components

Below we describe the main components of the ATPboost algorithms and the
main ideas behind them. As discussed in Section 1, they take into account the
3

The Python package is at https://github.com/BartoszPiotrowski/ATPboost.

4

binary learning setting, and in particular implement the need to teach the system
about multiple proofs by proper choice of examples, continuous interaction with
the ATP and intelligent processing of its feedback. The components are available
as procedures in our Python package.
Algorithm 1 Simple training/test split.
Require: Set of theorems T , set of premises P ⊇ T , ProofsT , FeaturesP , StatementsP , OrderP ,
paramsset , paramsmodel .
1: Ttrain , Ttest ← RandomlySplit(T )
2: D ← CreateTrainingSet(ProofsTtrain , FeaturesP , OrderP , paramsset )
3: M ← TrainModel(D, paramsmodel )
4: R ← CreateRankings(Ttest , M, FeaturesP , OrderP )
5: P ← ATPevaluation(R, StatementsP )

Algorithm 2 Incremental feedback-loop with training/test split.
Require: Set of theorems T , set of premises P ⊇ T , FeaturesP , StatementsP , ProofsT , OrderP ,
paramsset , paramsmodel , paramsnegmin (optionally).
1: Ttrain , Ttest ← RandomlySplit(T )
2: D ← CreateTrainingSet(ProofsTtrain , FeaturesP , OrderP , paramsset )
3: repeat
4:
M ← TrainModel(D, paramsmodel )
5:
Rtrain ← CreateRankings(Ttrain , M, FeaturesP , OrderP )
6:
Rtest ← CreateRankings(Ttest , M, FeaturesP , OrderP )
7:
Ptrain ← ATPevaluation(Rtrain , StatementsP )
8:
Ptest ← ATPevaluation(Rtest , StatementsP )
9:
Update(Proofstrain , Ptrain )
10:
Update(Proofstest , Ptest )
11:
if paramsnegmin then
12:
D ← NegativeMining(R, Proofstrain , FeaturesP , OrderP , paramsnegmin )
13:
else
14:
D ← CreateTrainingSet(Proofstrain , FeaturesP , OrderP , paramsset )
15: until Number of Proofstest increased after Update.

Algorithm 3 Incremental feedback-loop starting with no proofs.
Require: Set of theorems T , set of premises P ⊇ T , FeaturesP , StatementsP , OrderP , paramsset ,
paramsmodel , paramsnegmin (optionally).
1: ProofsT ← ∅
2: R ← CreateRandomRankings(T )
3: P ← ATPevaluation(R, StatementsP )
4: Update(ProofsT , P)
5: D ← CreateTrainingSet(ProofsT , FeaturesP , OrderP , paramsset )
6: repeat
7:
M ← TrainModel(D, paramsmodel )
8:
R ← CreateRankings(T, M, FeaturesP , OrderP )
9:
P ← ATPevaluation(R, StatementsP )
10:
Update(ProofsT , P)
11:
if paramsnegmin then
12:
D ← NegativeMining(R, ProofsT , FeaturesP , OrderP , paramsnegmin )
13:
else
14:
D ← CreateTrainingSet(ProofsT , FeaturesP , OrderP , paramsset )
15: until Number of ProofsT increased after Update.

CreateTrainingSet(ProofsT , FeaturesP , OrderP , params). This
procedure constructs a TrainingSet for a binary learning algorithm. This is
a sparse matrix of positive/negative examples and a corresponding vector of

5

binary labels. The examples (matrix rows) are created from ProofsT and FeaturesP , respecting OrderP . Each example is a concatenation of ft and fp ,
i.e., the features of a theorem t and a premise p. Positive examples express that
p is relevant for proving t, whereas the negatives mean the opposite.
The default method (simple) creates positives from all pairs (t, p) where
p ∈ Pt . Another method (short) creates positives only from the short proofs of
t. These are the proofs of t with at most m + 1 premises, where m is the minimal
number of premises used in a proof from Pt . Negative examples for theorem t
are chosen randomly from pairs (t, p) where p ∈ At \ Pt . The number of such
randomly chosen pairs is ratio · Npos , where Npos is the number of positives
and ratio∈ N is a parameter that needs to be optimized experimentally. Since
|At \ Pt | is usually much larger than |Pt |, it seems reasonable to have a large
ratio. This however increases class imbalance and the probability of presenting
to the learning algorithm a false negative. This is a pair (t, p) where p ∈
/ Pt , but
there is an ATP proof of t using p that is not yet in our dataset.
TrainModel(TrainingSet, params). This procedure trains a binary
learning classifier on the TrainingSet, creating a Model. We use XGBoost [5]
– a state-of-the-art tree-based gradient boosting algorithm performing very well
in machine learning competitions. It is also much faster to train compared to
deep learning methods, performs well with unbalanced training sets, and is optimized for working with sparse data. XGBoost has several important parameters,
such as numberOfTrees, maxDepth (of trees) and eta (learning rate). These
parameters have significant influence on the performance and require tuning.
CreateRankings(C, Model, FeaturesP , OrderP ). This procedure
uses the trained Model to construct RankingsC of premises from P for conjectures c ∈ C ⊆ T . Each conjecture c is paired with each premise p <P c and
concatenations of fc and fp are passed to the Model. The Model outputs a
real number in [0, 1], which is interpreted as the relevance of p for proving c. The
relevances are then used to sort the premises into RankingsC .
ATPevaluation(Rankings, Statements). Any ATP can be used for
evaluation. By default we use E [14] 4 . As usual, we construct the ATP problems
for several top slices (lengths 1, 2, . . . , 512) of the Rankings. To remove redundant premises we pseudo-minimize the proofs: only the premises needed in the
proofs are used as axioms and the ATP is rerun until a fixpoint is reached.
Update(OldProofs, NewProofs). The Update makes a union of the
new and old proofs, followed by a subsumption reduction. I.e., if premises of two
proofs of t are in a superset relation, the proof with the larger set is removed.
NegativeMining(ProofsT , RankingsT , FeaturesP , OrderP ,
params). This is used as a more advanced alternative to CreateTrainingSet. It examines the last RankingsT for the most misclassified positives.
I.e., for each t ∈ T we create a set MP t of those p that were previously ranked
high for t, but no ATP proof of t was using p. We define three variants:
4

The default time limit is 10 seconds and the memory limit is 2GB. The exact default
command is: ./eprover –auto-schedule –free-numbers -s -R –cpu-limit=10
–memory-limit=2000 –print-statistics -p –tstp-format problem_file

6

1. negmin_all: Let mt be the maximum rank of a t-useful premise (p ∈ Pt )
in RankingsT [t]. Then MP 1t = {p : rankt (p) < mt ∧ p ∈
/ Pt }.
2. negmin_rand: We randomly choose into MP 2t only a half of MP 1t .
3. negmin_1: MP 3t = {p : rankt (p) < |Pt | ∧ p ∈
/ Pt }.
The set MP it is then added as negatives to the examples produced by the CreateTrainingSet procedure. The idea of such negative mining is that the learner
takes into account the mistakes it made in the previous iteration.

3

Evaluation

We evaluate5 the algorithms on a set of 1342 MPTP2078 [1] large (chainy)
problems that are provable in 60s using their small (bushy) versions.
Parameter tuning: First we run Algorithm 1 to optimize the parameters.
The dataset was randomly split into a train set of 1000 problems and test set
of 342. For the train set, we use the proofs obtained by the 60s run on the
bushy versions. We tune the ratio parameter of CreateTrainingSet, and
the numberOfTrees, maxDepth and eta parameters of TrainModel. Due
to resource constraints we a priori assume good defaults: ratio = 16, numberOfTrees = 2000, maxDepth = 10, eta = 0.2. Then we observe how
changing each parameter separately influences the results. Table 1 shows the
ATP results for the ratio parameter, and Figure 1 for the model parameters.
It is clear that a high number of negatives is important. Using ratio = 16
1
2
4
8 16 32 64
ratio
Proved (%) 74.0 78.4 79.0 78.7 80.1 79.8 80.1

Table 1: Influence of the ratio of randomly generated negatives to positives.

Fig. 1: ATP performance of different parameters of the XGBoost model.
proves 6% more test problems than the balanced setting (ratio = 1). It is also
5

All the scripts we used for the evaluation are available at https://github.com/
BartoszPiotrowski/ATPboost/tree/master/experiments

7

clear that a higher number of trees – at least 500 – improves the results. However, too many trees (over 8000) slightly decrease the performance, likely due to
overfitting. The eta parameter gives best results with values between 0.04 and
0.64, and the maxDepth of trees should be around 10.
We evaluate Algorithm 1 also on a much bigger ATP-provable part of MML
with 29271 theorems in train part and 3253 in test. With parameters ratio = 20,
numberOfTrees = 4000, maxDepth = 10 and eta = 0.2 we proved 58.78%
theorems (1912). This is a 15.7% improvement over k-NN, which proved 50.81%
(1653) theorems. For a comparison, the improvement over k-NN obtained (with
much higher ATP time limits) with deep learning in [2] was 4.3%.
Incremental feedback loop with train/test split: This experiment evaluates Algorithm 2, testing different methods of negative mining. The train/test
split and the values of the parameters ratio, numberOfTrees, maxDepth,
eta are taken from the previous experiment. We test six methods in parallel.
Two XGB methods (simple and short) are the variants of the CreateTrainingSet procedure, three XGB methods (negmin_all, negmin_rand and
negmin_1) are the variants of NegativeMining, and the last one is a k-NN
learner similar to the one from [11], used here for comparison.
The experiment starts with the same proofs for training theorems as in the
previous one, and we performed 30 rounds of the feedback loop. Figure 2 shows
the results. All the new methods largely outperform k-NN, and XGB_short

Fig. 2: Number of proved theorems in subsequent iterations of Algorithm 2.
is much better than XGB_simple. I.e., positives from too many proofs seem
harmful, as in [12] where this was observed with k-NN. The differences between
the XGB variants short, negmin_1, negmin_all, and negmin_rand do
not seem significant and all perform well. At the end of the loop (30th round)
315-319 theorems of the 342 (ca 93%) are proved.
Incremental feedback-loop with no initial proofs: This is the final experiment which corresponds to the Algorithm 3 – there is no train/test split
and no initial proofs. The first ATP evaluation is done on random rankings,
proving 335 simple theorems out of the 1342. Than the feedback loop starts
running with the same options as in the previous experiment. Fig. 3 shows the
numbers of theorems that were proved in the subsequent rounds, as well as the

8

growth of the total number of different proofs. This is important, because all
these proofs are taken into account by the machine learning. Again, k-NN is the
weakest and XGB_simple is worse than the rest of the methods, which are
statistically indistinguishable. In the last round XGB_negmin_rand proves
1150 (86%) theorems. This is 26.8% more than k-NN (907) and 7.7% more than
XGB_simple (1068).

Fig. 3: Number of proved theorems (left) and number of all found proofs (right)
in subsequent rounds of the experiment corresponding to Algorithm 3.

References
1. J. Alama, T. Heskes, D. Kühlwein, E. Tsivtsivadze, and J. Urban. Premise selection
for mathematics by corpus analysis and kernel methods. J. Autom. Reasoning,
52(2):191–213, 2014.
2. A. A. Alemi, F. Chollet, G. Irving, C. Szegedy, and J. Urban, editors. DeepMath
- Deep Sequence Models for Premise Selection, 2016.
3. J. C. Blanchette, D. Greenaway, C. Kaliszyk, D. Kühlwein, and J. Urban. A
learning-based fact selector for Isabelle/HOL. J. Autom. Reasoning, 57(3):219–
244, 2016.
4. J. C. Blanchette, C. Kaliszyk, L. C. Paulson, and J. Urban. Hammering towards
QED. J. Formalized Reasoning, 9(1):101–148, 2016.
5. T. Chen and C. Guestrin. Xgboost: A scalable tree boosting system. 2016.
6. T. Eiter and D. Sands, editors. LPAR-21, 21st International Conference on Logic
for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, May 712, 2017, volume 46 of EPiC Series in Computing. EasyChair, 2017.
7. T. Gauthier, C. Kaliszyk, and J. Urban. TacticToe: Learning to reason with HOL4
tactics. In Eiter and Sands [6], pages 125–143.
8. J. Jakubuv and J. Urban. ENIGMA: efficient learning-based inference guiding
machine. In H. Geuvers, M. England, O. Hasan, F. Rabe, and O. Teschke, editors,
Intelligent Computer Mathematics - 10th International Conference, CICM 2017,
Edinburgh, UK, July 17-21, 2017, Proceedings, volume 10383 of Lecture Notes in
Computer Science, pages 292–302. Springer, 2017.
9. C. Kaliszyk and J. Urban. Learning-assisted automated reasoning with Flyspeck.
J. Autom. Reasoning, 53(2):173–213, 2014.

9
10. C. Kaliszyk and J. Urban. FEMaLeCoP: Fairly efficient machine learning connection prover. In M. Davis, A. Fehnker, A. McIver, and A. Voronkov, editors, Logic
for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume
9450 of Lecture Notes in Computer Science, pages 88–96. Springer, 2015.
11. C. Kaliszyk and J. Urban. Mizar 40 for mizar 40. Journal of Automated Reasoning,
55(3):245–256, Oct 2015.
12. D. Kuehlwein and J. Urban. Learning from multiple proofs: First experiments.
In P. Fontaine, R. A. Schmidt, and S. Schulz, editors, PAAR-2012, volume 21 of
EPiC Series, pages 82–94. EasyChair, 2013.
13. S. M. Loos, G. Irving, C. Szegedy, and C. Kaliszyk. Deep network guided proof
search. In Eiter and Sands [6], pages 85–105.
14. S. Schulz. E - A Brainiac Theorem Prover. AI Commun., 15(2-3):111–126, 2002.
15. G. Sutcliffe. The TPTP problem library and associated infrastructure. J. Autom.
Reasoning, 43(4):337–362, 2009.
16. J. Urban, G. Sutcliffe, P. Pudlák, and J. Vyskočil. MaLARea SG1 - Machine
Learner for Automated Reasoning with Semantic Guidance. In IJCAR, pages
441–456, 2008.
17. J. Urban, J. Vyskočil, and P. Štěpánek. MaLeCoP: Machine learning connection
prover. In K. Brünnler and G. Metcalfe, editors, TABLEAUX, volume 6793 of
LNCS, pages 263–277. Springer, 2011.

