 |
Mateja Jamnik, Manfred Kerber
School of Computer Science, The University of Birmingham
Birmingham B15 2TT, England
{M.Jamnik|M.Kerber}@cs.bham.ac.uk
http://www.cs.bham.ac.uk/~mmk/projects/MethodFormation/index.html
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 difficulty in applying a proof pattern to many domains is that in the current proof planning systems new methods have to be implemented and added by the developer of a system. In this work, we show how a system can learn new methods automatically given a 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. In this project we therefore built a hybrid proof planning system, which uses the existing proof planner [1], and combines it with our own machine learning system. This enhances the system with an automatic capability to learn new proof methods.
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 patterns 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 [3, 8], 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.
|
Figure 1 gives a structure of our approach to learning proof methods, and hence an outline of the description given here. In Section 2.1 we examine what needs to be learnt and give some examples of proofs that use a similar reasoning pattern. Then, in Section 2.2, we sketch the entire learning process: first, we simplify the method representation to ease the learning task. Second, we present our machine learning algorithm. Third, we revisit our method representation and enrich it so that the newly learnt methods can be used in a proof planner for proofs of other theorems. We go on in Section 2.3 to present some results of the evaluation tests that we ran for in order to assess the success of our approach.
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. It often happens that a pattern of lower level methods is applied time and time again in proofs of different problems. In this case it is sensible and useful to encapsulate this reasoning pattern in a new proof method. Such a higher level proof method based on lower level methods can either be implemented and added to the system by the user or the developer of the system. However, this is a very knowledge intensive task and hence, presents a difficulty in applying a proof strategy to many domains. Hence, we present an alternative, namely a framework in which these methods can be learnt by the system automatically.
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 was carried out and is described in Section 2.3.
We demonstrate our ideas with examples that we used to develop and test . All of the example conjectures can be automatically planned for in with the planner which uses strategies [6]. Throughout this paper, we give a general account of the framework exemplified with the existing implementation. Although some of our examples are trivial and can be proved by the existing proof planning systems, they demonstrate our approach. Note that our motivation is not to prove more theorems using the existing machine-oriented reasoners, but to enable proof planners to prove theorems using more human-oriented proof methods. That is, the methods that learns are on a higher level than the existing ones. Hence, the proofs constructed using them are not overwhelmed with unintuitive low-level proof steps, and can be argued to be more intuitive.
The proofs of these examples consist of simplifying an expression using a number of primitive simplification methods such as both (left and right) axioms of identity, both axioms of inverse and the axioms of associativity (where e is the identity element, -1 is the inverse function, and LHS => RHS stands for rewriting left hand side to right hand side).
| (X * Y) * Z | => | X * (Y * Z) | A-l | |
| X * (Y * Z) | => | (X * Y) * Z | A-r | |
| e * X | => | X | Id-l | |
| X * e | => | X | Id-r | |
| X * X-1 | => | e | Inv-r | |
| X-1*X | => | e | Inv-l |
Here are two examples of proof
steps which simplify given expressions and the inferences that are
used:
| a * ((a-1 * c)* b) | => | (by A-l) |
| (a * (a-1 * c))* b) | => | (by A-l) |
| ((a * a-1) * c)* b) | => | (by Inv-r) |
| (e * c)* b | => | (by Id-l) |
| c * b |
| a-1 *(a* b) | => | (by A-l) |
| (a-1 * a)* b | => | (by Inv-l) |
| e*b | => | (by Id-l) |
| b |
In other experiments we looked at examples in the areas of residue classes conjectures and set theory conjectures. For further information on these, see [4] and [5], both of which are available from the project's web page at the URL indicated on the front of this report.
The representation of a problem is of crucial importance for the ability to solve it - a good representation of a problem often renders the search for its solution easy [7]. The difficulty is in finding a good representation. Our problem is to devise a mechanism for learning methods. Hence, the representation of a method is important and should make the learning process as easy as possible.
We start by presenting a simple representation formalism which abstracts away as much information as possible for the learning process. Then we describe the learning algorithm. Finally, we show how the necessary information is restored as much as possible so that the proof planner can use the newly learnt method. Some information may be irrecoverably lost. In this case, some extra search in the application of the newly learnt methods will typically be necessary.
The methods we aim to learn are complex and are beyond the complexity that can typically be tackled in the field of machine learning. Therefore, we first simplify the problem and aim to learn the so-called method outlines, and second, we reconstruct the full information as far as possible. Method outlines are expressed in the language that we describe here.
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:
![[*]](down-arrow.gif){kind=icon}
Let the set of primitives P be
{A-l,A-r,Inv-l,Inv-r,Id-l,Id-r}.
Using this language,
the tactic of our simplification method described by the three group
theory examples above can be expressed as:
Method outlines are abstract methods which have a simple representation that is amenable to learning. We now present an algorithm which can learn method outlines from a set of well chosen examples. It can find an adequate minimal and least general generalisation within the given language restrictions. The algorithm is based on the generalisation of the simultaneous compression of well-chosen examples.
As with compression algorithms in general, we have to compromise the expressive power of the language used for compression with the time and space efficiency of the compression process. Optimal compression - in the sense of Kolmogorov complexity - can be achieved by using a Turing-complete programming language, however, is not computable in general, i.e., there is no algorithm which finds the shortest program to represent any particular string. As a compromise we have selected regular expressions with explicit exponents and branching points, which seem to offer a framework which is on the one hand general enough for our purpose, and on the other hand (augmented with appropriate heuristics) sufficiently efficient.
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.
Our learning technique considers some number of positive examples which are represented in terms of lists 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 this defined measure of size, which essentially counts the number of primitives in an expression. The pattern is also most specific (or equivalently, least general) with respect to the definition of specificity spec which is measured in terms of the number of nesting for each part of the generalisation. 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 choosing the 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: [[a2]*] and [a*]. According to size, size([[a2]*])= 1 and size([a*])=1. However, according to specificity, spec([[a2]*])=2 and spec([a*])=1. Hence, the algorithm chooses [[a2]*].
The learning algorithm is implemented in SML of NJ v.110. Its inputs
are lists of methods extracted from proofs that were
constructed in . Its output are method outlines which are passed
back to . The algorithm was tested on several examples of proofs
and it successfully produced the required method outlines. In
particular, for the example of group theory above:
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 by extra search or by some other mechanism.
In the particular case of our implementation in , information is missing about the parameters for the methods that constitute the newly learnt method. Namely, the methods which make up the new method in take some (or none) parameters. These could be in the form of position information indicating where in the expression the method is applied, or a term naming the concept for which the definition should be expanded, or instantiating a term used by the method, etc. The parameters of a method are supplied by control-rules to reduce and direct the search performed by the proof planner. For example, the parameter in the definition expansion method defn-exp names the concept that should be expanded. The possible relevant control-rules could be of the form `Expand only definitions of the current theory' or `Prefer definition expansion of the head symbol of the formula to prove'.
A set of methods together with a set of control-rules defines a planning strategy of 's multi-strategy proof planner [6]. Note that control-rules of a strategy are used not only for determining the parameters of methods, but also to prefer or reject methods according to the current proof situation.
For each learnt method outline we automatically build 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 methodical expression.
The precondition of a methodical expression 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 pattern which is captured by the method outline.
In the current implementation, the precondition of the methodical expression is computed by depth first search. Besides the choice points of the learnt method outline, 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.
Since the learnt pattern in the method outline was extracted from proofs of planned theorems, we can be sure that suitable control-rules for the parameters exist. The current implementation of the search mechanism looks for control-rules that supply the actually processed method with parameters and adds the possible instantiations to the search space.
From a learnt outline a learnt method can automatically be generated. The learnt method is applicable if some instantiation of the method outline, i.e., a sequence of methods, is applicable. Since methods are planning operators with pre- and postconditions, these conditions must be checked for the method outlines. The complex structure of methods does not allow to test the precondition of a subsequent method of the learnt outline without instantiating the postconditions of the previous methods. That is, the methods of an outline have to be applied to the current proof situation. We implemented a search engine for the application test of the learnt method. The application of a learnt method will introduce the open nodes and hypotheses generated by the search engine to the current proof. For details, see [4] and [5].
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, set
theory and group theory. The aim of these experiments
was to investigate if the proof planner enhanced with the
learnt methods (columns marked with L in Table 1), i.e.,
methodical expressions, can perform better than the standard
planner (columns marked with S in Table 1). 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 methodicals; 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.
We compared the values of matchings and proof length for the three problem domains.
| |||||||||||||||||||||||||||||||||||||||||||||||||||||||
In general, the availability of newly learnt methods that capture general patterns of reasoning improves the performance of the proof planner. In particular, the number of matchings is reduced across domains, as indicated in Table 1. Furthermore, as expected, learnt methods cause proofs to be shorter, since they encapsulate a number of other methods. Also, the time is in general reduced when using learnt methods. There are some overheads, and in some cases these are bigger than the improvements. Since the time should be related to the reduced number of matchings, but it is not in all our cases (group theory), this indicates that our implementation of the execution of methodical expressions, as described in Section 2.2, is not the most efficient, and can be improved.
In general, the coverage when using learnt methods is improved, which is also indicated by the fact that using learnt methods 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 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.
There are several aspects of our learning framework which need to be addressed in the future. With respect to the representation formalism we have mainly considered sequential rewriting proofs. Other styles (different directions of reasoning) should also be considered.
Regarding the learning algorithm itself, we need to examine what are good heuristics for our generalisation and how suboptimal solutions can be improved. While the learning mechanism is not efficient, we argue that we do not need a highly complicated and efficient technique for learning patterns, as in the GENOME project, for example. Our algorithm may be simple and naive, but is sufficient for our examples which are typically small (e.g., less than 50 steps).
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. With our approach, we cannot do that, however. It is a very challenging question left for future research.
We have developed a hybrid system, which is based on the 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.
Secondly, the technical problems to integrate the search engine into the proof planner were bigger than anticipated. This delayed the project so that the test set of examples is not as extended as ideally we would want it to be.
We kept strong links with the group in Saarbrücken, which led to an intensive exchange, in which not only the research fellow, the principal investigator, and the PhD student visited Saarbrücken, but also a number of persons from Saarbrücken visited us. We presented the work at several conferences, workshops (like a Dagstuhl workshop), the ESSLLI summer school, and in a number of seminar talks. These activities made it also possible to win Dr Volker Sorge as a lecturer for the School of Computer Science in Birmingham.
Dr Jamnik has in addition to the research originally proposed continued to work in the field of Diagrammatic Reasoning. She has completed a book on her work, was invited for research visits to Australia and Germany, and gave an invited talk at Stanford, USA.
We have published a summary of the results of the project as a technical report [5] and will submit it as a journal paper as well. All publications and other results will be kept on the web page of the project (http://www.cs.bham.ac.uk/~mmk/projects/MethodFormation/index.html), from which electronic versions of all publications and talks are available in gzipped PostScript and PDF format (see attached print out of the web page).
This document was adapted from a version created by LaTeX2HTML translator Version 98.1p1 release (March 2nd, 1998)
Note also, that there is no need for an empty primitive as it can be encoded with the use of the existing language. E.g., let epsilon be an empty primitive and we want to express [a,b,[epsilon|c],d]. Then an equivalent representation without the empty primitive is [a,[b|[b,c]],d]. We avoid using the empty primitive as it introduces a large number of unwanted generalisation possibilities.
Maintained by
Manfred Kerber,
e-mail:
M.Kerber@cs.bham.ac.uk
Last update: 1.5.2002
School of Computer Science,
The University of Birmingham.