High Performance ATP Systems by Combining Several AI Methods

1 Introduction

Research concerned with achieving more efficient (fully automated) theorem provers focuses on three directions: higher inference rates, eliminating unnecessary infer­ ences, and better control of the search. Although all these directions can indeed lead to more efficiency, bet­ ter control of the search offers the highest gains, but also causes the most problems and has some risks. Nearly all approaches to improving search control involve the use of techniques and methods from other areas of artificial intelligence (AI), as for example knowledge representa­ tion, case-based reasoning (CBR), learning, planning, or multi-agent systems. In most of the known works only ideas from one of these areas are exploited.

One area that should- from the human point of view- be the most promising for high efficiency gains is learning. But the use of machine-learning techniques for improving automated theorem provers faces several severe problems. Learned knowledge has to be stored, re­ trieved, and very often must be combined. So, the focus of attention should not be restricted to the area of ma­ chine learning. Other areas of AI must also contribute in order to successfully apply the results the learning techniques produce.

In this paper we present an approach to controlling the search of an automated theorem prover that com-

Matthias Fuchs

Fachbereich Informatik Universitiit Kaiserslautern 67663 Kaiserslautern Germany

hines techniques from several areas of AI .to overcome the problems that arise when trying to learn and to use control knowledge. The central idea is to utilize a known (i .e. , learned) proof of a so-called source problem solved previously in order to guide the search for a proof of the target problem at hand. To this end we employ a method called flexible re-enactment (cp. [9]) .

Source problems must of course satisfy certain simi­ larity criteria with respect to the target problem. Our techniques for maintaining a database of source problems and our mechanisms for ~electing source problems that are the most similar to the target are inspired by CBR. Unfortunately, one of the important premises of CBR, namely that "small differences between problems result in small differences of their solutions" , is not fulfilled in automated theorem proving.

We cope with this uncertainty by applying the TEAM­ WORK method ([4]), a multi-agent approach to dis­ tributed search. TEAMWORK reduces the risk of deploy­ ing an inappropriate heuristic by having a team of heu­ ristics (agents) guide the search concurrently and coop­ eratively . The reactive planning capabilities of a further agent, namely the supervisor, are made use of to com­ pose a suitable team (cf. [7]) . Moreover, the selection of the most suitable source problem required by flexible re-enactment can also be integrated with TEAMWORK in form of a specialized agent.

The combination of all these AI methods allowed us to build a theorem prover for pure equality reasoning that is fully automated, in both learning and proving, and is able to solve hard problems by using a kind of boot­ strapping process that starts with easy problems and uses their proofs to gradually solve harder and harder problems. Besides providing the problems , no interac­ tion with the system is required. Our experiments vali­ date and substantiate the achievements of our system.

We cannot provide as many details as some readers (and we) would like. These readers may refer to [6] .

2 Equational Reasoning

Equational reasoning deals with the following problem: Given a finite set E of equations (of terms over a fixed signature sig) and a goal u = v. The question is whether the goal equation is a logical consequence of E, i.e., E f=

u = v. Unfailing completion (e.g., [2]) has proven to be quite successful for solving such a proof problem A = (E, u = v). The method is also a good example for so­ called generating calculi that are based on generating new facts until a fact describing the goal is reached.

The inference rules of a generating theorem prover can be divided into two classes: expansion and contraction rules (see [3]). Completion uses the expansion critical­ pair-generation and the contractions reduction and sub­ sumption. Basis for the completion procedure is a so­ called reduction ordering >- that is used to restrict the applicability of the inference rules and to avoid cycles.

An algorithmic realization of the inference rules of a generating theorem prover can be characterized as fol­ lows. There are two sets of facts (equations in our case): the set FA of active facts and the set FP of passive facts. The algorithm centers on a main loop with the follow­ in~ body: At first a fact >. is selected and removed from F ("activate >." ). After that >. is normalized resulting in a fact >.' . (Normalization denotes the application of contraction rules to a fact until none of these rules is ap­ plicable anymore.) If>.' is neither trivial nor subsumed by an active fact, all elements of FA are normalized, >.' is added to FA, and all facts that can be generated with >.' and other elements of FA are added to FP. A proof is found if the normalization of the two terms of the goal leads to the same term.

