Automatic Learning in Proof Planning

Mateja Jamnik

Manfred Kerber

Martin Pollet

ABSTRACT

In this paper we present a framework for automated learning within mathematical reasoning systems. In particular, this framework enables proof planning systems to automatically learn new proof methods from well chosen examples of proofs which use a similar reasoning pattern to prove related theorems. Our framework consists of a representation formalism for methods and a machine learning technique which can learn methods using this representation formalism. We present the implementation of this framework within the Omega proof planning system, and some experiments we ran on this implementation to evaluate the validity of our approach.

1.  Introduction

Proof planning [pub349] is an approach to theorem proving which uses proof methods rather than low level logical inference rules to find a proof of a theorem at hand. A proof method specifies a general reasoning pattern that can be used in a proof, and typically represents a number of individual inference rules. For example, mathematical induction can be encoded as a proof method. Proof planners search for a proof plan of a theorem which consists of applications of several methods. An object level logical proof may be generated from a successful proof plan. Proof planning is a powerful technique because it often dramatically reduces the search space, since the search is done on the level of abstract methods rather than on the level of several inference rules that make up a method. Therefore, typically, there are fewer methods than inference rules explored in the search space. Proof planning also allows reuse of proof methods, and moreover generates proofs where the reasoning strategies of proofs are transparent, so they may have an intuitive appeal to a human mathematician. Indeed, the communication of proofs amongst mathematicians can be viewed to be on the level of proof plans.

One of the ways to extend the power of a proof planning system is to enlarge the set of available proof methods. This is particularly beneficial when a class of theorems can be proved in a similar way, hence a new proof method can encapsulate the general reasoning pattern of a proof for such theorems. A proof method in proof planning basically consists of a triple - preconditions, postconditions and a tactic. A tactic is a program which given that the preconditions are satisfied transforms an expression representing a subgoal in a way that the postconditions are satisfied by the transformed subgoal. If no method on an appropriate level is available in a given planning state, then a number of lower level methods (with inference rules as the lowest level methods) have to be applied in order to prove a given theorem. Alternatively, a new method can be added by the developer of a system. However, this is a very knowledge intensive task and hence, presents a difficulty in applying a proof strategy to many domains.

In this work, we show how a system can learn new methods automatically given a typically small number of well chosen examples of related proofs of theorems. This is a significant improvement, since examples (e.g., in the form of classroom example proofs) exist typically in abundance, while the extraction of methods from these examples can be considered as a major bottleneck of the proof planning methodology.

The idea is that the system starts with learning simple proof methods. As the database of available proof methods grows, the system can learn more complex proof methods. Inference rules can be treated as methods by assigning to them pre- and postconditions. Thus, from the learning perspective we can have a unified view of inference rules and methods as given sequences of primitives from which the system is learning a pattern. We will refer to all the existing methods available for the construction of proofs as primitive methods. As new methods are learnt from primitive methods, these too become primitive methods from which yet more new methods can be learnt. Clearly, there is a trade-off between the increased search space due to a larger number of methods, and increasingly better directed search possibilities for subproofs covered by the learnt methods. Namely, on the one hand, if there are more methods, then the search space is potentially larger. On the other hand, the organisation of a planning search space can be arranged so that the newly learnt, more complex methods are searched for first. If a learnt method is found to be applicable, then instead of a number of planning steps (that correspond to the lower level methods encapsulated by the learnt method), a proof planner needs to make one step only. Generally, proof plans consisting of higher level methods will be shorter than their corresponding plans that consist of lower level methods. Hence, the search for a complete proof plan is shallower, but also bushier. In order to measure this trade-off between the increased search space and better directed search, an empirical study is carried out in the second part of this paper.

Here, we present a hybrid proof planning system Learnomatic, which uses the existing proof planner Omega [omega], and combines it with our own machine learning system. This enhances the Omega system by providing it with the learnt methods that Omega can use in proving new theorems.

Automatic learning by reasoning systems is a difficult and ambitious problem. Our work demonstrates one way of starting to address this problem, and by doing so, it presents several contributions to the field. First, although machine learning techniques have been around for a while, they have been relatively little used in reasoning systems. Making a reasoning system learn proving strategies from examples, much like children learn to solve problems from examples demonstrated to them by the teacher, is hard. Our work makes an important step in a specialised domain towards a proof planning system that can reason and learn.

