Efficient Semantic Features for Automated Reasoning over Large Theories

1 Introduction: Reasoning in Large Theories

In the conclusion of his seminal paper on AI [Turing, 1950], Turing suggests two alternative ways how to eventually build learning (AI) machines: (i) focusing on an abstract activity like chess, and (ii) focusing on learning through physical senses. Both these paths have been followed with many successes, but so far without producing AI competitive in the most advanced application of human intelligence: scientific thinking. The approach we follow is to try to learn that from large bodies of computer-understandable scientific reasoning.

In the last decade, large corpora of complex mathematical (and scientific) knowledge and reasoning have been encoded

∗Supported by the Austrian Science Fund (FWF): P26201.

†Supported by NWO grant nr. 612.001.208.

‡Supported by the Czech Grant Agency, GACR P103/12/1994.

Jiˇr´ı Vyskoˇcil‡

Czech Technical University in Prague

in a fully computer-understandable form. In such encodings, the mathematical knowledge consisting of definitions, theorems, proofs and theories is explained in complete detail, allowing the computers to fully understand the semantics of such complicated objects and to verify correctness of the long reasoning chains with respect to the formal inference rules of the chosen logical framework (set theory, type theory, etc.).

Recent highlights of this development include the formal encoding and verification of two graduate textbooks leading to the proof of the Odd Order theorem ("every finite group of odd order is solvable") [Gonthier et al., 2013], the formal verification of the 300-page book leading the proof of the Kepler conjecture [Hales, 2012], and verification of the seL4 operating systemmicrokernel [Klein et al., 2010].

This means that larger and larger parts of mathematics and mathematical thinking can now be analyzed, explored, assisted, and further developed by computers in ways that are impossible in domains where complete semantics is missing. The computers can not only use inductive AI methods (such as learning) to extract ideas from the large corpora, but they can also combine them with deductive AI tools such as automated theorem provers (ATPs) to attempt formal proofs of new ideas, thus further growing the body of verified scientific knowledge (which can then again be further learned from, and so on ad infinitum). In fact, this has started to happen recently. Large formal corpora built in expressive logics of interactive theorem provers (ITPs) such as Isabelle [Nipkow and Klein, 2014], Mizar [Grabowski et al., 2010] and HOL Light [Harrison, 1996] have been translated to first-order logic, and ATPs such as Vampire [Kov´acs and Voronkov, 2013], E [Schulz, 2002] and Z3 [de Moura and Bjørner, 2008] are used to prove more and more complicated lemmas in the large theories.

Since existing ATP calculi perform poorly when given thousands to millions of facts, a crucial component that makes such ATP assistance practical are heuristic and learning AI methods that select a small number of most relevant facts for proving a given lemma [K¨uhlwein et al., 2012]. This means that we want to characterize all statements in the knowledge bases by mathematically relevant features that will to a large extent allow to pre-compute the most promising combinations of formulas for proving a given conjecture. In some sense, we are thus trying to make a high-level approximation of the proof-search problem, and to restrict the fragile local decisions taken by the underlying ATP search by such high-level knowledge about what makes sense globally and what is likely a blind alley. 1 The question is how to design efficient features that will make such global approximative methods as good as possible. This is the subject of this paper.

Contributions

1. Semantic features for characterizing mathematical statements. We propose matching, abstraction and unification features and their combinations as a suitable means for characterizing statements in large mathematical corpora written in expressive logical frameworks (Section 4).
2. Fast semantic feature-extraction mechanisms. The crucial idea making the use of semantic features feasible is that such features often correspond to the nodes of fast deductiveAI data-structures such as substitution trees and discrimination nets. We implement and optimize such feature extraction mechanisms and demonstrate that they scale very well even on the largest formal corpora, achieving extraction times below 100 seconds for over hundred thousand formulas (Sections 5 and 6).
3. Improved Premise-Selection Performance. We evaluate the performance of the semantic features when selecting suitable premises for proofs and compare them to the old features using standard machine-learning metrics such as Recall, Precision, AUC, etc. The newly proposed features improve the average predicted rank of a mathematical statement needed for a proof by 22% in comparison with the best old features.
4. Improved Theorem-Proving Performance. We compare the overall performance of the whole featurecharacterization/learning/theorem-proving stack for the new and old features and their combinations. The improved machine-learning performance translates to 8% more theorems proved automatically over the standard MPTP2078 large-theory benchmark, getting close to the ATP performance obtained by using human-selected facts (Section 7).

