Dynamic Strategy Priority: Empower the Strong and Abandon the Weak.

Abstract

Automated theorem provers are often used in other tools as black-boxes for discharging proof obligations. One example where this has enjoyed a lot of success is within interactive theorem proving. A key usability factor in such settings is the time taken for the provers to complete. Automated theorem provers typically run lists of proof strategies sequentially, which can cause proofs to be found more slowly than necessary if the ordering is suboptimal. We show that it is possible to predict which strategies are likely to succeed while they are running using an arti cial neural network. We also implement a run-time strategy scheduler in the Vampire prover which utilises a trained neural network to improve average proof search time, and hence increases usability as a black-box prover.

Introduction

Modern automated theorem provers (e.g. E [ 30 ], iProver [ 12 ], Vampire [ 13 ], CVC4 [ 7 ]) for rst-order logic rely on portfolio modes [ 25 ], which utilise tens to hundreds of distinct strategies. Of these strategies, only a few might solve a hard problem, often rapidly. Typically, a portfolio of strategies has a pre-de ned execution order: the prover will process strategies in this order, running each until a winning strategy is found or the prover runs out of time or strategies.

Portfolio modes are important as, in practice, there is no best strategy. Furthermore, it is uncommon that two hard problems are e ciently solved by the same strategy. However, portfolio execution is not without problems: deciding the optimal ordering and time allocation is hard in general [ 24 ], and produces overly-rigid, brittle engineering when applied to speci c domains, such as those found in the TPTP problem set [ 32 ]. Moreover, for any particular problem, some lengthy strategies that are successful on other problems are doomed to failure from the outset | as illustrated in Figure 1 | but are left to run unchecked by the prover, wasting time that could be spent on more productive strategies.

This work makes two contributions. We rst demonstrate correlation between trends in dynamic properties of proof search, and the pending success or failure of a strategy (Sections 4, 5). We then utilise this to implement strategy scheduling, prioritising those strategies most likely to succeed (Section 6). This approach di ers from previous work [ 30,20,16 ] which attempts to predict successful strategies a priori from static features of the input problem; instead (a) (b) 1 (c) 1 we tip running strategies for success based on dynamic, run-time features and use this information to make decisions at runtime. Our experiments (Section 7) show that guiding scheduling in this way can signi cantly speed up portfoliobased approaches. Before introducing these contributions and results we rst present necessary background in Sections 2 and 3. 2

Strategies in Vampire

Vampire is a rst-order superposition theorem prover. This section reviews its basic structure and components relevant to the rest of this paper. We will use the word strategy to refer to a set of con guration parameter values that control proof search and proof attempt to refer to a run of the prover using such a strategy. 2.1

Input and preprocessing

Vampire accepts problems in rst-order logic with equality and a pre-de ned set of rst-order theories (e.g. arithmetic, arrays, datatypes). Vampire typically works with problems in the TPTP format [ 32 ] but also accepts problems in SMT-LIB [ 3 ].

Problems are parsed and transformed into a set of input clauses used by the saturation algorithm. This process involves clausi cation and a number of preprocessing steps. These preprocessing steps can alter certain properties of the problem e.g. its size and distribution across the signature, sometimes signi cantly: for example, the E.T. system [ 10 ] implements a pre-processor for E which selects small sets of axioms from a larger set, for large-theory reasoning. This means that any prediction method that relies solely on the input problem (rather than dynamic characteristics such as post-preprocessing properties) will nd it harder to predict the best parameters for proof search. 2.2

Saturation algorithms

Superposition provers such as Vampire use saturation algorithms with redundancy elimination. They work with a search space consisting of a set of clauses and use a collection of generating, simplifying and deleting inferences to explore this space. Generating inferences, such as superposition, extend this search space by adding new clauses obtained by applying inferences to existing clauses. Simplifying inferences, such as demodulation, replace a clause by a simpler one. Deleting inferences, such as subsumption, delete a clause, typically when it becomes redundant (see [ 2 ]). Simplifying and deleting inferences must satisfy this condition to preserve completeness.