Second, proof methods have complex structures, and are hence very hard to learn by the existing machine learning techniques. We approach this problem by abstracting as much information from the proof method representation as needed, so that the machine learning techniques can tackle it. Later, after the reasoning pattern is learnt, the abstracted information is restored as much as possible.

Third, unlike in some of the existing related work [fuchs98,schulz00], we are not aiming to improve ways of directing proof search within a fixed set of primitives. In theorem proving systems these primitives are typically inference steps or tactics, and in proof planning systems these primitives are typically proof methods. Rather, we aim to learn the primitives themselves, and hence improve the framework and reduce the search within the proof planning environment. Namely, instead of searching amongst numerous low level proof methods, a proof planner can now search for a newly learnt proof method which encapsulates several of these low level primitive methods.

1.1.  Running Example

1. closed-under(Z₃,(lambda x lambda y. x (xy)))
2. associative-under(Z₃,(lambda x lambda y. (x y)))
3. commutative-under(Z₂,(lambda x lambda y.(xy)))

The aim of our work is to learn and generalise such patterns into proof methods that can then be used for proofs of other related theorems. We now show how this learning is done automatically within our framework.

2.  Learning

The methods we aim to learn are complex and beyond the complexity that can typically be tackled in the field of machine learning. Thus, we first simplify the problem and aim to learn so-called method outlines. For this purpose we use a simple representation formalism which abstracts away as much information as possible for the learning process, which is described next. Second, we restore the necessary information as much as possible so that the proof planner can use the newly learnt method using the mechanism described in Section 3.Some information may be irrecoverably lost. In this case, some extra search in the application of the newly learnt methods will typically be necessary.

Let us define the following language L, where P is a set of known identifiers of primitive methods used in a method that is being learnt:

• for any p in P, let p in L,
• for any l₁,l₂ in L, let [l₁,l₂] in L,
• for any l₁,l₂ in L, let [l₁|l₂] in L,
• for any l in L, let l^* in L,
• for any l in L and n in N, let lⁿ in L,
• for any list such that all l_i in list are also l_i in L, let T(list) in L.

2.1.  Learning Technique

Our learning technique considers some typically small number of positive examples which are represented in terms of sequences of identifiers for primitive methods, and generalises them so that the learnt pattern is in language L. The pattern is of smallest size with respect to a defined heuristic measure of size [jkpb02-tr], which essentially counts the number of primitives in an expression. The intuition for it is that a good generalisation is one that reduces the sequences of method identifiers to the smallest number of primitives (e.g., [a²] is better than [a,a]). The pattern is also most specific (or equivalently, least general) with respect to the definition of specificity spec. spec is measured in terms of the number of nestings for each part of the generalisation [jkpb02-tr]. Again, this is a heuristic measure. The intuition for this measure is that we give nested generalisations a priority since they are more specific and hence less likely to over-generalise.

We take both, the size (first) and the specificity (second), in account when selecting the appropriate generalisation. If the generalisations considered have the same rating according to the two measures, then we return all of them. For example, consider two possible generalisations constructed by the learning algorithm described below: [[a²]^*] and [a^*]. According to size, size([[a²]^*])= 1 and size([a^*])=1. However, according to specificity, spec([[a²]^*])= 2 and spec([a^*])=1. Hence, the algorithm selects [[a²]^*].

Here is the learning algorithm. Given some number of examples (e.g., e₁=[a,a,a,a,b,c] and e₂=[a,a,a,b,c]):

1. For every example e_i, split it into sublists of all possible lengths plus the rest of the list. We get a list of pattern lists pl_i, each of which containing patterns p_i.Notice that there are n mod m ways of splitting an example of length n into different sublists of length m. Namely, the sublists of length m can start in positions 1, 2,... , n mod m. E.g.:
   for e₁: {[[a],[a],[a],[a],[b],[c]], [[a,a],[a,a],[b,c]], [[a],[a,a], [a,b],[c]], [[a,a,a], [a,b,c]], [[a],[a,a,a], [b,c]],... }
   for e₂: {[[a],[a],[a],[b],[c]],[[a,a],[a,b],[c]], [[a], [a,a],[b,c]], [[a,a,a],[b,c]], [[a],[a,a,b],[c]],... }