2 The Large-Theory Setting: Premise Selection and Learning from Proofs

The object of our interest is a large mathematical corpus, understood as a set Γ of formally stated theorems, each with zero or more proofs. 2 Examples of such corpora are the Mizar Mathematical Library (MML), 3 the Isabelle Archive of Formal Proofs (AFP), 4 and the Flyspeck (Formal Proof of the Kepler Conjecture) development 5 done in HOL Light. Such large corpora contain tens to hundreds of thousands of proved statements. To be able to do many ATP experiments, 6 smaller benchmarks have been defined as meaningful subsets of the large corpora. Here we rely on the MPTP2078 benchmark [Alama et al., 2014] used in the 2012 CASC@Turing ATP competition [Sutcliffe, 2013] of the Alan Turing Centenary Conference. 7

1 Obviously, when developed, such guiding methods can be also tried directly inside the ATP calculi. See for example the hints method [Veroff, 1996], a similar work done for E [Schulz, 2000], and the MaLeCoP system [Urban et al., 2011].

2 We treat axioms and definitions as theorems with empty proof. In general, a theorem can have several alternative proofs.

3 http://mizar.org/

4 http://afp.sourceforge.net/

5 https://code.google.com/p/flyspeck/

6 A large number of ATP experiments is expensive. The ATPs are usually run with time limits between 1 second and 300 seconds.

In this setting, the task that we are interested in is to automatically prove a new conjecture given all the available theorems. Because the performance of existing ATP methods degrades considerably [Urban et al., 2010; Hoder and Voronkov, 2011] when given large numbers of redundant axioms, our research problem is to estimate the facts that are most likely to be useful in the final proof. Following [Alama et al., 2014] we define:

Definition 1 (Premise selection problem). Given an ATP A, a corpus Γ and a conjecture c, predict those facts from Γ that are likely to be useful when A searches for a proof of c.

The currently strongest premise selection methods use machine learning on the proofs of theorems in the corpus, such as naive Bayes, distance-weighted k-nearest neighbor, kernel methods, and basic ensemble methods [K¨uhlwein et al., 2012; K¨uhlwein et al., 2013; Kaliszyk and Urban, 2013b; 2013a; 2014]. It is possible that a particular fact is useful during a proof search without being used in the final formal proof object. Such cases are however rare and hard to detect efficiently. Therefore the relation of being useful during the proof search is usually approximated by being used in the final proof. Additionally, the learning setting is usually simplified by choosing at most one ("best") proof for each theorem c [Kuehlwein and Urban, 2013], and representing the proof of c as a set of theorems P(c) used in the proof. The query and update speed is important: in the ITP setting there are a number of alternative (usually less automated) theoremproving techniques that can be used if full automation is weak or slow. Likewise, the learning systems should quickly digest and adapt to new theorems and proofs. The overall largetheory setting is shown in Figure 1.

7 http://www.turing100.manchester.ac.uk/

Assuming a method F for extracting mathematically relevant features characterizing the theorems, this setting leads to the following multi-label learning task: Each proved theorem c ∈ Γ produces a training example consisting of F(c) and P(c), i.e., given the features F(c) we want the trained predictor to recommend the labels P(c) . The learning methods mentioned above are typically used as rankers: given the features of a new conjecture c, the highest ranked (using heuristically determined thresholds) labels for F(c) are given to an ATP, which then attempts a proof. To maximize the ATP performance, usually a portfolio of several most complementary learning methods, feature characterizations and ranking thresholds is used, and the (typically exponentially behaving) ATP is run in a strategy-scheduling mode [Tammet, 1997], i.e., with several shorter time limits over such complementary predictions rather than using the whole time limit for the most promising method.

3 Previously Introduced Features

The most commonly used features for characterizing mathematical statements in large theories are just their symbols [Hoder and Voronkov, 2011; Meng and Paulson, 2009]. In addition to that, large-theory ATP systems like HOL(y)Hammer [Kaliszyk and Urban, 2014], Sledgehammer [K¨uhlwein et al., 2013] and MaLARea [Urban et al., 2008] have so far used features that represent:

• Types, i.e., type constants, type constructors, and type classes [Kaliszyk and Urban, 2014]
• Termwalks of length 2 [K¨uhlwein et al., 2013]
• Subterms [Urban et al., 2008]
• Validity in a pool of finite models [Urban et al., 2008]
• Meta-information such as the theory name and presence in various databases [K¨uhlwein et al., 2013]

The normalizations for term and type variables that have been tried so far include:

• Replacing variables by their (variable-normalized) types [Kaliszyk and Urban, 2014]
• Using de Bruijn indices [Urban et al., 2008]
• Renaming all variables to a unique common variable [Urban et al., 2008]
• Using the original variable names (this is useful when the same variable names are used for similar purposes)

Except from validity in finite models, all these features can be extracted in a linear time and are thus easy to use. Since their distribution may be quite uneven, normalizing them by methods like TF-IDF 8 is relatively important before handing them over to fast-but-simple learners such as distance-weighted k-NN (used here for evaluation). Since the MPTP2078 is untyped and already comes with variables renamed to de Bruijn indices, we do not use the type enhancements and original variable names here. Validity in a large pool of finite models requires finding a diverse set of models in which the formulas are then evaluated. Even though such features may approximate the semantics really well, they are in general much more expensive to compute than the rest, and for that reason we also avoid them here.

8 Readers might wonder about latent semantics [Deerwester et al., 1990]. So far this does not raise the performance significantly.

4 New Semantic Features for Reasoning

A formal proof is usually defined as a sequence (resp. DAG) of formulas where each of them is either an axiom or is derived from earlier formulas (resp. DAG parents) by an application of an inference rule. In various ITP and ATP systems such inference rules differ, however a crucial and very frequent idiom of (not just) mathematical reasoning is the rule of Universal Instantiation, allowing to instantiate a general statement in a concrete context.

Scenario 1. To give the first simple example, the commutativity of addition (CA): X + Y = Y + X may be applied to prove that (L1): 1 + 2 = 2 + 1 , by matching 1 with X and 2 with Y . Assume that somebody already proved 1 + 2 = 2 + 1 by referring to X + Y = Y + X, and a new conjecture to prove is (L2): 3 + 7 = 7 + 3. When using only the features introduced previously (see Section 3), the feature overlap between these two instances will be the same as with (L3): 5 + 8 = 4 + 9 (which might have been proved very differently). In other words, none of the features captures the fact that L1 and L2 are closer to each other in the instantiation lattice than to L3, and thus have a higher chance of sharing a common proof pattern.

A complete way how to remedy this would be to use all (variable-normalized) generalizations of a term as its features. However, the lattice of all generalizations of a term is typically exponentially large wrt. the size of the term (see Figure 2). Fortunately, in this simple scenario, we can replace such full enumeration of generalizations of a given term t with a much smaller set: the set GenΓ(t) of all terms in our corpus Γ that generalize t. Indeed, since CA was used to prove L1, it must be in the corpus Γ. Therefore CA itself is in GenΓ(L1) and also in GenΓ(L2), introducing a new common matching feature for L1 and L2, but not for L3. Extraction of all such matching features for large corpora can be efficiently implemented using ATP indexing datastructures called discrimination trees (DTΓ), which we briefly discuss in Section 5.

Scenario 2. Now imagine a more complicated (but still quite common) case: L1 is in the corpus, but has a more complicated proof, and CA is not in the corpus (yet). For example, 1 and 2 are defined as von Neuman ordinals, where addition is the standard ordinal addition which is not commutative in general. Since CA is not in Γ, it is neither in its discrimination tree, and L1 and L2 will not get the common matching feature corresponding to CA. But it is still quite likely that the proof of L1 is relevant also for proving L2: if we are lucky, the proof is sufficiently general and actually derives the commutativity of ordinal addition for finite ordinals behind the scenes. This means that quite often the common matching feature is still interesting, even if not explicitly present in Γ.