The goal is to saturate the clause set with respect to the inference system. If the empty clause is derived then the input clauses are unsatis able. If no empty clause is derived and the search space is saturated then the input clauses are guaranteed to be satis able only if a complete strategy is used. A strategy is complete if it is guaranteed that all inferences between non-deleted clauses in the search space will be applied. Vampire includes many incomplete strategies as they can be very e cient at nding unsatis ability.

All saturation algorithms implemented in Vampire belong to the family of given clause algorithms, which achieve completeness via a fair clause selection process that prevents the inde nite skipping of old clauses. These algorithms typically divide clauses into three sets, unprocessed, passive and active, and follow a simple saturation loop: 1. Add non-redundant unprocessed clauses to passive. Redundancy is checked by attempting to forward simplify the new clause using processed clauses. 2. Remove processed (passive and active) clauses made redundant by newly processed clauses, i.e. backward simplify existing clauses using these clauses. 3. Select a given clause from passive, move it to active and perform all generating inferences between the given clause and all other active clauses, adding generated clauses to unprocessed.

Later we will show how iterations of this saturation loop from di erent proof attempts can be interleaved. Vampire implements three saturation algorithms: 1. Otter uses both passive and active clauses for simpli cations. 2. Limited Resource Strategy (LRS) [ 28 ] extends Otter with a heuristic that discards clauses that are unlikely to be used with the current resources, i.e. time and memory. This strategy is incomplete but also generally the most e ective at proving unsatis ability. 3. Discount uses only active clauses for simpli cations.

A recent development in Vampire is AVATAR [ 37,26 ] which integrates with the saturation loop to perform clause splitting. The general idea is to use a SAT solver to select a subproblem by naming each clause sub-component by a propositional variable, running a SAT solver on these abstracted clauses, and using the subsequent propositional model to select components to include in proof search. At the end of each iteration of the loop we check whether the underlying subproblem has changed. AVATAR can occasionally make loops run a little longer, but no more than other steps such as backward subsumption. Otherwise, the notion of saturation loop remains the same when using AVATAR.

There are also other proof strategies that t into the above loop format and can be interleaved with superposition based proof attempts. For example, instance generation [ 8 ] saturates the set of clauses with respect to the instance generation rule and nite model nding [ 27 ] iteratively checks larger model sizes (these loops tend to be much longer than those from other algorithms). 2.3

Strategies in Vampire