2. If there is any branching in the examples, then recursively repeat this algorithm on every element of the list of branches.
3. For every example e_i and for every pattern list pl_i find sequential repetitions of the same patterns p_i in the same example. Using an exponent denoting the number of repetitions, compress them into p_i^c and hence pl_i^c. E.g.:
   pl₁^c ={[[a]⁴,[b],[c]], [[[a,a]²],[b,c]],... }
   pl₂^c={[[a]³,[b],[c]], [[a],[a,a],[b,c]],... }
4. For every compressed pattern p_i^c in pl_i^c of every example e_i, compare it with p_j^c in all other examples e_j, and find matching p^c (called m_i) with the same constituent pattern, which may occur a different number of times. E.g.:
   m₁=(pl₁^c1,pl₂^c1) due to [a]⁴ and [a]³
   m₂=(pl₁^c2,pl₂^c2), due to [b,c] and [b,c], etc.
5. If there are no matches m_i in the previous step, then generalise the examples by joining them disjunctively using the "|" constructor.
6. For every p_i^c in a matching, generalise different exponents to a "*" constructor, and the same exponents n to a constant n. E.g.:Notice that here is a point where our generalisation technique can over-generalise, namely when there is a pattern in the exponents - like prime number - this is ignored and just a * is selected.
   for m₁: [a]⁴ and [a]³ are generalised to [a]^*;
   for m₂: [b,c] and [b,c] are generalised to [b,c]
7. For every p_g of a match, transform the rest of the pattern list on the left and on the right of p_g back to the example list, and recursively repeat the algorithm on them. E.g.:
   for m₁ in e₁: LHS=[], p_g=[a]^*, repeat on RHS=[b,c]
   for m₁ in e₂: LHS=[], p_g=[a]^*, repeat on RHS=[b,c]
   for m₂ in e₁: repeat on LHS=[a,a,a,a], p_g=[b,c], RHS=[]
   for m₂ in e₂: repeat on LHS=[a,a,a], p_g=[b,c], RHS=[].
8. Repeat recursively this algorithm on all possible generalisations inside the method outline (i.e., "*", exponent n, "|" and ",") in order to find nested generalisations (such as [[a]²]^*). Terminate, when no success.
9. If there is more than one generalisation remaining at the end of the recursive steps, then pick the ones with the smallest size and among these the ones with the largest specificity. Else, the examples cannot be generalised. E.g.: for the examples above, not applicable yet; after the algorithm is repeated on the rest of our examples, the learnt method outline will be [[a]^*,[b,c]].

The learning algorithm was implemented in Standard ML v.110. Its input are the sequences of proofs constructed in Omega . Its output are method outlines which are passed back to Omega . The algorithm was tested on several examples of proofs and it successfully produced the required method outlines.

In particular, for our example of the residue class theorems above, the sequences of methods identifiers from the proofs of these theorems are as follows:

1. {defn-exp, FORALL_i-sort,FORALL_i-sort, convert-resclass-to-num, defn-exp, or-e-rec, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp}
2. {defn-exp, FORALL_i-sort,FORALL_i-sort, FORALL_i-sort,convert-resclass-to-num, or-e-rec, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp}
3. {defn-exp, FORALL_i-sort,FORALL_i-sort, convert-resclass-to-num, or-e-rec, simp-num-exp, simp-num-exp, simp-num-exp, simp-num-exp}

Due to lack of space the reader is referred for the discussion of some properties of our learning algorithm to [jkpb02-tr]. There are some disadvantages to our technique, mostly related to the run time speed of the algorithm relative to the length of the examples considered for learning. The algorithm can deal with relatively small examples, which we encounter in our application domain, in an optimal way. The complexity of the algorithm is exponential in the worst case. Hence, we use some heuristics for large and badly behaved examples [jkpb02-tr].

3.  Using learnt methods

Method outlines that have been learnt so far do not contain all the information which is needed for the proof planner to use them. For instance, they do not specify what the pre- and postconditions of methods are, they also do not specify how the number of loop applications of methods is instantiated when used to prove a theorem. Hence, we need to restore the missing information.

