Verification-based Learning: A Generalized Strategy for Inferring Problem-Reduction Methods

I Introduction

Ver1ftca1 i on- Bt~ sed Let~rntflg : A Generalizlltion StrlltPgy for Inferring Problt>m-Redurtion Mt>t.hods

Sridhar Mahadevan*

Computer Science Department Rutgers University New Brunswick, NJ 08903

design / plannin g rlomain .... . k lt r· \-\l <~dg l' 11 .: :1 " J·r 'P r · {·hr· r -. . +rl ..;nrh domains, have frequent)) a<iup ted a prob/Pnt re. durt? nn a pJ-.'roaf h to solving problems. Thus, we need to de,·elop techniques for learn­ ing problem-solving methods which are appropri ate to the problem-reduction formulation of problem-solvin g. The primary contribution of this paper is to present a new technique for infer­ ring general problem-reduction methods from trainin g examples of decompositions of specific problems. This technique , Verificat ion­ Based Learning(VBL}, can be viewed as an extension of earlier techniques, particularly that of. [3, 6 J, to the problem-reduction formulation of problem-solving.

This research arose in the context of developing LEAP, a Learning Apprentice system for circuit design [7[. By a Learning Apprentice system, we mean one that is meant to act as an interactive problem-solving aid , and is specifically designed to augment its knowledge base by monitoring and analyzing the problem-solving activity of its users.** In those situations, where it is unable to provide advice 1 or when its advice is rej ected by the user , LEAP will augment its knowledge of circuit design , by analyzing and generalizing the solution provided by the user to form a new problem-reduction method. At present we have im­ plemented a prototype version of the LEAP system. The ex­ ample of a problem-reduction method in circuit design that we describe later in this paper is one of several instances of circuit decompositions we have used to test this prototype version.

B. The Problem-Reduction Formulation of Problem-Solving

We now give a more precise description of the model of problem-solving that we use in this paper. The problem-reduction formulation of problem-solving has been well-studied [8, 9[. ··· In this formulation, states describe problem in.tances: the initial state is the description of the problem being solved , the final state is a solution to the original problem, and a problem­ reduction method , which is a mapping between states, is one that decomposes a given problem into a number of simpler sub­ problems, such that the aolution to the original problem is ob­ tained by some compoaition of the ·olutions to each of the subproblems.

For the purposes of this paper , we define problem-reduction methods to be the following mapping,

**Thus, gaining expertise by "looking over their shoulders"

.. *The distinction between state space methods and problem-reduction methods is alternatively described in /8] as that between production-type. methods and re.duction-twe. methods.

where P is the specification of a problem (in some language), which is decomposed by the method M into a set of subproblems P l'" .. ,P N" The combinator C describes how the solutions to each of the subproblems Pi are to be combined to yield the solution to the or-iginal problem. We now illustrate the abstract notion of a problem-reduction method, with the following example chosen from the domain of symbolic integration.

Integral-of-a-Sum Method :

The above method decompo1es the problem of integrating a sum of two functions into a set of 1ubproblems, that of integrating each of the summands. Using the terminology introduced earlier,

the problem P is the integral f {/ 1 (z) + f 2 (x)}dx , the two sub-

problems P 1 and P 2 are J f 1 (x)dx and f f 2 (x)dx respectively, and the combinator C is addition.

C. Using Verification as a basis for Generalization

We now introduce the idea of using verification as a basis for the generalization of problem-reduction methods from instances. We represent an instance of the application of a problem­ reduction method as an ordered pair of states < x,y> ; x represents an instance of the class of problems to which the method can be applied , and y represents the composition of some set of sub­ problems whose solution implies the solution to the original problem x. Given such an instance of an unknown problem­ reduction method as a pair of states <x,y>, the generalization problem that we address in this paper consists in determining this general method from the instance. As a first step towards the generalization , the program verifies that the solution to the com­ posi t ion of the subproblems, y, implies the solution to the original problem x. The second (and final) step involves the cent ral idea underlying the VBL technique: the unknown method can be determined by generalizing the problem-8tates x and y, retaining only those features of theu problem-state· that were im­ portant for the purpose of verifieation.

The idea of using verification as a basis for a learning tech­ nique , is related to similar schemes used in other analytical learning techniques, specifically Goal-Directed Learning [4J, Explanation-Based Learning [ 10[ and Constraint-Based Generalization [5[. All these learning techniques are similar in that they first generate an explanation or proof (here, a verification) of why the given trammg instance (here, instances represent applications of problem-reduction methods) satisfies a particular goal (here, the goal is showing that the decomposition of the problem instance was a correct one) , and then they generalize the instance (here, forming a new problem-reduction method) using the constructed explanation or proof to constrain the generalization.

D. Outline of the paper

• In sect ion 2, we state the generalization problem for inferring problem-reduction methods from examples.
• Sections 3 and 4 contain two detailed examples of the application of VBL to the task of inferring problem­ reduction methods in circuit design and symbolic in­ tegration .
• Finally , in section 5, we summarize by viewing VBL from a number of different perspectives, outlining some of its limitations and describing some work in progress on them.

II The Generalization Problem for Inferring Problem-Reduction Methods

A. Statement of the Problem

Before proceeding to give domain-specific examples of VBL, as we will be doing in sections 3 and 4, it is important that we state the generalization problem that this paper addresses, in domain-independent terms. Figure ll-1 provides such a statement.

Figure Il-l : The Generalization Problem for Inferring Problem-Redurt.ion Methods

· Given -

• o A language of instances of problems.
• o A language of generalizations of problems. Each generalization in this language describes some class of problem instances.
• o A single positive instance of a problem-reduction , which is composed of the following pair.
• Specification of a problem P in the instance language.
• Specification of a set of subproblems Pi in the instance language and a combinator C.
• o Some domain theory, in the form of a set of tran·formations, which can be used to verify assertions of the form -- the solution to the com­ position of the set of subproblems Pi implies the solution to the problem P. More formally, such assertions can be stated as

· Deternline -

• o Description of a problem-reduction method in the generalization language that is consistent with the observed instance; this is computed by generaliz­ ing the specifications P and Pi, using the verification of the above assertion to constrain the generalization.

B. Discussion

The domain theory required by VBL, in order to construct a proof or verification of the assertion in figure 11-1, is a set of tran·formation·; each transformation can be viewed as a primitive problem-reduction method , and new problem-reduction methods can be viewed as being obtained by composing these primitive methods together in a specific manner. Forming a new problem­ solving method by composing together a sequence of primitive methods is a general strategy, which has been used as the basis for many earlier techniques [3, 11[. In the next section, we will provide an example from circuit design , which illustrates how we use this approach to infer new problem-reduction methods.

III Learning Problem-Reduction Methods for Circuit Design

In this section we describe an application of VBL to the task of acquiring problem-reduction methods for circuit design. We begin by formulating circuit design as a problem-reduction process. We then focus on a particular problem-reduction method for designing a small class of circuit specifications, first describing the method itself, and subsequently , in a number of detailed steps, showing how it may be acquired from a single training in­ stance.

A . C ircuit DPsign as Probl<'m RPdn<"t.iou

In order to view circuit design as a problem-reduction process. we need to specify the various components that constit ute t he problem-reduction model. The language of instances of problems corresponds to the functional specifications of circuits; these define the mapping between the input and output signals of a circuit . (for example, the out put of an adder equals the sum of its inputs.) The initial state is the functional specification of a cir­ cuit to be designed, the final state is an implementation of the circuit specification in terms of a set of primitive components, and a problem-reduction method is one that decomposes a given circuit specification P into specifications Pi of a number of inter­ connected simpler circuits (submodules) . The language of generalizations of problems enhances the expressive capabilities of the instance language, by including the ability to specify arbitrary boolean functions as part of functional specifications**** We thus view the problem of learning problem-reduction methods in circuit design , as an instance of the more general problem of inferring problem-reduction methods from examples.

B . An lllustration of Problem-Reduction in Circuit Design

For the sake of concreteness in the discussion of the VBL technique, we need to consider a simple example of a problem­ reduction method in circuit design, and phrase the remainder of the discussion in terms of this example. We first describe the method itself, and then provide an example of its use.

Figure 111-1 provides a simple example of a problem-reduction method that suggests one plausible way of implementing a con­ junction of any two boolean expreBBions. The left-hand side (LHS) of the problem-reduction method describes the class of specifications to which it can be applied . The right-hand side (RHS) of the method suggests both a decomposition of the specification in the LHS into specifications for a set of sub­ modules , and also a way of interconnecting them.

A training example that represents an instance of the above method is given in figure III-2. In this example the circuit being designed is a product-of-sums circuit whose specification P is as given in the figure . The context here is that of a Learning Ap­ prentice system, which being ignorant of the above general method for implementing a conjunction of two boolean expres­ sions, may suggest using an AND gate and two OR gates as one way of implementing the circuit specification P. The user steps in at this point , and disregarding the system's suggestion, provides his preferred way of implementing the specification P, which is to use a set of NOR gates interconnected as shown in figure 111-2.

**HFor reasons of clarity in the ensuing discussion of the learning method, we adopt a simplified representation of functional specifications of circuits. Specifically, this representation omits any reference to attributes of signals such as timing and encoding. (7] provides further details of this representation.

The Learning Apprentice v1ews the user-supplied example as representing an instance of the application of an unknown problem-reduction method, and sets itself the task of inferring the general method . The general problem-reduction method that is inferred from the training instance in figure 111-2, is the one we described earlier, in figure 111-1. In the next few paragraphs, we provide a detailed description of the use of VBL in determining this general method.

-------------~-·---·· ·· ---

Functional specification to be Implemented P:

User's Solution: Product-of-Sums circuit

where

P 1 : (EQUALS X (NOT (OR lnput 1 lnput 2 )) )

P 2 : (EQUALS Y (NOT (OR lnput 3 lnput 4 )) )

P 3 : (EQUALS Output (NOT (OR X Y)) )

C. Step 1: Forming the Composed Specification

The first step in the process of inferring a general problem­ reduction method from a training example is verifying the correct­ ness of the decomposition for the given example. In circuit design, this corresponds to ensuring that the function computed by the decomposed circuit meets the original circuit specification. Before attempting to construct a proof of correctness, we must have some way of determining the function computed by the decom­ posed circuit. It is to this matter that we turn to next , in our discussion of VBL.

**< bool·fnl> above represents an arbitrary boolean function .

By composing the specifications of each of the submodules constituting a given circuit, in a way that depends on the inter­ ·· .rlfl ''''''' n uf lh f' '-ld l!ll ·H111 if':o- Y, · ' '71ft ,j, , · t " l 'i· t f i P I IL·I /1 f,j th1 r irc uJL ·::. fun ction from its s tru cture . Tht~ curnpos ed specificahon , ca n be compu ted by a simple substitution process, and is deter­ mined by the relat ionships between signals at various points in t he ci rcui t. For example, we can obtain a relationship between the output signal and the inputs of the product-of-sums circuit in fi gure Ill-2 , by substituting for X and Y in the specification P 3 , t heir relat ionships to the input signals described in P 1 and P 2 . Carrying this out , we obtain the following composed specification for the product-of-sums circuit.

Several remarks may now be made, in connection with our definition of a composed specification, which are of importance to the generalization process that follows .

• In general , the composed specification will be a reexpreaaed version of the original specification. This is due to con·traint& on the possible structures that primitive circuits (problems) can take. For example, in VLSI design, since circuits naturally invert their in­ puts, specifications in terms of AND and OR boolean functions must often be reexpressed in order to obtain implementations using combinations of NAND and NOR gates. Thus, since we must show that the com­ posed specification implies the original specification, this motivates the need for a verification of the cor­ rectness of a decomposition.
• o The form of the composed specification depends on the structure of the decomposed circuit (problem) . We will make use of this property, when generalizing each. of the submodule (subproblem} specifications.

D- Step 2: The Process of Verification

Having obtained the composed specification of a decomposed circuit (problem) , the next step in the VBL technique is to con­ struct a proof of the correctness of the decomposition. That is, we need to verify the truth of the following assertion , which we repeat from figure Il-l, and which states that the composed specification must imply the original specification.

For the product-of-sums circuit example, by substituting its com­ posed and original specifications in the above expression, we ob­ tain the following assertion, whose verification is the topic of this section .

If we are ooly concerned about verifying arbitrary assertions of the above form, it is clear that there exists considerable latitude in the choice of an appropriate scheme for verification. Many such schemes have been developed by researchers interested in circuit verification 112]. However, since we view verification as only a means to our end of wanting to infer problem-reduction methods, any scheme we choose must meet the following ad­ ditional requirement - it ·hould be pouible to uae the proof conli t rurl.ed by the ' ' t:. r i j 'icfl/1('11 -ri.oth. ,, , the specifications that were nerded through.*** } ·· ,,. for ,,,j LJ/I ·,'JI f e_fl(llrf!j, {If th< proof to carry We now describe a verification scheme sat isfying the above re­ quirement. We construct the proof as a sequence of tranaformations, which will yield the original specification when applied to the composed specification. Each such transformation, which can be viewed as a primitive problem-reduction method, is specified by its precondition - the class of specifications to which it can be applied - and its po.tcondition, which describes the result of applying the transformation . Constructing a verification as a sequence of such transformations satisfies the above require­ ment , since it enables us to determine from the sequence a generalizat ion of the circuit specifications P and Pi, using con·traint propagation. Two examples of transformations that we will use in the current example are given below.

De-Morgan's Law: Precondition: (NOT (OR <bool-fnl> (bool-fn2>) ) Postcondition: (AND (NOT <bool-fnl>) (NOT <bool-fn2)) Remove-Double-Negation: Precondition: (NOT (NOT <bool-fn>) Postcondition: <bool-fn>

Using the scheme mentioned above, we now provide, for the product-of-sums circuit example, a verification of the correctness of the user-suggested decomposition in figure Ill-2.

Verification as a Sequence of Transformations

In summary, we have now cast the problem of verification as one of a aearch for a sequence of transformations, which will produce the original specification when applied to the composed specifica­ tion .****

u · Truth to.blu is a simple example of a scheme that could be used to verify the above assertion, but which does not meet the above requirement .

**·· Although no mention of it will be made in this paper, we are &88Um·

ing that this search can be controlled by some appropriate search strategy, such as meam-end.t analysis.

E. St<'p 3: Dt't<'rminiug lh<' <.<·JJ<'raJi,,.d Compo~<'d Specification

In order to infer a new problem-reduct ion method from the given training example, we need to compute both its precondition (the IF part), and its postcondition (the THEN part). If we regard the original and composed specifications as instances of the precondition and postcondition of the new method , then clearly, the next step consists in generalizing these specifications; further­ more, as we mentioned earlier, we would like to constrain the generalization using the proof of the correctness of the decomposi­ tion.

In this section we describe how, given the verification proof as a sequence of transformations , the composed specification may be generalized using a restricted version of a well-known technique, constraint backpropagation(CBP). CBP is a technique for deter­ mining the domain of a sequence of operators that produces some constrained range of states ]6] . In our case, transformations can be viewed as operators, but we have no constraint on the range except that it match any arbitrary functional specification, which we denote by < any-func-spec>. (since we are learning arbitrary problem-reduction methods, and not sequences that lead to "solved" states, as in ]4]. ) The domain of the sequence, in our case, is a generalized composed specification that will produce, upon application of the sequence, a corresponding generalized original specification.

The problem with using weakest precondition techniques to compute the domain of a sequence is that, in many cases, dis­ junctive expressions are produced. In particular, disjuncts arise when ever sequences contain operators that were applied to only a part of the expression representing the problem state. For ex­ ample, in the verification sequence above, the first application of the Remove-Double-Negation transformation was to a subexpres­ sion matching its precondition. Disjunctive expressions cause two kinds of problems. First, since the number of disjuncts can grow exponentially in the length of the sequence, storing all of them is a non-trivial issue. Second, even if all the disjuncts could be stored, it is quite likely that some of the disjuncts represent in­ itial situations in which the sequence is an inefficient one to use. (For example, we have observed this problem crop up when using goal regression to compute the weakest precondition of a plan; some of the disjuncts represent initial states in which the plan is a very inefficient one to apply.)

We illustrate below a simple solution to this problem that uses information regarding how transformations were applied (in particular, their bindings) , from the verification of the training in­ stance, to prune out some disjuncts during the CBP process. (For example, the expression (NOT (NOT (NOT (NOT < bool-fn> )))) is a valid domain description of a sequence of two Remove­ Double-Negations, which is not generated in the CBP computa­ tion below.)

Computing th<' g<'uf'ralizNI ( ·.,mpos<'d Specification

(AND (OR Input 1 Input 2 ) <bool-fnl> ) (AND <bool-fn2> Rernove-Double-Neg- 1 (NOT (NOT <bool-fnl>)) Remove-Double-Neg- 1 (AND (NOT (NOT <bool-fn2>)) (NOT (NOT <bool-fnl>)) De-Morgan- 1 (NOT (OR (NOT <bool-fn2>) (NOT <bool-fnl>) ))

To begin with, the expression < bool-fnl > above is produced by intersecting the range of the first Remove-Double-Negation transformation (any boolean function) with the range of the en­ tire sequence ( < any-func-spec> ). Installing this expression as the second argument to the AND expression (the original specification), as we have done above, reflects the context in which this transformation was used in the forward direction {during verification) . In the first step above, we backpropagate < bool-fnl > over this transformation, keeping the expression sur­ rounding it unchanged. Similar remarks hold for the occurrence of < bool-fn2> above, and for the backpropagation over the second transformation. Finally, backpropagating over De­ Morgan's does not present a similar problem, since its range in­ tersects onto the expression backpropagated over the first two transformations.***** The generalized composed specification it­ self is of little use to us; what we really need are generalizations of the specifications of the submodules (in general, subproblems) that constitute the product-of-sums circuit in figure 111-2. These generalized specifications are shown below.**

Generalized specifications of the subrnodules in figure

111-2 . pl : (EQUALS X (NOT <bool-fn2>) . p2 : (EQUALS y (NOT <bool-fnl)) . Pa : (EQUALS <out) (NOT (OR X Y))

Comparing the generalized submodule specifications m figure III-I with the submodule specifications given in figure 111-2, we see that the important feature of the two submodule specifications P 1 and P 2 (the two input NOR gates in figure 111-2), which enabled the verification to carry through, is that they both be the negation of some boolean function.

F. Step 4: Determining the (;eneraliz"'l Original Specification

In this section , we describe methods for generalizing the original specification , given that the generalized composed specification has already been computed. One simple . method in­ volves storing the variable bindings generated while computing the generalized composed specification (for example, the subexpres­ sion (OR lnput 3 lnput 4 ) was replaced by < bool-fnl > ), and apply­ ing these substitutions to the original specification . Another method , which illustrates better that the composed and original specifications form the domain and range of a sequence of trans­ formations , involves, as we show below, reapplying the transfor­ mation sequence to the generalized composed specification .

· ·· · · Although implementing this procedure has been tempts at formali~ing it have not yet been successfuL an easy task, at·

**Fi~uring out the generalization of each submoduJe specification from the gene~ahzed composed specification is straightforward, provided some book­ keepmg was done while forming the composed specification in the first

place.

Computing the Generalized Original Specification

(NOT (OR (NOT (bool-fn2>) (NOT <bool-fnl>) )) De-Morgan (AND (NOT (NOT <bool-fn2>)) (NOT (NOT <bool-fnl>)) Remove-Dou bie-N ega tion (AND <bool-fn2) (NOT (NOT <bool-fnl>)) Remove-Double-Negation

Comparing the generalized original specification - the last expres­ sion in the above sequence - with the original specification P in figure 111-2, we see that a generalization of the original specifica­ tion has been achieved from a conjunction of disjunctions to a conjunction of an11 boolean function·.

G. Step 5: Forming the New Problem-Reduction Method

We showed above how the original specification P and the submodule specification Pi could be generalized. The final step is to form a new problem-reduction method that is based on these generalized .specifications. It is clear that the generalized original specification will form the precondition , or LHS , of the new problem-reduction method. Also, the postcondition, or RHS, of the new method can be formed from the generalized submodule specifications and the combinator C. For our present example, the new problem-reduction method that is inferred (from the training instance in figure III-2) is the one given in figure III-1.

IV Learning Problem-Reduction Methods for Symbolic Integration

In this sectioR we will briefly .illustrate how the same VBL technique can be used to learn problem-reduction methods in symbolic integration. This will provide some justification for our claim that VBL is general technique , and can be applied to more than one domain. Further details of the steps sketched below are described in 113].

A. Symbolic Integration as Problem-Reduction

We begin by viewing the process of integration in terms of problem-reduction. To this end , note that the language of in­ stances of problems in symbolic integration is the language of in­ tegrals of mathematical functions. The language of generalizations of problems includes the ability to specify arbitrar11 functions as part of integrals. Problem-reduction methods here are the standard rules of integration*** We may thus view the problem of learning integration methods from examples, as an instance of the more general problem of inferring problem-reduction methods from examples.

B . An Illustration of Problem-Reduction in Symbolic Integration

Consider the following example of a problem in Symbolic In­ tegration, and a way of decomposing the problem.

Original Problem P: J {3x 2 + sin(x)}dx

Decomposition: J 3x 2 dx + J sin(x)dx

···such as the ooe we described in section l.B.

The original problem P has been decomposed above into two sub­ problems, P 1 , which is J 3x 2 dx , and P 2 , which is J sin(x)dx. The combinator C above is addition . The generalization problem here lies in determining a general method , by generalizing the specifications P and Pi, which could produce the above decom­ position. In the next few paragraphs, we summarize the main steps involved in inferring the general method ,

C. Stepsl&2: Forming the Composed Specification and Verification

Here, unlike the circuits domain , we do not need to construct the composed specification, since the combinator (addition) specifies that explicitly. We can proceed directly to the verifica­ tion step.

We now describe what verification means in symbolic integra­ tion. We can make use of the following result , which asserts that if the derivatives of two integration problems are shown to be equal, then the solutions to the two problems are identical. (The reasoning is that if the derivatives of two functions are equal, then they differ at most by a constant. Two solutions to an indefinite integration problem which differ by a constant are both instances of a more general family of solutions, F(x) + a constant. ) We may thus take as the problem of verification in symbolic integration, the task of showing that the derivative of the composed specification is equal to the derivative of the original specification. Given the above result , this will imply the equivalence of the original specification and the composed specification. As earlier, we can proceed to verify instances of problem-reductions using a sequence of transformations, except in this case transformations correspond to rules of differentiation. An example of such a transformation , which would be useful in verifying the above problem-reduction instance, is given below.

Derivative-of-a-Sum

Precondition: d j dx{fl(x) + f2(x)}

Postcondition: d j dx{ll(x)} + d j dx{f2(x)}

D. Step 3: Determining the General Composed Specification

Given a verification of a problem-reduction in symbolic in­ tegration as a sequence of transformations of the kind shown above, we can use a procedure completely analogous to the one ri t·~r ri bed earli er in sec t ion ~ 5 tc determ1n t" the gf'nerahzeJ com­ posed speci fi cation. As earlier. we ha vr to rest rict t he CBP proce­ dure in order to avoid generating d isj une" . {·sing thi s procedure. we will obtain t he following generalized composed specification,

specification J 3x 2 dx + J sin(x)dx , we see the generalization that has been achieved.

E. Step 4: Determining the Generalized Original Specification

Having obtained the generalized composed specification, the generalized original specification can be determined, once again, in either of the two ways described in section 3.6. That is , we may use the bindings obtained during the CBP computation of the generalized composed specification , or reapply the sequence of transformations used in the verification to the generalized com­ posed specification. Using either of these two ways , we will ob­ tain the following generalized original specification,

F. Step 5: Forming the new Integration method

Finally, given the generalized composed and generalized original specification as above, we can form the new integration method by defining the latter to be its precondition and the former to be its postcondition. This is shown below****

New Method:

Precondition:! {! 2 {x) + f 1 (x)}dx

Postcondition:! f 2 (x)dx + J f 1 (x)dx

V Conclusions

A . Different Perspectives for viewing VBL

We begin summarizing the VBL technique by viewing it from a number of different perspectives.

VBL as learning problem-solving methods: VBL can be described as a general technique for learning problem-solving methods. As it is an analytical generalization technique, one of its nice features is that it produces justifiable generalizations [4[, as opposed to empirical generalization techniques, such as described in [14[, which rely primarily on detecting syntactic similarities among training instances.

VBL as forming macros: Another way of thinking about what VBL does is by viewing each problem-reduction method as being constructed as a macro of the sequence of t ransformations used in the verification. In this sense VBL seems similar to earlier work on plan generalization systems like STRIPS [3[, but operating in the problem-reduction space, as opposed to the state-space. On the other hand , it is important to note that any proof technique for generating verifications can be used {provided, of course, that it meets the requirement that we imposed in section 3.4), and using a sequence of transformations is just one such scheme.

VBL as learning plans: Circuit design may be viewed as a planning problem. From this perspective each submodule becomes a planning method , and a circuit becomes a network of such methods. Given a particular plan used in a specific situation , one can generalize it by generalizing the class of situations in which exactly t he same plan cou ld be applied, which is what MAC­ ROPS did [3[. [7[ shows how this may be done for circuit design. This highlights an interesting new feature of VBL, which is the ability to generalize plans by generalizing the individual methods in the plan. For example, in section 3, the specification of the NOR gate was generalized to a negation of any boolean function, which really represents a class of possible submodules {for eg. , a NAND gate). Thus, we can describe VBL as a technique for generalizing plans by generalizing the su bgoals achieved by the in­ dividual methods constituting a given plan.

B. Limitations of the technique

We must now make clear some important requirements that need to be fulfilled in order to apply VBL to some given domain. We summarize below some of these requirements. [7[ describes, in more detail , problems that are anticipated in using this and other related techniques in real-world situations.

u··Note that this is exactly the Integral-of-a-sum method that we il­ lustrated in section I.B.

Underlying Domain Theory : The success of the VBL tech­ nique rests on its capability to construct a proof of the correct­ ness of a decomposition , which implies the existence of a strong underlying theory of the domain {such as Circuit Analysis) . Most of the theory that is needed, for example, the transfor­ mations and the ability to propagate constraints, we assume are part of a knowledge-based system on top of which the Learning Apprentice will be designed. While this is true for the specific Learning Apprentice system LEAP, there are domains, such as Well-Log Interpretat ion, where the lack of a strong underlying domain model prevents the successful application of pure analyti­ cal generalization methods [15] . This in turn motivates the need for an empirical component in the overall learning system.

Adequaey of the Verification Technique: One important ques­ tion , which directly affects the usefulness of VBL, is - how hard is it to verify arbitrary problem decompositions? It might be that a very large number of transformations are needed to cover a wide range of problems. One related issue, which we have not discussed in this paper, is the existence of multiple ways of generating verification proof·· For example, an alternative scheme for verifying the product-of-sum circuit example is that of truth trees [16[, which has certain desirable properties (such as guaranteed termination), making · the issue of control an easy one; however , these properties hold only for the restricted class of combinational circuits. More generally, we believe that construct­ ing verification proofs as a sequence of transformations is a weak but general way of approaching the verification problem. By ex­ ploiting t he properties of the particular domain (such as the func­ tional specifications of the product-of-sums circuit being boolean expressions), we may be able to come up with more powerful (and more restricted) schemes for verification.

C. Future Research Topics

We now describe some avenues for further research that we are currently exploring.

Extending Weakest Precondition Techniques: One of the problems that we described earlier had to do with the appearance of disjunctive expressions during the CBP computation. Some of the disjuncts, we said, correspond to initial situations in which it is correct, but not efficient, to use the sequence. It seems that we need more powerful analytical tools in order to learn the class of situations in which it is efficient to use a macro {as opposed to when it can be used). Work is in progress on formulating this problem within the framework of Goal-Directed Learning [4 J, by providing the system with an explicit definition of the "class of states in which it is efficient to apply a macro", and having this aid the generalization process.

Extending the notion of Verification: Although we have for­ mulated the problem of verification as one of finding a sequence of transformations, it is important to note that the concept of verification is more general , and , in the extreme, it could be viewed as a restricted form of theorem-proving. (the assertion be­ ing proved is the invariance property of problem-reduct ion methods.) Also, the connection between work on proving circuits correct , and that of generalizing problem-reduction methods seems an interesting one to pursue. In particular, we need to state more precisely the additional requirement that we imposed on proof techniques for verification - that they focus on those features that were important in order for the proof to work .

VI Acknowledgments

I thank the following people for their contributions to the form and content of this paper. Tom Mitchell , for many ideas and for greatly improving the presentation of the paper. Saul Amarel and Natesa Sridharan, for their careful reading of a draft. Lou Steinberg and other members of the Rutgers AI/ VLSI project , for many useful discussions. Smadar Kedar-Cabelli , Prasad Tadepalli and Rich Keller, for many interesting discussions on analytical learning techniques.

• [1 Mitchell , T ., Steinberg, L. and Shulman, J. "A Knowledge­ Based Approach to Design." In IEEE Principles of Knowledge-Based System·. Denver , December, 1984 .
• [2[ Barstow, D. "An Experiment 10 Automatic Programming." Artificial (1979) 73-119. Knowledge-Based Intelligence . 12:2
• [3[ Fikes, R., Hart , ing Generalized (1972) 251-288. P . and Nilsson , N. "Learning and Execut­ Robot Plans." A rtifical Intelligence . 3
• [4[ Mitchell, T. "Learning and Problem-Solving." In /JCA/-88. August , 1983, 1139-1151.
• [5[ Minton, S. "Constraint-Based Generalization ." In AAA/-8.{ Austin , Texas, August , 1984, 251-254 .
• [6[ Utgoff, P . and Mitchell, T. "Acquisition of Appropriate Bias for Inductive Concept Learning." In AAA/-8£. August , 1982, 414-417 .
• [7[ Mitchell, T. , Mahadevan, S. and Steinberg, L., "LEAP - A Learning Apprentice for VLSI Design" , to appear 10 IJCA/-85
• [8[ Amarel , S., "An Approach to Heuristic Problem-Solving and Theorem-Proving in the Propositional Calculus." In Systems and Computer Science. Univ. of Toronto Press, 1967, .
• [9[ Nilsson, ligence. N. Problem-Solving Methods McGraw-Hill , 1971. m Artificial Intel-
• [10[ deJong, G. "Automatic Schema Acquisition in a Natural Language Environment." In AAAI-8£. Pittsburgh, 1982, 410-413.
• [11[ Silver, B. "Learning Equation Solving Methods from Examples." In /JCAI-88. August , 1983, 429-431.
• [12[ Barrow, H. "Proving the Correctness of Digital Hardware Designs." In AAA/-88. Washington D.C., 1983, 17-21.
• [13[ Mahadevan, S. "Verification-Based Learning: A Generaliza­ tion Strategy for Inferring Problem-Reduction Methods.", Technical report LCSR-TR-66, Rutgers Univ , 1985.
• [14[ Porter, B. and Transformations." In 1984, 278-282. Kibler, D. "Learning AAA/-8.{ Austin, Texas, Operator August ,
• [15[ Smith, R.G., Winston , H.A., Mitchell , T.M. , and Buchanan, B.G. , "Representation, Use and Generation of Explicit Justifications for Knowledge Base Refinement", submitted to IJCA/85
• [16[ Jefferey , R. Formal Logic: Its Scope and Limit·. McGraw-Hill , 1967.