Vampire includes more than 50 parameters. By only varying parameters and values used by Vampire at the last CASC competition, we obtain over 500 million strategies. These parameters control { Preprocessing steps (24 di erent parameters) { The saturation algorithm and related behaviour e.g. clause selection { Inferences used (16 di erent kinds with variations) Even restricting these parameters to a single saturation algorithm and straightforward preprocessing steps, the number of possible strategies is vast. For this reason, Vampire implements a portfolio CASC mode [ 13 ] that categorises problems based on syntactic features and attempts a sequence of approximately 50 strategies over a ve minute period (this number can vary signi cantly). These strategies are the result of extensive benchmarking and have been shown, experimentally, to work well on unseen problems i.e. those not used for training.

The syntactic features used by the current portfolio mode are coarse-grained and include the rough size of the problem (e.g. bucketed into tiny, small, medium, large, huge), the presence of features such as equality or certain theories, and whether the problem is e ectively propositional or horn. Not all combinations of these are considered. Portfolio mode is created by considering a set of training data over a list of strategies and attempting to cover as much of it as possible by splitting the set of problems into smaller groups based on these features until all solutions t into a given time limit. This process is greedy and places the strategy that solves the most problems during training rst and then the next best strategy after removing the problems solved by the rst solver and so on. 3

Machine Learning and Theorem Proving

In this section we review the necessary background in machine learning in the context of theorem proving, in particular neural networks. Other technologies exist which are capable of similar performance, but neural networks produced the best combination of convenience and performance for our purposes. Input Layer

Hidden Layer Input 1 Input 2 Input 3 Classi cation

Classi cation with neural networks

Binary classi cation problems can be heuristically solved by means of supervised learning methods. A binary classi cation problem is, informally, the statement \given input X, does X belong to class A or class B", where X is a member of the target domain D, and A; B are disjoint subsets of D such that D = A [ B. Supervised learning methods attempt to solve binary classi cation problems by starting with a neutral, untrained heuristic for classifying X into A or B, then changing their internal state to improve the heuristic by looking at examples of A and B (\training"). Typically, supervised learning methods do not work on X directly, but from a set of \features" derived from X. Engineering features, or choosing which of a set of supplied features to use, is a eld of study in itself.

A neural network consists of a collection of arti cial \neurons", wired together with connections into a neural network architecture (see Figure 2 for an example). Each neuron n computes a real-valued function fn, which may be tuned with real-valued parameters: every neuron has a bias bn, and weight vector wn.

fn is de ned on an input vector x as

fn(x) = A (wn x + bn) i.e. a weighted sum of all connected input neurons' activation functions, plus the bias of the neuron, all fed through an activation function A(x). The choice of activation function is dependent on both the position of the neuron in the architecture, and on the target domain: a common choice is the sigmoid function (x), as shown in Figure 3. 1 Fig. 3: The sigmoid function (x) = 1+e x . This function \squeezes" the output to the range [0; 1].

Neural network parameters may be trained by a variety of di erent techniques (randomly, neuro-evolution methods, backpropagation methods, etc.). We used a backpropagation method, which, given a training input X and correct output y, tunes the network parameters by propagating an error signal backwards through the network to obtain updated parameters for each neuron, hence reducing the error signal for that example [ 29 ]. Repeating this process for multiple training examples can produce very good results, but frequently only with the correct combination of learning algorithm, starting weights, network architecture, and training examples. 3.2

Related work

Machine learning has potential for signi cant e ect in this area: despite the computational di culties experienced by theorem provers, frequently proofs have human (or otherwise regular) structure, which may be exploited by the use of learning methods. The authors are aware of work in the elds of premise selection [ 9,15,35,38 ], static strategy selection [ 4,18,17 ], and more recently, direct proof guidance [ 36,11,19 ]. However, we are not aware of any previous work in the area of strategy selection at runtime for conventional theorem provers. The closest area of work is that of static strategy selection where work, with the exception of Bridge et al. [ 4 ] focusses on static properties of the input problem rather than dynamic properties of the proof search space. Bridge considered various dynamic features of the search space after 100 steps of the saturation algorithm in the default mode (of the E theorem prover [ 30 ]).

So far, machine learning techniques have typically used classical machinelearning techniques such as nave Bayesian methods, SVMs [ 34 ], and decision trees [ 23 ]. However, some newer work has begun to utilise recently-developed deep-neural-network methods [ 9,38,19 ].

Feature collection

This section discusses which features are extracted from Vampire for prediction and how they are extracted. This information is rstly required to identify a correlation and will then be used to train a predictor.

Modifying Vampire to log execution data (such as memory usage, or more speci c metrics such as the number of generated clauses) for di erent strategies obtained from its primary portfolio mode1 is straightforward, but some datacollection decisions were made: { Only numerical data immediately available in the prover was collected, but there is scope here for both non-numeric and derivative data sources, which may provide greater insight into the proof state in future work. Suppose that quantities A and B are measured directly, but are more often discussed in terms of categories C that all A; B pairs fall into. Data could then include C as well, or instead of, A and B, embedding C into the neural network via a one-hot encoding. { Data was collected at intervals of a xed number of internal resolution steps (in the experiments presented in this paper, this value was 10). This may not necessarily correspond to xed time intervals, as each step may be more or less expensive, depending on the strategy and the problem. { All available data was collected, even if it emerged to be constant or unhelpful. This allowed an agnostic approach to learning in which the neural network training procedure selected relevant features.

In all, 376 features are recorded, including the number of active clauses, passive clauses, and subsumptions, for instance. The execution traces produced are di cult to work with, however: some are short or non-existent, others are extremely lengthy. The mean execution trace length was 536 (standard deviation: 1208) with the longest trace being 9971 recorded steps long. Some feature values also have an extremely high variance. To deal with these problems, a post-processing step is applied. For each feature, the mean over the entire data set is then mapped to 0, and the dataset is scaled to unit variance. Data that are too short (fewer than 10 steps) are discarded (the strategy likely did not take very long in any case). The remaining data is then sliced into 10 evenly-sized \buckets", then an average of each bucket is taken to produce 10 values for every trace, and hence a xed data size.

However, even now these data are not representative of the classi cation problem desired: these traces show completed runs of Vampire, whereas the classi er will be used to predict the success or otherwise of runs of Vampire that are still in progress. Hence, we take \snapshots" at various stages (in these experiments, at every quarter) of the trace, discarding the rest of the data, then post-process the remaining trace as described above. Conveniently, this also provides 4 times the original number of training examples. An example post-processed trace is shown in Figure 4. 1 CASC-mode, a portfolio designed for the CASC competition [ 33 ].

Predicting successful strategies

Being able to predict which proof search attempts will succeed in time, and which will fail, based solely on information in the execution trace may seem unlikely. However, it is known that the \slowly-growing search space" maxim, which states that strategies which minimise the number of derived clauses over time are more likely to succeed, is an e ective heuristic for nding good strategies in saturationbased theorem proving [ 24 ]. Since the data we use includes the number of derived clauses, among many other features, it appears more plausible that this approach might work at least as well as the slow-growth heuristic alone. Engineering a prediction algorithm that attempts to partition traces into \succeeding" and \failing" classes is possible with the use of modern machine-learning techniques. Conveniently, these methods do not usually produce a binary output, but instead some f (X) 2 [0; 1] which might be seen as the \level of con dence" in success of the trace, X. This success score can be used to apply an ordering to executing strategies, allowing \smart" dynamic scheduling of strategies.

In particular, we evaluated (using the Keras [ 5 ] backend-agnostic neural network suite and the scikit-learn [ 22 ] utilities) 1. A simple neural network with one input for each datum in the trace and a single hidden layer. 2. A convolutional network [ 14 ] which performs a 1-dimensional convolutional pass along the time axis for each feature before the hidden layer. 3. A recurrent network [ 6 ], feeding the time series into a gated recurrent unit before processing.

Results for this classi cation task are shown in Figure 5. The consistent level of accuracy achieved is encouraging. Both of the more-advanced classi ers performed better than the simple neural network. However, the simple network was chosen for integration into Vampire for implementation simplicity, and for performance reasons | it is \good enough".

Method Simple neural network Convolutional network

Recurrent network

Intelligent scheduling for Vampire

We show that this abstract predictor can be used in a concrete implementation for the Vampire prover. In the modi ed prover, it is used to run several strategies from Vampire's portfolio in a modi ed scheduler: strategies self-report their own execution data to the supervisor process and halt for re-evaluation at regular intervals. When a strategy halts, the scheduler then decides whether to re-schedule the strategy for some more time, or to swap it out for a di erent strategy. The algorithm used is as follows, taking as input a set of strategies to run:

To embed the neural network into Vampire, we took the trained network weights from our Python-based experiments, and generated a C source le with these weights included as a large array. The neural network's architecture was then re-implemented manually in C++, using the network weights compiled into the new program. This approach had several advantages: while perhaps not as e cient as an architecture such as TensorFlow [ 1 ] (which may use graphics hardware to accelerate computations), our approach is reasonably e cient, but is also low-latency, does not incur any additional dependencies, and does not add signi cantly to program start-up time. 7

Experimental results

We evaluate whether our prediction results carry through to improved performance in Vampire.

Experimental setup We take all relevant problems for Vampire from TPTP 6.4.0 (17,281 problems in total) and run three variations of Vampire 4.2.1's CASC portfolio mode: { baseline was the standard portfolio mode { no-prediction uses the dynamic scheduling architecture without prediction.

This e ectively produces a round-robin scheduling of strategies. { prediction uses the trained neural network to predict whether a strategy will be successful as previously described.

The default 3GB memory limit and 300s time limit from the standard portfolio mode were kept but in addition each variation was run in a multicore setup using 4 cores to distribute strategies over.Experiments were run on the StarExec cluster [ 31 ] where each node contains an Intel Xeon 2.4GHz processor. Results Figure 6 illustrates the overall results by plotting the number of problems solved against time taken. Table 1 gives some raw numbers. In this table New refers to the number of problems solved by this variation that were not solved by baseline, Unique refers to the number of problems solved by this variation and not by the other two, and the average solution times are given for wall-clock and cpu-time with standard deviation.

Table 2 gives further statistics comparing the two scheduling variations with the baseline. For the purposes of this table we only compare the results on problems that both the given variation and baseline solve and where the di erence between solution times is greater than 1 second. This second part is important as it allows for small variations in solution times due to natural non-determinism2. 2 This allowance is often not made but it can heavily skew results. Without it all variations look almost identical as the cases where variations behave in the same way dominate. This does not indicate that the variations are not an improvement, Speedup is a multiplication factor (a speedup of 2 means a proof was found in half the time), similarly for slowdown. Better means that the given variation was faster, whereas worse means that the variation was slower.

Discussion An immediate observation is that the overall number of problems solved is slightly worse for the variations performing scheduling. An immediate explanation for this could be that the strategies in the portfolio mode might still be quite fragile i.e. their performance might be degrading with the small overhead of context-switching and additional memory contention. Further experiments could explore this by using more generic strategies with longer individual time limits (many strategies in CASC mode run for less than 1 second). However, the overall number of problems solved is still high enough to make the result useful. The new problems solved by the scheduling variations could also be attributed to this non-determinism, suggesting again that more e ort should be spent to provide a broader set of complementary strategies to choose from. We note that one explanation for this second e ect could have been if the strategy schedule but there are many cases where there is no di erence. The most likely explanation for this is that solutions are quick and no scheduling is required e.g. if the problem is solved during preprocessing. was longer than the time given and prediction moved a strategy into the allowed time. This is a behaviour we might expect for short time limits but for this experiment all strategies were run.

The average solution times are improved with the two variations and the variation using prediction achieves the best solution time on average. When looking at the more detailed results of Table 2 we see that in the majority of cases the prediction variant was faster than the baseline, which was not the case when no prediction was applied. Furthermore, the impact of getting it wrong was larger without prediction (i.e. the slowdown is bigger). 8

Conclusions and future work

The aim of these experiments was to improve Vampire's overall performance, if not in the number of total theorems proved, but in the average time taken to prove problems. This approach has been shown to produce a signi cant increase in speed without an excessive penalty in the number of problems solved.

There are several routes that could be explored in order to further improve performance. As well as improving predictor performance by use of more sophisticated data curation, processing, and machine-learning techniques, it may also be possible to improve the nave scheduling algorithm. Further research might include designing scheduling algorithms which keep predictions as up-to-date as possible, maximise processor utilisation, minimise memory usage/swapping, reduce context-switching overhead, or even minimise the number of required calls to the prediction algorithm.

This form of optimisation for Vampire is relatively novel: historically the aim of the team has been to prove as many theorems as possible, rather than to improve the speed of moderately-hard problem solving. As immediate impact, these developments may be useful in improving Vampire's performance in the new SLH division in the CASC competition, as well as improving the overall usability of ITP via quicker \hammer" results, such as those reported via Sledgehammer [ 21 ].

References

1. Mart n Abadi, Paul Barham, Jianmin Chen, Zhifeng Chen, Andy Davis, Je rey Dean , Matthieu Devin, Sanjay Ghemawat, Geo rey Irving, Michael Isard , et al. Tensor ow: A system for large-scale machine learning . In OSDI , volume 16 , pages 265 { 283 , 2016 .

2. L. Bachmair and H. Ganzinger . Resolution theorem proving . In A. Robinson and A . Voronkov, editors, Handbook of Automated Reasoning, volume I, chapter 2 , pages 19 { 99 . Elsevier Science , 2001 .

3. Clark Barrett , Cesare Tinelli , et al. The smt-lib standard: Version 2 .0.

4. James P Bridge , Sean B Holden, and Lawrence C Paulson. Machine learning for rst-order theorem proving . Journal of automated reasoning , 53 ( 2 ): 141 { 172 , 2014 .

5. Francois Chollet et al. Keras. https://keras.io, 2015 .

6. Junyoung Chung , Caglar Gulcehre, Kyunghyun Cho, and Yoshua Bengio . Gated feedback recurrent neural networks . In International Conference on Machine Learning , pages 2067 { 2075 , 2015 .

7. Morgan Deters, Andrew Reynolds, Tim King, Clark W. Barrett, and Cesare Tinelli . A tour of CVC4: how it works, and how to use it . In Formal Methods in ComputerAided Design, FMCAD 2014 , Lausanne, Switzerland, October 21-24 , 2014 , page 7 , 2014 .

8. H. Ganzinger and K. Korovin . New directions in instantiation-based theorem proving . In Proc. LICS'03 , pages 55 { 64 , 2003 .

9. Geo rey Irving, Christian Szegedy, Alexander A Alemi, Niklas Een, Francois Chollet, and Josef Urban . DeepMath | deep sequence models for premise selection . In Advances in Neural Information Processing Systems , pages 2235 { 2243 , 2016 .

10. Cezary Kaliszyk , Stephan Schulz, Josef Urban, and Jir Vyskocil . System description: Et 0 .1. In International Conference on Automated Deduction, pages 389 { 398 . Springer, 2015 .

11. Cezary Kaliszyk and Josef Urban . FEMaLeCoP: Fairly e cient machine learning connection prover . In Logic for Programming , Arti cial Intelligence, and Reasoning , pages 88 { 96 . Springer, 2015 .

12. K. Korovin . iProver { an instantiation-based theorem prover for rst-order logic (system description) . In A. Armando, P. Baumgartner , and G. Dowek, editors, Proceedings of the 4th International Joint Conference on Automated Reasoning, (IJCAR 2008 ), volume 5195 of Lecture Notes in Computer Science, pages 292 { 298 . Springer, 2008 .

13. Laura Kovacs and Andrei Voronkov . First-order theorem proving and Vampire . In International Conference on Computer Aided Veri cation, pages 1 { 35 . Springer, 2013 .

14. Alex Krizhevsky , Ilya Sutskever, and Geo rey E Hinton . Imagenet classi cation with deep convolutional neural networks . In Advances in neural information processing systems , pages 1097 { 1105 , 2012 .

15. Daniel Kuhlwein, Jasmin Christian Blanchette, Cezary Kaliszyk, and Josef Urban. MaSh: machine learning for sledgehammer . In International Conference on Interactive Theorem Proving , pages 35 { 50 . Springer, 2013 .

16. Daniel Kuhlwein, Stephan Schulz, and Josef Urban . E-MaLeS 1.1 . In International Conference on Automated Deduction, pages 407 { 413 . Springer, 2013 .

17. Daniel Kuhlwein, Stephan Schulz, and Josef Urban . E-MaLeS 1.1 . In International Conference on Automated Deduction, pages 407 { 413 . Springer, 2013 .

18. Daniel Kuhlwein and Josef Urban . Males: A framework for automatic tuning of automated theorem provers . Journal of Automated Reasoning , 55 ( 2 ): 91 { 116 , 2015 .

19. Sarah Loos , Geo rey Irving, Christian Szegedy, and Cezary Kaliszyk . Deep network guided proof search . arXiv preprint arXiv:1701.06972 , 2017 .

20. William McCune and Larry Wos . Otter | the CADE-13 competition incarnations . Journal of Automated Reasoning , 18 ( 2 ): 211 { 220 , 1997 .

21. Lawrence C Paulson and Jasmin Christian Blanchette . Three years of experience with sledgehammer, a practical link between automatic and interactive theorem provers . IWIL-2010 , 1, 2010 .

22. F. Pedregosa , G. Varoquaux , A. Gramfort , V. Michel , B. Thirion , O. Grisel , M. Blondel , P. Prettenhofer , R. Weiss , V. Dubourg , J. Vanderplas , A. Passos , D. Cournapeau , M. Brucher , M. Perrot , and E. Duchesnay . Scikit-learn: Machine learning in Python . Journal of Machine Learning Research , 12 : 2825 { 2830 , 2011 .

23. J Ross Quinlan . Learning e cient classi cation procedures and their application to chess end games . In Machine Learning , Volume I, pages 463 { 482 . Elsevier , 1983 .

24. Giles Reger and Martin Suda . Measuring progress to predict success: Can a good proof strategy be evolved ? AITP 2017 , 2017 .

25. Giles Reger , Martin Suda , and Andrei Voronkov . The challenges of evaluating a new feature in Vampire . In Vampire Workshop , pages 70 { 74 , 2014 .

26. Giles Reger , Martin Suda , and Andrei Voronkov . Playing with AVATAR . In P. Amy Felty and Aart Middeldorp, editors, Automated Deduction - CADE-25: 25th International Conference on Automated Deduction , Berlin, Germany, August 1-7 , 2015 , Proceedings, pages 399 { 415 , Cham , 2015 . Springer International Publishing.

27. Giles Reger , Martin Suda , and Andrei Voronkov . Finding nite models in multisorted rst-order logic . In Nadia Creignou and Daniel Le Berre, editors, Theory and Applications of Satis ability Testing { SAT 2016 : 19th International Conference, Bordeaux, France, July 5-8 , 2016 , Proceedings, pages 323 { 341 . Springer International Publishing, 2016 .

28. A. Riazanov and A. Voronkov . Limited resource strategy in resolution theorem proving . J. Symb. Comp. , 36 ( 1-2 ): 101 { 115 , 2003 .

29. David E Rumelhart, Geo rey E Hinton , and Ronald J Williams . Learning representations by back-propagating errors . nature , 323 ( 6088 ): 533 , 1986 .

30. Stephan Schulz . E | a brainiac theorem prover . AI Communications , 15 ( 2 , 3): 111 { 126 , 2002 .

31. Aaron Stump , Geo Sutcli e, and Cesare Tinelli. StarExec, a cross community logic solving service . https://www.starexec.org, 2012 .

32. G. Sutcli e. The TPTP problem library and associated infrastructure, from CNF to TH0 , TPTP v6.4.0. Journal of Automated Reasoning , 59 ( 4 ): 483 { 502 , 2017 .

33. Geo Sutcli e and Christian Suttner . The state of CASC . AI Communications , 19 ( 1 ): 35 { 48 , 2006 .

34. Johan AK Suykens and Joos Vandewalle. Least squares support vector machine classi ers . Neural processing letters , 9 ( 3 ): 293 { 300 , 1999 .

35. Josef Urban. MaLARea: a metasystem for automated reasoning in large theories . ESARLT , 257 , 2007 .

36. Josef Urban , Jir Vyskocil, and Petr Stepanek. MaLeCoP machine learning connection prover . In International Conference on Automated Reasoning with Analytic Tableaux and Related Methods , pages 263 { 277 . Springer, 2011 .

37. Andrei Voronkov . AVATAR: The architecture for rst-order theorem provers . In Armin Biere and Roderick Bloem , editors, Computer Aided Veri cation , volume 8559 of Lecture Notes in Computer Science, pages 696 { 710 . Springer International Publishing, 2014 .

38. Mingzhe Wang , Yihe Tang , Jian Wang , and Jia Deng . Premise selection for theorem proving by deep graph embedding . In Advances in Neural Information Processing Systems , pages 2783 { 2793 , 2017 .