For each learnt outline we automatically create a method for which its precondition is fulfilled if there is a sequence of methods that is an instantiation of the method outline, and each method of the sequence is applicable. The postcondition introduces the new open goals and hypotheses resulting from applying the methods of the sequence to the current goal. We will call this kind of method a learnt method.

Since methods in Omega may be very complex, the precondition of a learnt method cannot be extracted from the pre- and postconditions of the uninstantiated methods in the method outline. Hence, we actually have to apply a method to produce a proof situation for which we can test the preconditions of the subsequent method in the method outline. That is, we have to perform proof planning guided by the learnt outline.

The precondition test performs a depth first search on the learnt method outline. Besides the choice points of the learnt method, i.e., disjunctions and number of repetitions for "*", we also have to decide to which open goal every single method in the method outline should be applied. Additionally, for methods containing parameters an instantiation has to be chosen. More details on the application test and on the learnt method reuse can be found in [jkpb02-tr].

4.  Evaluation - experiments

In order to evaluate the success of our approach, we carried out an empirical study in different problem domains on a number of theorems. This test set includes the theorems from which new methods were learnt, but most of them are new and more complex. In particular, we tested our framework on examples of residue classes (e.g., like our running examples), set theoryHere are a set theory theorem and a non-theorem: FORALL x,y,z . ((x union y) intersection z) = (x intersection z) union (y intersection z) and FORALL x,y,z . (x union y) intersection z) = (x union z) intersection (y union z). and group theory.Here are some group theory examples: a o (((a^-1 o b) o (c o d)) o f) = (b o (c o d)) o f and (c o (b o (a^-1 o (a o b^-1)))) o (((d o a) o a^-1) o f) = c o (d o f). The aim of these experiments was to investigate if the proof planner Omega enhanced with the learnt methods, can perform better than the standard Omega planner.There are several reasons for comparing the performance of Omega with and without a learning capability, rather than with the performance of other learning reasoning systems. First, there are only few proof planners around. In the future, we plan to apply our learning approach to lambda-Clam proof planner in order to assess the benefits of our approach in other systems. Second, as discussed in Section 5, little work has been done on applying machine learning techniques to automated theorem provers, hence a direct comparison with another approach is infeasible. The learnt methods were added to the search space in a way that their applicability is checked first, before the existing standard methods.

The measures that we consider are: coverage - the ability to prove new theorems with the help of learnt methods; timing - the time it takes to prove a theorem; proof length - the number of steps in the proof plan; and matchings - the number of all true and false attempts to match candidate methods. Checking the candidate methods that may be applied in the proof, i.e., matchings, is by far the most expensive part of the proof search, and is hence the best measure to indicate the validity of our approach.

Table 1 compares the values of matchings and proof length for the three problem domains.Note that assoc-z3z-times and closed-z3z-plusplus in Table 1 are our second and first running example, respectively. It compares the values for these measures when the planner searches for the proof with the standard set of available methods (column marked with S), and when in addition to these, there are also our newly learnt methods available to the planner (column marked with L). "--" means that the planner ran out of resources (four hours of CPU time) and could not find a proof plan.

4.1.  Residue class domain:

The next two theorems (about the closed property) and the average of all theorems of a similar type, can use the choose method. choose can only prove a subpart of a theorem, hence a number of other methods need to be used in addition to choose in order to prove the theorem. Hence, the proofs of this type are longer than the proofs of the former type (that use tryanderror), as is evident also from Table 1. As expected, the improvement in the number of matchings reflects this, and is a factor of two on average. In general, the more complicated the theorem, the better is the improvement made by the availability of the learnt methods.

4.2.  Set theory domain:

4.3.  Group theory domain:

It is evident from Table 1 that the number of matchings is improved, but it is only reduced by about 15%. We noticed that for some very simple theorems, a larger number of matchings is required if the learnt methods are available in the search space. However, for more complex examples, this is no longer the case, and an improvement is noticed. The reason for this behaviour is that additional methods increase the search space, so when there are only a few ways to apply methods in the case of simple theorems, this causes some overheads. In the case of complex examples, there are many more possible ways to apply methods, hence the presence of complex learnt methods causes small or no overheads, or in fact, a reduced number of matchings.