Assuming that there is a given order in which contract­ ing inference rules are applied, normalization of a fact is a deterministic process. Hence, the remaining indeter­ minism is to determine which fact should be activated next . In order to eliminate this indeterminism, selection strategies and heuristics are used (see, e.g., [5]). In sec­ tion 4 we present such a selection heuristic that is based on re-enacting a successful proof attempt for a problem that is somewhat similar to the problem at hand.

Since we want to learn from (successful) proof at­ tempts, we have to obtain, represent, and store an actual proof run produced by the algorithm and a selection heu­ ristic. S.A denotes the sequence of facts activated dur­ ing a proof run for problem A using a fixed heuristic 1l. The actual proof to A is denoted by P .A and it is obtained by eliminating from s.A all facts that did not contribute to the proof. We refer to the facts occur­ ring in P .A also as the set P .A of positive facts . The other facts in S .A form the set N .A of negative facts that is needed for some learning approaches (see [8; 9]) . A successful proof attempt is stored as the quadru­ ple (A,1l,S.A,P.A) (or (A,C,S.A,P.A) with C denoting the teams used) that allows the use of various approaches for learning from previous proof experience.

3 Teamwork

The TEAMWORK method is a knowledge-based distribu­ tion method for certain search processes ([4]). Equa­ tional deduction by completion, as well as for example first-order deduction by (hyper-) resolution, is a mem­ ber of this class of search processes. In a TEAMWORKbased system there are four different types of agents: experts, specialists, referees, and a supervisor. Experts and specialists are the agents that work on really solving a given problem. Experts form the core of a team. They are problem solvers (in our case theorem provers) that use the same inference mechanism (in our case unfail­ ing completion), but different selection strategies for the next inference step to do. Specialists can also search for a solution (using other inference mechanisms) or they can help the supervisor, for example by analyzing and classifying the given problem like PES (see section 5.2). Each expert/specialist needs its own computing node. Therefore, the supervisor determines the subset of ex­ perts/specialists that are active during a working period.

After a working period a team meeting takes place. In the judgment phase , each active expert and specialist is evaluated by a referee. Each referee has two tasks: judg­ ing the whole work of the expert/specialist of the last working period and selecting outstanding results. The first task results in a measure of success, an objective measure that allows the supervisor to compare the ex­ perts. The second task is responsible for the cooperation of the experts and specialists, since each selected result will be part of the common start search state of the next working period. The referees send the results of their work to the supervisor.

In the cooperation phase the supervisor has to con­ struct a new starting state for the next working period, select the members of the team for this next period and determine the length of the period. The new start state for the whole team consists of the whole search state of the best expert enriched by the selected results of the other experts and the specialists. The supervisor deter­ mines the next team with a reactive planning process in­ volving general information about components and prob­ lem domains (long-term memory) and actual informa­ tion about the performance of the components (short­ term memory). The long-term memory suggests a plan skeleton that contains several small teams for different phases of a proof attempt. These suggested teams are reinforced with appropriate experts/specialists (if more computing nodes are available) . During each team meet­ ing the plan has to be updated. This means that adjust­ ments are made according to the actual results (see [7]).

TEAMWORK allows for synergetic effects that result in enormous speed-ups and in finding solutions to problems that are beyond the possibilities of the single experts and specialists. While the competition of the experts directs the whole team into interesting (and promising) parts of the search space, the cooperation provides the experts with excellent facts they are not able to come up with alone. Thus gaps in their derivations towards the goal can be closed. This makes TEAMWORK the ideal basis for a learning theorem prover.

4 Flexible Re-enactment

Similarity between two proof problems A and B can oc­ cur in many variations. One possible kind of similarity is that a considerable number of the facts that contribute to a proof of A are also useful for proving B (or vice versa). This means in our terminology that the associ­ ated sets of positive facts PA and PB or the proofs PA and P8 "have a lot in common" or, in other words, share many facts. ("PAn PB is almost equal to PA and PB.") Our goal is to think up a heuristic that is able to exploit such a similarity.