One might again first try to use brute force and attempt to generate all common generalizations for all pairs of terms in Γ. Again, see Figure 2 for an example when such lattice is exponentially large. It is however no longer possible to rely just on the terms that already are in Γ as in the previous case, and some method for generating some common matching features seems needed in this case. We have proposed and implemented two kinds of heuristic solutions. The first inserts for each term t a small number of more general terms into DTΓ, typically by generalizing the term only linearlymany times, see Section 5 for details. Some of such generalization methods actually corresponds to the internal nodes of DTΓ. The second solution collects such (differently optimized) generalization nodes explicitly, using another kind of efficient ATP indexing datastructure called substitution tree (STΓ), described in more detail in Section 6 (see Figure 4). This means that just by building STΓ, we naturally obtain for each term t in Γ a set of (some) generalizing features of t: the set ST Anc Γ (t) of the ancestors of t in STΓ. Even the substitution tree however cannot (reasonably) guarantee that every two terms in Γ have there their least general generalization (lgg). Such requirement would again result in exponential size for examples such as Figure 2.

Scenario 3. Finally, what substitution trees can guarantee (and are usually used for in ATP) is efficient retrieval of all unifying terms. The easiest semantic motivation for collecting such features comes from the resolution rule, which is the basis of many ATP procedures. Given formulas p(X, a) and p(a,X) =⇒ False, the resolution rule derives False by unifying p(X, a) and p(a,X). Note that the two unifying literals do not match in any direction, however they will always have a nontrivial lgg.

5 Discrimination Trees for Matching and Generalization Features

Selection of candidate clause-heads that unify, match, or subsume a given goal is a central operation in automated deduction. In order to perform such selection efficiently, all major theorem provers use term indexing techniques [Robinson and Voronkov, 2001]. Discrimination trees, as first implemented by [Greenbaum, 1986], index terms in a trie, which keeps single path-strings at each of the indexed terms (Figure 3 taken from [Robinson and Voronkov, 2001]). A discrimination tree can be constructed efficiently, by inserting each term in the traversal preorder. Since discrimination trees are based on path indexing, retrieval of generalizations is straightforward, but retrieval of unifiable terms is more involved.

To address Scenario 1, we create a discrimination net with all the available terms in the corpus inserted in the net. Efficient implementation is needed, since the largest mathematical corpora contain millions of terms. The result of a lookup then corresponds to first order matching. This means that all terms in the corpus that are more general than the queried one are returned. In order to extend this to generalizations that are shared between terms, but not yet in the net (Scenario 2), we do heuristic generalizations. This consists of selecting a subterm of the term and replacing it by a variable. We consider several strategies for selecting the subterms to generalize:

• repeated right-most inner-most
• repeated left-most inner-most
• all positions
• combinations of above (quadratic in the size of the term), including combination of the previous one with itself.

To avoid redundant generation of generalizations of terms that are already in the net, the generation of subterms and their right-most inner-most generalizations is done together. We first iterate over the term top-down, and for each subterm level we try to insert its generalizations iteratively. If a particular generalization is already present in the net, we do not compute any further generalizations, but instead proceed to the next subterm. This optimization brings the sum of feature extraction times for all formulas below 100s for the largest formal mathematical corpus available (MML1147) containing millions of terms, see Section 7 (Table 2).

6 Substitution Trees for Unification and Generalization Features

Substitution trees [Graf, 1995] are a term indexing technique which is based on unifiability checking, rather than simple equality tests. In order to do so, substitution trees keep substitutions in the nodes. This allows for substitution trees to be smaller than other indexing techniques. Since the traversal order is not fixed, substitution trees need to compute the common generalizations of terms during insertion.

Our implementation is using the so called linear substitution trees in the same way as described in [Graf, 1996; Robinson and Voronkov, 2001]. The retrieval from a substitution tree may require more backtracking steps than in other indexing techniques, but the retrieval of unifiable terms is straightforward: it amounts to following all the paths that contain substitutions compatible with the given term. This is simpler than for example implementing unification on discrimination trees [Hoder and Voronkov, 2009].

To get interesting generalizations as features of a term t that is already inserted in the tree, we extract a path from the root to the leaf. Each node on such path represents generalization of the term t (Figure 4).

7 Experimental Analysis

Benchmark Data and Evaluation Scenario

The MPTP2078 benchmark consists of 2078 related largetheory problems (conjectures) extracted from the Mizar library. These problems contain 4494 unique formulas used as conjectures and axioms. The formulas and problems have a natural linear ordering derived from their (chronological) order of appearance in the Mizar library. As usual in such large-theory evaluations [Kaliszyk and Urban, 2014], we emulate the scenario of using AI/ATP assistance in interactive theorem proving: For each conjecture C we assume that all formulas stated earlier in the development can be used to prove C. This scenario results in large ATP problems that have 1877 axioms on average. Such problems are typically difficult to solve without techniques for pre-selection of the most relevant axioms (cf. Table 4).