The success of our approach is also evident from the fact, that when our learnt methods are not available to the planner, then it cannot prove some complex theorems, i.e., the coverage of the system that uses learnt methods is increased. When trying to apply methods such as associativity left or right, for which the planner has no control knowledge about their application, it runs out of resources. Our learnt methods, however, provide control over the way the methods are applied in the proof, and enable a planner to generate a proof plan. Again, the proof length is reduced by using learnt methods, as expected.

On average, the time it took to prove theorems of reside classes with the newly learnt methods was up to 50% shorter than without such methods. For conjectures in set theory the proof search with learnt methods was about 15% shorter. The search in group theory took approximately 100% longer than without the learnt methods. The time results reflect in principle the behaviour of the proof search measured by method matchings, but also contain the overhead due to the current implementation for the reuse of the learnt methods (see Section 3). For example, the current proof situation is copied for the applicability test of the learnt method, and the new open goals and hypotheses resulting from a successful application are copied back into the original proof. This overhead could be reduced in later versions.

4.4.  Analysis:

In general, the coverage when using learnt methods is improved, which is also indicated by the fact that using learnt methods Omega can prove theorems that it can otherwise not prove.

The reason for the improvements described above is due to the fact that our learnt methods provide a structure according to which the existing methods can be applied, and hence they direct search. This structure also gives a better explanation why certain methods are best applied in particular combinations. For example, the simplification method for group theory examples indicates how the methods about associativity, inverse and identity should be combined together, rather than applied blindly in any possible combination.

5.  Related work

Our approach to learning methods is related to techniques for learning macro-operators, which was originally proposed for planning in artificial intelligence [ruby-kibler89,korf85]. But within theorem proving and proof planning related work is scarce. E.g., some work has been done on applying machine learning techniques to theorem proving, in particular on improving the proof search [fuchs98,schulz00]. However, not much work has concentrated on high level learning of structures of proofs and extending the reasoning primitives within an automated theorem prover.

Silver [pub220] and Desimone [pub321] used precondition analysis which learns new inference schemas by evaluating the pre- and postconditions of each inference step used in the proof. A dependency chart between these pre- and postconditions is created, and constitutes the pre- and postconditions of the newly learnt inference schema. These schemas are syntactically complete proof steps, whereas the Omega methods contain arbitrary function calls which cannot be determined by just evaluating the syntax of the inference steps.

Kolbe, Walter, Melis and Whittle have done related work on the use of analogy [pubmw] and proof reuse [kolbe-walther94,kolbe97]. Their systems require a lot of reasoning with one example to reconstruct the features which can then be used to prove a new example. The reconstruction effort needs to be spent in every new example for which the old proof is to be reused. In contrast, we use several examples to learn a reasoning pattern from them, and then with a simple application, without any reconstruction or additional reasoning, reuse the learnt proof method in any number of relevant theorems.

In terms of a learning mechanism, more recent work on learning regular expressions, grammar inference and sequence learning [sun-giles00] is related. Learning regular expressions is equivalent to learning finite state automata, which are also recognisers for regular grammars. Muggleton has done related work on grammatical inference methods [muggleton90]. The main difference to our work is that these techniques typically require a large number of examples in order to make a reliable generalisation, or supervision or an oracle which confirms when new examples are representative of the inferred generalisation. Furthermore, these techniques only learn sequences. However, our language is larger than regular grammars as it includes constant repetitions of expressions and expressions represented as trees.

Related is also the work on pattern matching in DNA sequences [brazma94], as in the GENOME project, and some ideas on our learning mechanism have been inspired by this work.

6.  Conclusion and future work

In this paper we described a hybrid system Learnomatic, which is based on the Omega proof planning system enhanced by automatic learning of new proof methods. This is an important advance in addressing such a difficult problem, since it makes first steps in the direction of enabling systems to better their own reasoning power. Proof methods can be either engineered or learnt. Engineering is expensive, since every single new method has to be freshly engineered. Hence, it is better to learn, whereby we have a general methodology that enables the system to automatically learn new methods. The hope is that ultimately, as the learning becomes more complex, the system will be able to find better or new proofs of theorems across a number of problem domains.