Given I = (As, 1i, SAs, PAs ) as past experience re­ garding a source problem As, and assuming that a tar­ get problem Ar is similar to As in the way just de­ scribed, it is reasonable to concentrate on mainly deduc­ ing facts when attempting to prove Ar that also played a role in finding the source proof PAs , namely the pos­ itive facts PAs. We therefore design a heuristic FlexRE which-when trying to prove Ar-makes use of I by giving preference to facts that were important for find­ ing PAs. Such facts will henceforth be referred to as fo­ cus facts. Note that focus facts are facts inferred or._.infer­ able in connection with Ar. They must be distinguished from the positive facts PAs belonging to the source prob­ lem As, since it might be the case that some>. E PAs is not deducible at all in connection with Ar (due to a different axiomatization). PAs is merely used to deter­ mine if some fact >. inferable in connection with Ar is a focus fact. To put it another way, the use of PAs is effected by FlexRE on a strictly heuristic basis, meaning that PAs only influences the selection of facts from pP, not, for instance, pP itself. That is, PAs is a guideline that FlexRE tries to follow if possible.

Depending on how strongly focus facts are preferred, FlexRE will re-enact (parts of) PAs more or less quickly. Some of the focus facts, though useful for proving As, may be irrelevant regarding the proof PAr of Ar even­ tually found. But these irrelevant focus facts are not a big problem. The crucial difficulty is to find those (non­ focus) facts that have to supplement the relevant focus facts in order to obtain a proof PAr . It is very likely that these (few) missing facts are descendants of rele­ vant focus facts. Consequently, FlexRE should also favor descendants of focus facts. Favoring descendants should weaken with their "distance" from focus facts, since it cannot be assumed that the few missing facts are located very deeply relative to focus facts . 1

Preferring descendants of focus facts in addition to giving preference to focus facts themselves justifies the attribute 'flexible' in the term 'flexible re-enactment' which summarizes the working method of FlexRE (see [9] or [6]) .

5 Learning and CBR in the Teamwork Environment

In sections 3 and 4 we concentrated on how to use knowl­ edge learned from previous successful proofs (in form of flexible re-enactment) and on how to overcome the prob­ lems such a use might cause (in form of the TEAMWORK method with cooperation with other experts, assessment of experts and results, and reactive planning to adapt to the problem at hand using long- and short-term mem­ ory). The problems that remain are how to find a proof that should be re-enacted in order to solve a given target problem and how to structure, build, and maintain the long-term memory from proof run to proof run.

1 "Distance" and (relative) depth basically refer to the number of inference steps separating two facts, one of these facts contributing to the deduction of the other.

The first problem will be tackled by a specialist PES that is providing the supervisor with information about known proof problems that are similar to the given tar­ get problem (see subsection 5.2). The second problem naturally depends on how the proof problems are pre­ sented to the system. Found proofs have . simply to be extracted, analyzed and stored (the latter depending on how specialist PES will perform its retrieval). As we shall see in the next subsection, the necessary components are already provided in form of TEAMWORK agents.

5.1 T he Basic Learning Cycle

Systems that use learning techniques for solving their tasks can be (very) roughly divided into two groups: systems that have a cleculy defined learning phase af­ ter which (usually) no further learning takes place, and systems that always learn. In automated theorem prov­ ing, systems of the first type may be usable in clearly defined situations (see, for example, [8]), but in general learning should never stop.

Nevertheless, one can observe times in the use of a (learning) theorem prover in which new domains are ex­ plored, and other times in which one is interested in proving one particular problem. When exploring a new domain, typically there is a set of problems to be solved , and when starting the exploration no knowledge in the prover will be triggered. In the following, we will first concentrate on the exploration of a new domain and then we will point out how the one-problem case is handled.

When exploring a new domain the ordering of the problems given to a prover may influence its success. In order to deal with this problem we decided to let the prover handle the ordering of the given set of prob­ lems and also allow the prover to make several attempts to solve a problem. The latter is necessary since each solved problem may result in new knowledge that al­ lows for solving some other problems that could not be solved so far ("bootstrapping"). Note that the set of problems given to the prover has to include easy and typical problems of a domain that the prover can use to get fundamental knowledge about this domain.

