EGS: A Transformational Approach to Automatic Example Generation

1. Introduction

Examples are important tn Artificial Intelligence . They are critical to machine lt>arning, automated reasoning, knowledge repnsentat10n , intelligent human interface. and computer-aided instruction 125. 1 ~ . i, 18. 21, 4J. Examples illustrate abstract notions and complicated procedures, provide us with a source of information on which tdeas ancl concepts are devdoped, and serve as a tool with which hypoth~ses can be validated.

Generat ing namples is. however, a difficult task in general. A problem for example generation can be specified as a constraint - a conj unctiOn of conditions each of which must be satisfied simuitaneously. Those conditions usually interact with each other in complicated ways [24J . It is often the case that ao example g~nNation system is used as a component of a larger system. In such cases, it is important that the example generator be efficient enough that it does not. detract from the performance of the larger system

Example generation differs from database retrieval or problem so!Y ing . Database retriev al deals with only the previously sorted and stored data items, wlwreas example generation often requires const.mct.ing noHI examples where known examples fail. Problem solving usually involves finding a solution or sohtions, largely ignoring the issue of finding good solutions. However , example genPration is constantly concerned with choosing good example.· from among many possibilities. This problem appears difficult to solve because it involves highly abstract notions like utility, motivation , and objective.

EGS: A Transformational Approach to Automatic Example Generation

Myung W. Kim

DPpartment of Computer Sciences University of Texas at Austin Austin, TX 78712

Automat ic example generation raises two fundamental issues: rcpre,,cn.tation and evaluation. The representation problem addresses the quest ions: what is an example and hew should it be represented; the evaluation issue deals with methods for evaluating whether and/or how well a proposed example satisfies the mitial constraint. In most cases example is not clearly defined . Evtdence, samples, models. diagrams, and even arbitrarily defined data structures are often referred to as examples. The vagueness in the meanmg of example causes difficulties in making use of the existing methodologies and tools for powerful reasoning; such reasomng appears critical to example generation. For an effective and efficient evaluation capahilit)' it is required that the involved concepts be defined unambiguously or somehow related to their effective cornput.ational proceclures. It is quite natural that an automatic example generation system should he hased on the rigorous formali'm of its problem domain .

Due t.o such difficulties, the approaches to automatic example generation in the current literatur~ are problem application specific or limited in PXpressive power . In the transformational approach examples are generated as the result. of successive transformations of the cnnst.raint formula. This approach suggests a general framework for example generation and also provides a uniform representation scheme for problems in which problem-specific procedural knowledge can be applied tf) adneve efficien~y as well .

The Example Generation System (EGS) presented here bas adopted the Boyer-Moore thPory I2J as the underlying domain formahsm . Several advantage~ are immediate.