There are several limitations of our approach that could be improved in the future. Namely, the learning algorithm may overgeneralise, so we need to examine what are good heuristics for our generalisation and how suboptimal solutions can be improved. In particular, we want to address the question how to deal with noise in the examples. In order to reduce unnecessary steps, the preconditions of the learnt methods would ideally be stronger. Currently, we use an applicability test to search if the preconditions of the method outline are satisfied. In the future, preconditions should be learnt as well. Finally, in order to model the human learning capability in theorem proving more adequately it would be necessary to model how humans introduce new vocabulary for new (emerging) concepts.

A demonstration of Learnomatic implementation can be found on the following web page:

http://www.cs.bham.ac.uk/~mmk/demos/LearnOmatic/ Further information, also with links to papers with more comprehensive references can be found on http://www.cs.bham.ac.uk/~mmk/projects/MethodFormation/

6.1.   Acknowledgements

References

• [omega] C. Benzmüller, et al., ` Omega : Towards a mathematical assistant', in 14th Conference on Automated Deduction, ed., W. McCune, number 1249 in LNAI, pp. 252-255, (1997). Springer.

• [brazma94] A. Brazma, `Learning regular expressions by pattern matching', Technical Report TCU/CS/1994/1, Institute of Mathematics and Computer Science, University of Latvia, (1994).

• [pub349] A. Bundy, `The use of explicit plans to guide inductive proofs', in 9th Conference on Automated Deduction, eds., E. Lusk and R. Overbeek, number 310 in LNCS, pp. 111-120, (1988).

• [pub321] R.V. Desimone, `Learning control knowledge within an explanation-based learning framework', in Progress in Machine Learning - Proceedings of 2nd European Working Session on Learning, EWSL-87, eds., I. Bratko and N. Lavrac, (1987). Sigma Press.

• [fuchs98] M. Fuchs and M. Fuchs, `Feature-based learning of search-guiding heuristics for theorem proving', AI Comm., 11, 175-189, (1998).

• [jkpb02-tr] M. Jamnik, M. Kerber, M. Pollet, and C. Benzmüller, `Automatic learning of proof methods in proof planning', Technical Report CSRP-02-5, School of Computer Science, University of Birmingham, UK, (2002).

• [kolbe97] T. Kolbe and J. Brauburger, ` Plagiator -- A Learning Prover', in 14th Conference on Automated Deduction, ed., W. McCune, number 1249 in LNAI, pp. 256-259, (1997). Springer.

• [kolbe-walther94] T. Kolbe and C. Walther, `Reusing Proofs', in Proceedings of the 11th ECAI, ed., A. Cohn, 80-84, Wiley, (1994).

• [korf85] R.E. Korf, Learning to Solve Problems by Searching for Macro-operators, Pitman Publishing Ltd., 1985.

• [meier-sorge-calculemus00] A. Meier and V. Sorge, `Exploring properties of residue classes', in Symbolic Calculation and Automated Reasoning: The Calculemus 2000 Symposium, eds., M. Kerber and M. Kohlhase, pp. 175-190, (2001). A K Peters.

• [pubmw] E. Melis and J. Whittle, `Analogy in inductive theorem proving', Journal of Automated Reasoning, 22(2), (1998).

• [muggleton90] S. Muggleton, Acquisition of Expert Knowledge, Addison-Wesley, 1990.

• [ruby-kibler89] D. Ruby and D.F. Kibler, `Learning subgoal sequences for planning', in Proceedings of the 11th IJCAI, ed., N.S. Sridharan, pp. 609-614, (1989). International Joint Conference on AI, Morgan Kaufmann.

• [schulz00] S. Schulz, Learning Search Control Knowledge for Equational Deduction, Ph.D. dissertation, Fakultät f. Informatik, TU München, 2000.

• [pub220] B. Silver, `Precondition analysis: Learning control information', in Machine Learning 2, eds., R.S. Michalski, et al, (1984). Tioga Press.

• [sun-giles00] R. Sun and L. Giles, eds. Sequence Learning: Paradigms, Algorithms, and Applications, number 1828 in LNAI, 2000. Springer.