As already stated, in a TEAMWORK-based system the long-term memory that represents knowledge about do­ mains is the responsibility of the supervisor. When con­ fronted with a set of example problems of a new do­ main, the supervisor controls not only the single proof attempts, but a whole series of proof attempts that are to result in solving as many of the problems as possible.

Since the supervisor has no appropriate information when being confronted with a new domain, the first step is to try to solve the given problems with conventional means, i.e., without the use of experts and specialists that employ learned knowledge. This is accomplished by using a pre-defined team for a few cycles for each of the given problems (in a separate run). After generating 1 =(A, C, SA, PA) for each solved problem A, this data is integrated into a database of past proof experience that is part of the long-term memory. This database is essentially organized as case base. Hence, the struc­ ture and retrieval processes regarding this database are strongly related to CBR techniques (cp. [10] and sub­ section 5.2). Then the supervisor tries to solve the re­ maining problems (again imposing a time limit on each run), but now the teams are different . The team of the first working period is again pre-defined, and contains, besides good general purpose experts, the specialist PES.

After the first working period, the supervisor uses its reactive planning process to adapt the team to the prob­ lem. If PES was not able to report to the supervisor a problem from the case base that is similar to the target problem at hand, then the supervisor proceeds according to its standard procedure. Otherwise, the expert FlexRE will become a member of the next team, utilizing the re­ ported problem from the case base as source problem. 2 Problems that can now be solved are analyzed so as to produce new data for the case base. For the remaining unsolved problems this whole process is repeated until no more new problems can be proven. Note that after the initial round that uses the pre-defined team with­ out components using learned knowledge, in all other rounds each solved problem is immediately added to the case base so that it already can be used for the proof at­ tempt of the next problem. Thus the number of rounds is often reduced.

In the one-problem case, i.e., in the presence offunda­ mental domain knowledge, the supervisor immediately employs a team that includes PES, and the supervisor plans and controls the whole proof attempt as described above. If the system is successful, the data of the run is also added to the case base.

5.2 Specialist PES

As described before, specialist PES retrieves one or pos­ sibly several source problems that are similar to a given target problem AT, and transmits information on these problems to the supervisor. More exactly, after receiv­ ing a target problem AT = (AxT , AT) given over a fixed signature sigT, PES returns infor.mation RpEs (AT) on similar problems As, where RPES (AT) = {( u, Ps) : condT ( u(As))}. The data is determined by condT and comprises the set of positive facts Ps associated with source problem As, and a signature match u from As to AT. ( u provides an appropriate renaming of the func­ tion symbols occurring in sigs.) condT denotes that a problem As (translated from sigs to sigT by applying u) is most similar to AT (there are no other problems more similar to AT than As) , but also that the similarity be­ tween As and AT seems to be sufficient.

2 Jf PES provides more than one possible source problem, then the supervisor can react in various ways: It can select the most similar source problem and discard all others (which was done in section 6), or it may use several experts FlexRE, each using a different source problem, or it may supply the single FlexRE with the source problems provided by PES in successiOn.

In order to construct such a predicate we shall use a quasi-ordering tT that allows us to compare the simi­ larity between proof problems and a target problem. It should hold true that A1 >-T A2 if (and only if) AT is more similar to A1 than to A2 . Furthermore, an absolute measure of similarity is needed in order to construct a minimal similarity predicate ms that estimates whether the similarity between the target and a source problem seems to be sufficient or not.

Basically, there are two possibilities to construct tT in order to estimate whether a problem A1 can provide a more suitable source proof than a problem A2 : On the one hand it is possible to compare the problem de­ scriptions, and on the other hand one can compare the search effort spent on solving the two problems. Con­ sidering the working method of FlexRE it is reasonable to consider A1 as providing a more suitable source proof than A2 , if the target AT is more similar to problem A1 than to A2 w.r.t. its problem description. Neverthe­ less some information on the search conducted to solve a problem, namely the length of the search protocolS, can be consulted. Since some of the positive facts of more difficult problems (problems with a longer search proto­ col) were quite difficult to reach it seems to be sensible to force the activation of these probably useful, but hard to reach facts by using them as focus facts ( cp. section 4). Thus more difficult problems should be favored.