• The Boyer-Moore theory provides a general and expressively powerful language.
• The problems of representation and evaluation can be easily solved .
• EGS can share with the Royer-Moore theorem prover , which impl~ments the Boyer-Moore theory , a substantial portion of its reasoning capability and knowledge base.
• The theorem prnv ing environment serves as a rich source of problems for applicatton or examples [7 , 18. 23. 10, llJ .

EGS. written in INTERI.ISP, cur rently running on a DEC-2060 under TOPS-20 has been trnplemented on top of the Boyer-Moore theorem provn. In EGS. a constraint is specified as a (well-formed) formula in the Boyer-Moore theory . The variables of the constraint. called con.·traint variable.· . are interpreted as existentially quantified. An example is defined as an assignment of QUOTEd con.·tant .9 to the constraint variables; this asstgnment causes tbe constraint formula to t·valuate to non-F. A counter-examplt ts similarly defined except that the assignment causes the constraint formula to evaluate to F. For instance, the assignment '((X . (QUOTE (A B)))) is an example of (LISTP X), whereas '((X . (QUOTE 3))) is a counter-example. However , '((X . (CONS U V))) IS not an example of (LISTP X) since X is assigned a non-QUOTEd constant.

The example generation problem in EGS is specified in terms of constraints. The EGS command:

FINDX ((AND (MEMBER X L) (MrnBER Y L) (NOT (EQUAL X Y) ) (EQUAL (REVERSE L) L))

NlL)

may be read as:

Find examples of lisf-paimdromes containing at least two different member.~ .

FINDX is a top-level command for example generation. Its first argument is a constraint. and its second argument specifies the resource limits such as a time limit or the maximum number of examples to be generated . The output might be: 1

((L (QUOTE (A B A))) (X (QUOTE A) ) (Y (QUOTE B))) ((L (QUOTE (C (A) C))) (X (QUOTE (A)) (Y (QUOTE C))) ((L (QUOTE (1 NIL NIL 1)) ex (QUOTE 1)) (Y (QUGTE NIL)))

2. The Boyer-Moore Theory and Their Theorem Prover

The l.loyer-Moore theory is obtained from the propositional calculus wit.h var iables and funr.tion symbols. Its three principles: t he induction principle, the shell principle, and the dcl"1nition principle charaderize the tht>ory. Variables in a formula are implicitly universally quantified . Lacking quantifiers and allowing recursion as an alternative gives rise to the constructive nature of the theory. The language of the theory can be viewed as a (functional) programming language since function definitions (admitted) are like programs. In fact. , the language of the theory is akin to that of the pure LISP.

When a function IS defined, the Boyer-Moore theorem prover generates compiled LISP code corresponding to the definition [3]. Tins provides a simple and yet efficient interpreter for the language. The interpreter. if g1ven a term together with a proper environment , will compute the term's value with respect to the environment. This r~ature , in fact .. gives a straightforward solution to the evaluatiOn problem.

1 EGS is non-detc rmini:::tir in that the outputs of EGS to the same question may vary. The n on-rlel~rrninism has been intentionally introduced; however, t.his feature can be t.urned off.

3. The Implementation of EGS

EGS has !wen implemented as task-driven in that examples are generated as the result of iterating the task :;eneration and task performing sequence. A fa~k descriptor, which describes a task , is a list of ln,ek .,rare, ta.ek operator, hnrd-list, soft-list, and reference­ list.. The hard-list is a li st of condition formulas assumed conjoined. The soft-list is an association list, each component of which is of the form (v t.) corresponding to a substitution equality 2 (EQUAL v t). The reference-list contains information needed in performing the task . For exam pie:

(78 TEST ( (MrnBER X (CONS U V)) (NOT (NUMBERP U)) (LESSP (QUOTE 7) X) (PRIME X)) ((L (CONS U V))) (CLUE (PRIME X) FLG NIL))

desnibes a TEST task. In a task descriptor , the hard-list and the soft-list together can be considered as a subgoal and we call the pair of the hard-list and the soft-list a context. In this paper subgoal and context are used interchangeably·.

Each task operation corresponds to a particular transformation of formulas . Such transformations include partially instantiating variables with constants, analyzing terms by cases, solving equations, and unfolding definitions. Simplification is a non task­ specific global transformation, which is invoked after a task-specific transformation is completed. Generally a task transforms formulas of t.he hard-list to create subgoals. Tasks are maintained in an agenda in the order of task scores; the task on the top of the agenda is performed. The result of performing a task , in turn , is further procrssed to produce more new tasks . EGS repeats this sequence until any terminat ion condition is met - the agenda becomes empty, the specified number of examples are generated , or the time limit is exc··edrd. An illust ration of EGS example generation will be given later. The task-driven structure of EGS with agenda can be viewed as best-first search. Its search space can be represented as a tree, each node of which corresponds to a task.

EC:S consists of six major functional components: Preproce.~sor . Eucutivc, Ta .. ,k Generat or, Ta sk Performer, Simplifier, and Evaluator and a global data structure Task Agenda. Also the /\"now/edge Ba'F maintains knowledge of various forms . Figure l depicts the gener:tl architecture of EGS. The function of each component is desc ribed in the following.

Preprocessor

This component checks the syntax of the input constraint and also translates the constraint, which may be input in an abbreviated format .. into the corresponding well-formed formula. For example, (AND p q r) is translated into (AND p (AND q r)).

Executive

The Executive manages the flow of control in EGS. It controls other components of EGS to maintain the proper sequence of example generation. Control loops through the task generation and task performing sequence until any termination condition is met .

2 An equality of the form (EQUAL lhs rhs) where lhs( rhs) is a variable and rhs(lh~) is a. term not. conta.ining the lh s(rhs) variable.

Task Generator

This componen t generates tasks from contexts resulting from performing a previous task . A task is generated by assigning an applir3hle task oper:ttor and attaching the collected task-relevant information to l.h<· context. This task is scored with its plausibility. The scoring algori thm is:

SCORE = (Cl * OP-SCORE) + (C2 * S·-SCORE) + (C3 * CREDIT)

OP-SCDRE : the score associated with the task operator; s --SCOR£: the score computed based on the syntactic complex1ty of the formulas in the hard-list ; CREDIT. the score for extra credit; and Cl. C2 and C3 are the weight coefficients .

Thts scoring mechanism provides EGS with substantial cont rolbhility

Task Performer

Each t.ask oprr3tor is associated with a unique process which !(CnNairs a list of suhgoals (contexts). Performing a task involves retrwving th1· relevant information and applying the process cnrre<ponrling to the task operator to the context of the task. The fullnl\ mg are the functional descriptions of the task operators .

• START marks the initial task for a single session of example generation .
• TEST rrt rievrs known examples corresponding to a clue and 1-est.s ea"h of t he examples with the bard-list until the fixed n11mh,. r of successful tests are obtained. A suhgoal for ··ach of t.he successful tests is generated.
• SOLVE inv okes t he built-m Linear Solver to solve the simul taneous linear equations/inequalities or applies the sol··cr knowledge t.o directly solve a condition or a set of cond it wns .
• ANALYZE appli<·s the· ca,,e knowledge to do case analysis.
• EXPAND opens up t he definition of a selected function in the hard-list. For an EXPAND task, each of the resulting subgoals is temporarily inactivated by making a RECAll.. task.
• ASSEMBLE reconstructs an example based on information from t.he soft-list.
• RECALL act ivates an inactive subgoal for being processed by other task operations.

Simplifier

The major functions of t he simplifier are:

1. t.o t.ransfr r sequentially each substitution equality in the bard-list onto the soft-list , after carrying out the corresponding substitution on the formulas of the hard­ list ;
2. to rewrite condition formulas on the bard-list to make them simpler and easier to handle.

The simplifier is generally invoked on each of those subgoals resulting from performing a task. Simplification possibly eliminates a subgoal or spli t-s it in to more subgoals. The resulting subgoals are t.hen subject to further processing by the task generator .

Some of the importan t advantages of simplification are as follows

• By carry ing out a global simplification, the simplifier relieves the t-ask generator of the need to care about mundane details.
• By normali zing formulas , the simplifier allows tbe task generator to he ahle to relatively easily predict tbe patterns of formulas to be encountered .
• By eliminati ng apparently unsat isfiable subgoals , tbe simplifier enables EGS to focus more on the promising ones.
• The fact that t he simplifier makes use of rewrite lemmas provides EGS with some degree of extensibility .

Evaluator

This component evaluatl's bow well the proposed examples satisfy the initial constraint . This evaluation function would be important for the system to he able to learn or self-organize from experience. Currently it only JUdges whether a proposed example satisfies the initial const raint..

4. The Knowledge Base of EGS

EGS's abi lity to generate examples critically depends on 1ts knowledge base. EGS employs various forms of knowledge: heurist ic information , definitions, theorems , known examples, and equatton solvers in the form of production rules, etc. Under each concept (function) name, knowledge is frame-structured . Know(P,dge is divided into the knowledge shared with the Boyer-Moore t h~or<'m prover and F::GS-specific knowledge (boxed under X- FRAME in F1gure 2).

Dennttlons and LISP Code

When a function is bring defined . the Boyer-Moore system generates LISP code, wh ich implements the defined function in the runnmg LISP environment [ :~J - This code is invoked when a term is evaluat.cd . EvaiHal.tn)l terms is extensively required when a TEST task is performed or a proposed nample is verified by the evaluator .

The symbolic definitions of functions are also important. Performing an EXP AI'\D task retrieves the definition of a selected function and expands the corresponding function call in the hard-list with the defin itiOn. By appealing to the symbolic definitions , EGS is able to generate examples for constraints which are very restrictive or involve nov~! concepts.

CONCFPT -NAME:

Lemmas

In th~ noyPr-Moore theorem prover lemmas are proved and stored under their hy function names with the user-assigned types. The EGS simplifier makes use of rewrit e type lemmas when it rewrites terms

Known Examples

Known examples are important knowledge to EGS because they play the role of building blocks for generating examples. Generated examples are often simply known examples or , at least, constituted of known examples . Rich and well-sorted known examples substantially increase the dficiency of EGS and make the system behave more naturally . Known examples are used when a TrnT task is performed.

In EGS, for a given function a known example is represented as a list of QUOTEd constants - actually stored unQUOTEd - each of which corresponds to a formal argument of the function . Known examples for a function are classified into three types: Typical, Boundary, and Counter. Known examples for MEMBER can be represented as:

(EXAMPLES (TYPICAL (A (A 8 C)) (4 (7 3 4 . 5)) ((C) (A 8 (C) (D))) (B ((0) A 9 8 G)) ((E F) (M N (E F) 6))) (BOUNDARY (*) (A (A)) (NIL (NIL NIL NIL)) (C (C . C))) (COUNI"ER (E E) (NIL 8) (6 (2 4 7 5)) (8 (A . B)) (D (A 8 C)))) .

Currently known examples must be sorted and given by the user . This, however, has advantages in that generated examples are more user-tun~d .

Solvers

A solver is user-supplied , procedurally attached. production rule-like knowledge whose action part transforms a formula, possibly a set of formulas, into a form which is simpler and easier to hand!~ . For example, a formula: (EQUAL (REVERSE L) (QUUI'E (A 8 C))) can be directly transformed into: (EQUAL L (REVERSE (QUUTE (A B C)))) . The built-in linear solver is a special solver for simultaneous linear equations/inequalities. Solvers are specific to the patterns of formulas and often heuristic; however, they are efficient. The solver knowledge substantially increases the efficiency of EGS.

5. A Simple Illustration of EGS Example Generation

Suppose the following command is typed in: FINDX ((AND (!IDlBER X L) (LESSP X Y) (LESSP Y (CAR L) ) ) NIL) . 1. The preprocessor translates the input constraint into: (AND (IIDlBER X L) (AND (LESSP X Y) (LESSP Y (CARL)))) . ((O START ((AND (!IDlBER X L) (AND (LESSP X Y) (LESSP Y (CAR L)))) )

2. A START task is initiated . The task agenda would be· NIL NIL)) . 3. The START task is performed and the re&ulting subgoal is simplified to produce a new subgoal: (( (IIDlBER X L) (LESSP X Y) (LESSP Y (CAR L))) NIL). 4. The task generator is invoked with the subgoal and gcnNates new tasks; the task agenda would be then : ((76 TEST ((!IDlBER X L) (LESSP X Y) (LESSP Y (CAR L))) NIL (CLUE (!IDlBER X L) FLG NIL)) (74 TEST ((!IDlBER X L) (LESSP X Y) (LESSP Y (CAR L))) NIL (CLUE (LESSP X Y) FLG NIL)) (33 ANALYZE ( (IIDlBER X L) (LESSP X Y) (LESSP Y (CAR L) ) ) NIL (CLUE (L CAR))) ( -9000 EXPAND ( (AND (IIDlBER X L) NIL NIL)) . (AND (LESSP X Y) (LESSP Y (CARL)))))

1. The t.op task is processed . The task performer retrieves !IDlBER 's typical and boundary stored examples - let 's assume !IDlBER 's stored examples are given as (*) -and tests them with the hard-list i.e. evaluates each of condition formulas in the hard-list under the environment es tablished by associating the CLUE arguments with the corresponding values in an example. Only the example (4 (7 3 4 . 5)) survives the test; in

Constramt

Examples 3

(SUBBAGP X (DEI.EI'E U Y)) (NOT (EQUAL (IMPLIES P (IMPLIES Q R)) (IMPLIES (IMPLIES P Q) R))) ( (U 1) ex B) (Y . NIL)) ( (U C) ex . (A B)) (Y . (C C B A))) c cu 3) ex . C2)) cY . c2 3 5))) ((P ((P ((P !FALSE) (Q 1FALSE) (Q 1FALSE) (Q 1 TRUE) (R . 1 FALSE) ) NIL) (R . 1 FALSE) ) 2) (R . 1FALSE)) (AND (MDIBER X Y) (MDIBEll. Y Z)) ((X A) (Y (A)) (Z (A (A)))) ((X A) (Y (B A B)) (Z . (A (B A . B) B C))) ((X 2) (Y (3 2)) (Z . ( (3 2) A B))) (AND (ORDERED L) (NOT (EQUAL (SORT L) L))) (AND (MDIBEll. ' P L) (MDIBEll. , Q L) (EQUAL (REVERSE L) L)) (AND (NUMBEll.P Z) (PRIME X) (NOT (DIVIDES X Z)) (EQUAL (TIMES X K) (TIMES B Z))) (AND (PRIME P) (PRIME Q) (NOT (EQUAL P Q)) (EQUAL (REMAINDER A P) (REMAINDEll. B P)) (EQUAL (REMAINDER A Q) (REMAINDEll. B Q)) (NUMBEll.P B) (LESSP 8 (TIMES P Q))) ((L (ABC))) ((L (3 5 7 . 2))) ((L (P Q P))) ((L (Q p Q))) ((L (P Q Q P))) ((8 15) CK . 20 ex . 5) (Z 7)) ((B 18) (K 3o) ex . 3) (Z :;) ) ((8 5) (K 3) (X 5) (Z 3)) ((A 43) (8 . 3) (P . 5) (Q . 2)) ((A 37) (8 . 1) (P . 2) (Q . 3)) ((A 9) (8 . 3) (P . 2) (Q . 3))

the case that none of the examples succeed, EGS would appeal to other types of tasks, for example, definition expansion. The subgoal produced after simplification is:

(((LESSP (QUOTE 4) Y) (LESSP Y (QUOTE 7))) ((L . (QUOTE (7 3 4 . 5))) ex . (QUOTE 4)))) .

1. The above subgoal gives rise to several new tasks and t he top task wou ld be:
2. To perform the SOLVE task , the built-in linear solver is invoke<l . As the result Y gets '(QUOTE 6) and further simplification yields a new subgoal :
3. Only an ASSE11BLE task is generated with the subgoal and it would IJr the highest scored task:
4. The ASSE11BLE task constructs an example:
5. This example is verified by t he evaluator. More examples would possibly he generated by continuing the similar procedure of performing and generating tasks.

(82 SOLVE ( (LESSP (QUOTE 4) Y) (LESS! Y (QUOTE 7))) ((L . (QUOTE (7 3 4 . 5))) (X . (QUOTE 4) )) (MODE LI NEAR POLY.LST ((-5 ((Y . - 1)) LEQ) (6 ((Y . 1)) LEQ)))) .

(NIL ( (Y (QUOTE 6)) (L (QUOTE (7 3 4 . 5))) (X (QUOTE 4)))) .

(10000 ASSE11BLE NIL ((Y . (QUOTE 6)) (L . (QUOTE (7 3 4 . 5))) ex CQUOTE 4))) (TEMPLET (LX Y))) .

((L . (QUOTE (7 3 4 . 5))) (X (QUOTE 4)) (Y .. (QUOTE 6)))

6. Related Work and Future Research

Examples have long been used for many A.I. tasks , especially for machine learning [l :l , 14 . 2.)[. However , very few learn ing system ran generate cxampl<'s by themselves and often examples are given by the user int r radively or are stored initially in the system. Lenat's AM [l :l[ lacks reasoning for example generation, therefore , its example generation capabili ty is limited. AM generates examples for a concept simply by execut ing the algorit hmic specification ( a LISP-like program) of the concept with the known exampl(·s. Grlernter [7 . 8j experimented with the idea that humans almost a lways draw diag rams when trying to prove geometry theorems. In his geometry machine, Gelernter used diagrams to prune the backward chaining during the proof search . The use of diagrams in t his way r~d uccd t.h~ proof search many orders of magnitude. CEG [20[ is a ~-ph~se st.ructurcd example generation system over the domain of LISP d~ta and programs. In CEG, a constraint is ~Jwcified in t.h r form of a set of desired property-value pairs . CEG's express ive power and abilit.y in problem handling are limited. Moreover , its me::11"-ends analysis method for example mod ification may not be 'uitablc for cases where moderate expressive power is r~quired. lla ll ~n ty ne and Bledsoe's CRAP HER [lJ generates counter-examples for non-trivial topological conjectures. Given a conj~cture, GHAF'IIEH const ructs a set-theoretic relationship graph among the set Yariables occurring in the conjecture. The graph ~erve~ as a 1\lobal const ra int spec ification when the set variables are as<i)\n~d v al u~s . nr-:F-AHF j6J employed the constraint-satisfaction tl·chni<]·te. REF-AHF was able to solve admittedly difficult problems such as cryptoarithmetic problems and the 8-queens problem. The regre.·.·ion method for plan modification [24], proposed by Waldinger ran also he useful fnr example generation . Green 's QA3[9J and the PUOLOG intt·rprett·r [15J a re both driven by resolution-based theorem proving, howeve r. they can ha rdly be classified as example generators in l heir own right.

3 11ere Px;~:mplPs arP print.ed wit.hout "QUJTE" . For most ca.ses the shown f'Xamples have Ueen gpnera t ed well within 10 seconds or CPU time.

E\peri rnent s haH been rarricd out applying EGS to the problems of cont rolling backward cltaining in the Boyer-Moore theorem prover and semantically dtrcking con jectures by way of finding counter­ namples. The'c nperirnents ha,·e shown EGS to be powerful and efficient. Howe,·cr, seve ral improvements are still needed ; the following only drsnilws those projected for the near future :

• incorporating a simple learning capability - updating the stored examples in favor of better examples through evaluating and classifying experienced examples:
• devisin 11 a high-leHI con trol mechanism for dynamically adjusting the task score computation - for example. the t.ask t.rre . "hic·h rcp rrsrnts the derivational relationship of tasks. ran be usP<I to even ly distribute examples:
• ex tending and elaborating the knowledge base;
• enriching the user int <· rface facility.

Integration of EGS into the Iloyer-Moore theorem prover is a lso bring considered. Thts would result in a user-friendly environment fur theory development where examples can play an invaluable role.

7. Conclusions

In this paper . a nrw approach to automatic example generation and its implrmcnt at inn have bern presented . The transformational approach has sner:il advantages.

• It suggests a general paradigm for example generation. In this approach, rxample generation is viewed as t,ransformation from a constraint spec ification to a representation which conforms to an example description scheme - the substitution equality for EGS. This view provides flexibility in se lecting representation schemes for constraints and examples.
• The problems of representation and evaluation can rebtively easily be solved.
• It enables general formal reasoning and problem-specific procedural knowledge t.o cooperate with each other to achieve both generality and efficiency .
• It prov ides mod ifiability and controllability of the system.

Considering the important role examples play in human intelligence and in A.l. as a study of computer simulation of human intelligence, the author belieVPs that bet.tn understanding of the true nature of fXI!mple.s will lrad us to greatly enrich contemporary A.l. research .

ACKNOWLEDGEMENTS

I wou ld like to thank Dr. Robert Boyer and Dr . .J Moore for their invaluable advice and support. I owe much tha1·:;s to Prof. W. W. 13ledsoe for his encouragement. My gratitude also goes to William Young , who pat.iPntly proofread the original draft. Dr . Donald Good generously permitted me the use of space and resources for the preparation of this paper.