For each conjecture C we also use its ITP (human-written) proof to extract only the premises needed for the ITP proof of C, i.e., P(C). 9 This proof information is used in three ways:

9 In general, we can also use ATP proofs of the previous theorems

(i) to train the machine learners on all previous proofs for each conjecture C, (ii) to compare the premises predicted by such trained machine learners with the actual proof premises P(C), and (iii) to construct the small ATP problem for C, which (unlike the large version) contains as axioms only the (few) premises P(C) - and in this way, the ATP is very significantly advised by the human author of the ITP proof.

Speed and Machine-Learning Performance

The features that we evaluate are summarized in Table 1. We limit the evaluation to two fast learning methods: distanceweighted k-NN and naive Bayes, however the latter performs significantly worse. Table 2 shows the numbers of features obtained on MPTP2078, the feature-extraction and learning speeds on such MPTP2078 features. To see how the feature extraction process scales, we have also tested the methods on the whole MML library (version 1147) containing 146500 formulas. Note that practically all the extraction methods scale well to this corpus (we did not run UNI, due to its size), typically taking less than 100 seconds to process the whole corpus. This means that computing the features of a new conjecture which is being proved over the (already memoryloaded) corpus will take only miliseconds. Such times are negligible in comparison with standard ATP times (seconds).

Table 3 shows the standard machine learning (k-NN) evaluation, comparing the actual (needed) ITP proof premises of each conjecture C (i.e., P (C)) with the predictions of the machine learners trained on all ITP proofs preceding C. The average rank of a needed premise on MPTP2078 decreases from 53.03 with the best old feature method TRM0 (formulas characterized by all their subterms with all variables renamed to just one) to 43.43 with the best new method MAT∅ (using the set of all matching terms as features, without any generalizations). This is a large improvement of the standard machinelearning prediction: thanks to better features, the ranking of needed premises is improved by 22.1%. The best combination of features (SYM|TRM0|MAT∅|ABS) improves this to 41.97. This is a big difference for the ATP search, evaluated next.

alongside with their ITP proofs for the learning, however we will not complicate the evaluation setting here.

Evaluation of the Theorem-Proving Performance

First we measure the performance of unaided ATPs running for 60 seconds on the large and small versions of the problems, see Table 4. While Vampire outperforms E, particularly on the large problems, we choose E for the complete evaluation which includes premise selection, because the machine learning advice will not interact with the SInE selection heuristics [Hoder and Voronkov, 2011] used by Vampire very frequently on the large problems.

The complete evaluation then proceeds as follows. For each of the best new and old premise-selection methods we create six versions of ATP problems, by taking the topranking segments of 8, 16, 32, 64, 128, and 256 predicted premises, and we run E on such problems for 10 seconds. Each problem thus takes again at most 60 seconds altogether, allowing us to compare the results also with the 60-second unaided ATP runs on the large and small problems. Table 5 then compares the ATP performance (measured as a union of the six slices), also adding the best-performing combination of the old and new features. The best new method MAT∅ solves 80 problems (8%) more than the best old method TRM0, and the best-performing combination solves 103 (10%) problems more. This is getting close to the performance of E on the human-advised premises (1210 in Table 4). The behaviour of the ATP with respect to the number of premises used is depicted in Figure 5, showing even higher improvements.

8 Conclusion

We have shown that even when dealing with the largest formal corpora, one can have efficient features that encode important semantic relations and thus make the selection of relevant knowledge much more precise. The newly introduced semantic features significantly improve selection of relevant knowledge from large formal mathematical corpora.

This improvement is 22% in terms of the average predicted rank, while the combination of the new and old features helps to increase the intelligence of the advising algorithms to a level that is nearly equal to that of the human formalizers when comparing the final ATP performance. In particular, the best new method MAT∅ proves 8% more theorems automatically than the best old method. The cost of manually producing these proofs is very high: The Flyspeck project took about 25 person-years and the Mizar library about 100-150 person-years. So the reported improvements just for these two corpora translate to 2 and 8-12 person-years respectively.

There is a large number of directions for future work, including employing such semantic features also for internal guidance in systems like MaLeCoP and in resolution/superposition ATPs, re-using their efficient termindexing datastructures.