Similarity between problem descriptions is surely also suitable for constructing an absolute similarity value in order to decide in favor of or against sufficient similarity. Information on the search protocol is difficult to use for this particular purpose and should only be used as a criterion to compare different problems.

In order to assess the differences between the prob­ lem descriptions of two proof problems we employ the similarity measure simT. As discussed before, this mea­ sure is useful to construct tT and ms . The design of simT is motivated by the fact that a target problem AT = ( AxT, AT) is proved by virtue of a proof of a source problem As = (Axs, .As), if all axioms of Axs are subsumed by axioms of AxT and the target goal AT is subsumed by the source goal .As. Hence, subsump­ tion criteria will play the major role in our approach. Furthermore, refinements by using other criteria (e.g., subsumption modulo AC) are imaginable (see below). These refinements have proven their usefulness in exper­ iments, although naturally a simple proof replay often is impossible if Axs and AxT are similar in such a way.

In order to realize measure simT we introduce a (asymmetric) similarity rating sim~q defined on equa­ tions over sigT. Let ax 1 and ax2 be two equations. We define sim~q(ax 1 ,ax2) E (0;1] by sim~q(ax1,ax2) = max{ rating(pi) : p; ( ax1, ax2), 1 ::; i ::; m}. Pl, . .. , Pm are similarity criteria defined on equations. The func­ tion rating judges the reliability of a measure in order to judge similarity between two equations.

Possible similarity criteria are the relations <l, <l A, and <lH U l>H where <l denotes "plain" subsumption, and <lA subsumption modulo the theory given by a set of equations A. (Here, we shall always use A = AC). ax1 <l H ax2 stands for a homeomorphic embedding of ax2 in ax 1 . We used the ratings 1, 0.8, and 0.2 for the criteria <l, <l A, and <l H U l>H, respectively. Hence, subsumption is considered to be very important, whereas homeomor­ phic embedding is considered to be a very weak similarity criterion. Note that we actually refined 8im~q by adding further similarity criteria thus increasing the ability to produce distinctive measures. But a description of these technical details is beyond the scope of this paper.

With the help of this measure we are able to con­ struct a similarity measure defined on proof problems. In the following let AT = (AxT, AT) be a target prob­ lem, and A s = (Axs, As) be a source problem given over 8i9T· LetAxT = {ax1, ... ,axm},Axs = {ax~, ... ,ax~} (n, m > 0). The similarity of target and source problem is 8imT(AT,As) = (81 ,82,83) E [0; 1]3, where

Thus, 81 judges the degree of "coverage" of Axs through similar axioms of AxT. For example, we have 8 1 = 1 if all source axioms are subsumed by target ax­ ioms. 8 1 decreases if only weaker similarity criteria are fulfilled. The value 82 represents the percentage of target axioms that have a similar counterpart in Ax s. Addi­ tional axioms in AxT do not prevent the source proof from being applicable (in the case 8 1 = 1), but may complicate the search for this proof. Finally, 83 mea­ sures the similarity between target and source goal AT and As. We have 83 = 1 if As subsumes AT.

With the help of simT we are now able to estimate if the similarity between AT and As seems to be sufficient. To this end, we check if the predicate ms is fulfilled with ms(simT(AT,As)) iff c1 · 81 + c2 · 82 + c3 · 83 ~min, where c1, c2, c3 E IR., and min E IR is the threshold. In our implementation we use c 1 = 3, c 2 = 1, c3 = 2, and min = 1. Hence additional axioms in AxT are considered quite harmless, while a good coverage of Axs is considered to be important. Since we use min = 1, a subsumption of one third of the axioms of Ax s, or no superfluous target axioms, or a subsumed target goal each suffice alone to reach the threshold.

simT is also employed to define ~T· We define ~T as a lexicographic combination of two quasi-orderings ~s and ~D, where ~s compares the similarity of two prob­ lem descriptions with respect to the target problem (us­ ing 8imT ), and ~D compares the length of the search protocols ( cp. [6]). Using ~T and ms, we can define condT. We apply

In the subsequent section we shall discuss the exper­ imental results we obtained with DISCOUNT by using specialist PES and expert FlexRE.

6 Experimental Results

Finding appropriate test sets of problems for our learning prover was not easy, because in most publications only hard problems are given. But we must solve at least one problem with conventional means in order. to start the bootstrapping process. Fortunately, the TPTP library ([13]) contains two domains that include related prob­ lems of various degrees of difficulty. While we could use the domain groups (GRP) without any changes, the do­ main logic calculi (LCL) consists of several subdomains (some of which contain only hard problems, again) and is not given in a pure unit-equality axiomatization. There­ fore we had to transform the problems of one subdomain (the CN calculus) for our experiments.

The achievements of a learning approach can only be observed when results from conventional provers are also provided. Besides two of our experts (AddWeight, or Add for short, and Occnest , see [5]) we will also use OTTER (version 3.0, using the autonomous mode, see [11]) to allow a comparison. Since OTTER has won the CADE-13 theorem prover competition ([12]) in the category "Unit Equality Problems", we think that a comparison with the current state-of-the-art is thus provided.

Our learning approach is integrated into our prover DISCOUNT (see [1]) , that is implemented in Con Unix machines and has an old and slow inference engine. We limited each distributed run of it to 3 minutes, while the other provers had 10 minutes. The ordering in which DISCOUNT tried the problems is the lexicographical or­ dering of the names of the problem. All experiments were performed on SUN Sparc-10 machines, the team runs employing two of them. There are 125 problems in the GRP domain and 24 in the LCL (CN) domain (for the transformation into equality problems, for more results and a broader analysis of them, see [6]) .

Table 1 shows that our main goal, developing a prover that is able to automatically learn and therefore to solve more problems than other provers, has definitely been achieved. In both domains, our learning team clearly outperformed OTTER and the single experts by at least 15 percent. Table 2 highlights some of the problem so­ lution chains that are produced by our prover. In the GRP domain, problem 179-1 was solved conventionally and used in the next round to solve problem 179-2, which was basis for solving problem 183-1 (in the same round). Using problem 183-1 DISCOUNT was able to solve prob­ lem 167-3, which was then used to solve problem 167-1. In the LCL domain, problem 047-1 was used to solve 0481 which allows for solving 050-1 that then is the source for problem 051-1. Due to the immediate usage of solved problems when trying to solve the next one , the chain of the GRP domain is the result of 4 rounds , while the chain of the LCL domain was produced in only 3 rounds of the bootstrapping process. Note that any other order­ ing of the problems would produce the same Table 1 and the same chains in Table 2. Only the number of rounds needed may be different.

Among all the problems there is only one problem that OTTER can solve and our learning team cannot, but 27 problems that our learning team can solve and OTTER cannot.

In general, our experiments show that our concept of a learning theorem prover clearly outperforms current conventional theorem provers if the learning prover is provided with enough "exercise" in the domain it has to work in. In this case even the learning process is accomplished by the prover without help from the user.

7 Conclusion and Future Work

We presented a concept for a learning theorem prover that uses methods from several areas of AI. AI methods like planning and CBR are combined with the TEAM­ WORK multi-agent architecture, resulting in a theorem prover that clearly outperforms renowned provers. A prerequisite for the success of our system-as for a hu­ man student- is the presentation of problem domains in a "learnable'.' way, meaning that the presented problems cover the whole spectrum of difficulty ranging from easy to challenging. In a kind of bootstrapping process the system is able to solve harder and harder problems with­ out any interaction on the parts of a user ("teacher").

Despite the success of our system, nevertheless most components are only first ideas that leave much room for improvements and extensions . Also, there are other concepts that can be used (e.g., [8)) or are at least worth investigating (e:g., the division of problems into easier sub-problems on the basis of learning), that will provide a wider range in the use of learned knowledge.

Acknowledgments

This work was supported by the Schwerpunktpro­ gramm Deduktion of the Deutsche Forschungsgemein­ schaft (DFG) .