Using a Cognitive Architecture to Plan Dialogs for the Adaptive Explanation of Proofs

1 Introduction

A person who explains to another person a technical de­ vice or a logical line of reasoning adapts his explanations to the addressee's knowledge. A computer program de­ signed to take over the explaining part should also adopt this principle.

Assorted systems take into account the intended audi­ ence's knowledge in the generation of explanations (see e.g. [Cawsey, 1990; Paris , 1991; Wahlster et al. , 1993]) . Most of them adapt to the addressee by choosing be­ tween different discourse strategies. Since proofs are inherently rich in inferences , the explanation of proofs must also consider which inferences the audience can make [Horacek, 1997; Zukerman and McConachy, 1993] . However , because of the constraints of the human mem­ ory, inferences are not chainable without costs. Ex­ plicit representation of the addressee's cognitive states proves to be useful in choosing the information to con­ vey [Walker and Rambow, 1994].

While a mathematician communicates a proof on a level of abstraction that is tailored to the audience, state­ of-the-art proof presentation systems such as PRO V ERE

Drawing on results from cognitive science, we are cur­ rently developing an interactive proof explanation sys­ tem, called Prex (for proof explainer). In this paper , which extends the work reported in [Fiedler , 1998], we propose an architecture for its dialog planner based on the theory of human cognition ACT-R [Anderson and Lebiere, 1998]. The latter explicit ly represents the ad­ dressee's knowledge in a declarative memory and his cog­ nitive skills in procedural production rules. This cogni­ tive model enables the dialog planner to trace the ad­ dressee's cognitive states during the explanation. Hence, for each proof step, it can choose as an appropriate ex­ planation its most abstract justification that is known by the addressee. Moreover, the system can revise its assumptions about the user's knowledge and react to his interactions.

The architecture of Prex, which is sketched in Sec­ tion 3, is designed to allow for multimodal generation . The dialog planner is described in detail in Section 4. Since it is necessary to know some of the concepts in ACT-R to understand the macroplanning process, the cognitive architecture is first introduced in the next sec­ tion.

2 ACT-R: A Cognitive Architecture

In cognitive science several approaches are used to de­ scribe the funct ionality of the cognitive apparatus , e.g. production systems, mental models or distributed neural representations. Production systems that model human cognition are called cognitive architectures. In this sec­ tion we describe the cognitive architecture ACT-R [An­ derson and Lebiere, 1998], which is well suited for user adaptive explanation generation because of its conflict resolution mechanism. Further examples for coe;nitive architectures are SOAR [Newell , 1990] and EPIC lMeyer and Kieras , 1997].

ACT-R has two types of knowledge bases, or memo1'ies, to store permanent knowledge in: declarative and procedural representations of knowledge are explicitly separated into the declarative memory and the procedu­ ral production rule base, but are intimately connecte? .

Procedural knowledge is represented m productiOn rules (or simply: productions) whose conditions and ac­ tions are defined in terms of declarative structures. A production can only apply if its conditions are satis­ fied by the knowledge currently available in the declara­ tive memory. An item in the declarative memory is an­ notated with an activat ion that influences its retrieval. The application of a production modifies the declarative memory, or it results in an c:>bservable event. The set of applicable productions is called the conflz~t set . A co~­ flict resolution heuristic derived from a ratiOnal analysts of human cognition determines which production in the conflict set will eventually be applied.

ln order to allow for a goal-oriented behavior of the system, ACT-R manages goals in a goal stack. The cur­ rent goal is that on the top of the stack. ~nly produc­ t ions that match the current goal are apphcable.

2.1 Declarative Knowledge

Declarative knowledge is represented in terms of chunks in the declarative memory. Below is an example for a chunk encoding the fact that F ~ G, where subset-fact is a concept and F and G are contextual chunks associated to factFsubsetG .

factFsubsetG

isa subset-fact

set 1 F

set2 G

Chunks are annotated with continuous activations that influence their retrieval. The activation A; of a chunk C· consists of its base-level activation B; and the weighted activat ions of contextual ch~nks: In B; , which is defined such that it decreases loganthmtcally when C; is not used ACT-R models the forgetting of declarative knowledge.' Note that the definition o~ the activation es­ tablishes a spreading act ivation to adJacent chunks , but not fur ther; multi-link-spread is not supported.

T he constraint on the capacity of the human work­ ing memory is approached by defining a retrieval thresh­ old r , where only those chunks C; can be matched whose activation A; is higher than r. Chunks wtth an activa­ t ion less than T are considered as forgot ten.

New declarative knowledge is acquired when a new chunk is stored in the declarative memory, as is always the case when a goal is popped from the goal stack. The application of a production may also c~us~ a ne.w chunk to be stored if required by the productiOns actiOn part.

2.2 Procedural Knowledge

The operational knowledge of ACT-R is formalized in terms of productions. Prod uctions generally constst of a condition part and an action part , and can be apphed if the condition part is fulfilled. In ACT-R both I?<l:rts are defined in terms of chunk patterns. The condttton is fulfilled if its first chunk pattern matches the current goal and the remaining chunk patterns match chu~ks i.n the declarative memory. An example for a productiOn ts

IF the current goal is to show that x E Sz and it is known that X E St and St ~ s2

THEN conclude that x E 52 by the definition of~

Similar to the base-level activation of chunks, the strength of a production is defined such that it decreases logarithmically when the production is not used. The time spent to match a production with a chunk depends on the activation of the chunk . 1 It is defined such that it is negative exponent ial to the sum of the activation of the chunk and the strength of the production. Hence, the higher the activation of the chunk and the strength of the production, the faster the productiOn matches the chunk . Since the activation must be greater than the retrieval threshold r , r constrains the time maximally available to match a production with a chunk.

The conflict resolution heuristic starts from assump­ tions on the probabili ty P that the application of the current production leads to t~e goal and on the cos~s C of achieving that goal by thts means. Moreover G ts the time maximally available to fulfill the goal. The net utility E of the application of a production is defined as

We do not go into detail on how P , G an~ C are. calcu­ lated. For the purposes of this paper, tt ts sufficient to note that G only depends on the goal, but not on the production.

To sum up, in ACT-R the choice of a production to apply is as follows:

1. The conflict set is determined by testing the match of the productions with the current goal.
2. The production p with the highest utility is chosen.
3. The actual instantiation of p is determined via the activations of the corresponding chunks. If no in­ stantiation is possible (because of r) , pis removed from the conflict set and the algorithm resumes in step 2, otherwise the instantiation of pis applied .

ACT-R provides a learning mechanism, cal~ed produc­ tion compilation, which allows for the learnmg of ~ew productions. We are currently exploring this mechamsm for its utility for the explanation of proofs.

3 The Architecture of P. rex

Prex is planned as a generic explanation system that can be connected to different theorem provers. It adopts the following features of the interactive proof development environment r2MEGA [Benzmiiller et al. , 1997]:

• Mathematical theories are organized in a hierarchi­ cal knowledge base. Each theory in it. may contain axioms, definitions , theorems along wtth proofs , as well as proof methods , and control rules how to ap­ ply proof methods.
• A proof of a theorem is represented in a hierarchi­ cal data structure. This representation makes ex­ plicit the various levels of abstraction by providing several justificat ions for a single proof node, where each justification belongs to a different level of ab­ straction. The least abstract level corresponds to a

1 In this contextrtime does not mean the CPU time needed to calculate the matchr but the time a luman would need for the match according to the cognitive model.

proof in Gentzen's natural deduction (ND) calculus [Gentzen, 1935]. Candidates for higher levels are proof plans, where justifications are mainly given by more abstract proof methods that belong to the theorem's mathematical theory or to an ancestor theory thereof.

An example for a proof is given below. Each line consists of four elements (label, antecedent, succedent, and jus­ tification) and describes a node of the proof. The label is used as a reference for the node. The antecedent is a list of labels denoting the hypotheses under which the formula in the node, the succedent, holds. 2 This relation between antecedent and succedent is denoted by 1-.

We call .6. 1- <p the fact in the node. The proof of the fact in the node is given by its justification. A justifica­ tion consists of a rule and a list of labels, the premises of the node. J; denotes an unspecified justification. HYP and DefU stand for a hypothesis and the definition of U, respectively. £3 has two justifications on different levels of abstraction: the least abstract justification with the ND-rule CASE (i.e. the rule for case analyses) and the more abstract justification with the rule U-Lemma that stands for an already proven lemma about a property of U. By agreement, if a node has more than one jus­ tification, these are sorted from most abstract to least abstract .

The proof is as follows: From a E U V a E V we can conclude that a E U U V by the U-Lemma. If we do not know the U-Lemma, we can come to the conclusion by considering the case analysis with the cases that a E U or a E V, respectively. In each case, we can derive that a E U U V by the definition of U.

A formal language for specifying proofs is the interface by which theorem provers can be connected to P rex. An overview of the architecture of Prex is provided in Figure 1.

The crucial component of the system is the dialog planner. It is implemented in ACT-R, i.e. its operators are defined in terms of productions and the discourse history is represented in the declarative memory by stor­ ing conveyed information as chunks (details are given in Section 4) . Moreover , presumed declarative and proce­ dural knowledge of the user is encoded in the declarative memory and the production rule base, respectively. This establishes that the dialog planner is modeling the user.

In order to explain a particular proof, the dialog plan­ ner first assumes the user 's supposed cognitive state by updating its declarative and procedural memories. This is done by looking up the user's presumed knowledge in the user model, which was recorded during a previ­ ous session. An individual model for each user persists between the sessions.

2 As notation we use t:. and r for antecedents and <p and t/J for succedents.

The individual user models are stored in the database of user models. Each user model contains assumptions on the knowledge of the user that are relevant to proof explanation. In particular, it makes assumptions on which mathematical theories the user knows, which def­ initions, proofs, proof methods and mathematical facts he knows, and which productions he has already learned.

After updating the declarative and procedural memo­ ries, the dialog planner sets the global goal to show the conclusion of the proof's theorem. ACT-R tries to ful­ fill this goal by successively applying productions that decompose or fulfill goals. Thereby, the dialog planner not only produces a multimodal dialog plan (see Sec­ tion 4.1), but also traces the user's cognitive states in the course of the explanation. This allows the system both to always choose an explanation adapted to the user (see Section 4.2), and to react to the user's inter­ actions in a flexible way: The dialog planner analyzes the interaction in terms of applications of productions. Then it plans an appropriate response.

The dialog plan produced by the dialog planner is passed on to the presentation component. Currently, we use PROVERB's microplanner [Huang and Fiedler , 1997] to plan the scope and internal structure of the sen­ tences, which are then realized by the syntactic generator TAG-GEN [Kilger and Finkler , 1995].

An analyzer receives the user's interactions and passes them on to the dialog planner. In the current experimental stage, we use a simplistic analyzer that un­ derstands a small set of predefined interactions.

4 The Dialog Planner

In the community of NLG, there is a broad consensus that the generation of natural language should be done in three major steps [Reiter, 1994j. First a macroplan­ ner (text planner) determines what to say, i.e. content and order of the information to be conveyed. Then ami­ croplanner (sentence planner) determines how to say it , i.e. it plans the scope and the internal structure of the sentences. Finally, a realizer (surface generator) pro­ duces the surface text. In this classification, the dialog planner is a macroplanner for managing dialogs.

As Wahlster et al. argued, such a three-staged ar­ chitecture is also appropriate for multimodal generation [Wahlster et al. , 1993]. By defining the operators and the dialog plan such that they are independent of the com­ munication mode, our dialog planner plans text, graphics and speech.

Since the dialog planner in Prex is based on ACT-R, ~he plan operators are defined as productions. A goal 1s the task to show the fact in a node n of the proof. A production fulfills the goal directly by communicating the derivation of the fact irt n from already known facts or splits the goal into new subgoals such as to show the facts in the premises of n. The derivation of a fact is conveyed by so-called mathematics communicating acts (MCAs) and accompanied by storing the fact as a chunk in the declarative memory. Hence the discourse history is represented in the declarative memory. ACT-R's conflict resolution mechanism and the activation of the chunks ensure an explanation tailored to the user. The produced dialog plan is represented in terms of MCAs.

4.1 Mathematics Communicating Acts

Mathematics communicating acts (MCAs) are the prim­ itive actions planned by the dialog planner. They are derived from PROVERB's proof communicative acts [Huang, 1994]. MCAs are viewed as speech acts that are independent of the modality to be chosen. Each MCA at least can be realized as a portion of text. Moreover some MCAs manifest themselves in the graphical arrangement of the text.

In Prex we distinguish between two types of MCAs:

• MCAs of the first type, called derivational MCAs , convey a step of the derivation. An example for a derivational MCA with a possible verbalization is:

(Derive :Reasons (a E U, U ~ V) :Conclusion a E V :Method Def~)

"Since a is an element of U and U is a subset of V, a is an element of V by the definition of subset."

• MCAs of the second type, called structural MCAs, communicate information about the structure of a proof. For example, case analyses are introduced by:

(Case-Analysis :Goal ~ :Cases (ipl,lf'2)) "To prove ~. let us consider the two cases

by assuming lf'l and lf'2 ."

4.2 Plan Operators

Operational knowledge concerning the presentation is encoded as productions in ACT-R that are independent from the modality to be chosen. The proof explaining productions are derived from PROVERB's macroplan­ ning operators [Huang, 1994]. Each of those corresponds to one or several productions in P rex.

Each production either fulfills the current goal directly or splits it into subgoals. Let us assume that the follow­ ing nodes are in the current proof:

An example for a production is:

(P1) IF

The current goal is to show r 1- t/J

and R is the most abstract known rule justifying

the current goal

and ll1 1- <p1, ... ,t:.n 1- 4'n are known

THEN produce MCA (Derive :Reasons (<pl, ... ,<pn) :Conclusion t/J :Method R) and pop the current goal (thereby storing r 1- t/J in the declarative memory)

By producing the MCA the current goal is fulfilled and can be popped from the goal stack. An example for a production decomposing the current goal into several subgoals is:

(P2) IF

The current goal is to show r 1- t/J

and R is the most abstract known rule justifying

the current goal

and <I> = {<p;J.C:.; 1- <p; is unknown for 1 < i <

n} # 0

-

-

THEN for each <p; E <I> push the goal to show .C:. ; 1- <p; Note that the conditions of (P1) and (P2) only differ ~n the knowledge of the premises lf'i for rule R. (P2) mtroduces the subgoals to prove the unknown premises in tl>. As soon as those are derived, (P1) can apply and derive the conclusion.

Now assume that the following nodes are in the current proof:

Label Po HI PI H2 p2 c Antecedent Succedent r 1- 4'1 v 4'2 HI 1- 4'1 r, H1 1- t/J H2 1- 4'2 r,H2 1- t/J r 1- t/J Justification lo HYP ]I HYP h CASE( Po , P1 , P2)

A specific production managing such a case analysis is the following:

(P3) IF The current goal is to show f 1- t/J and CASE is the most abstract known rule jus­ tifying the current goal and r 1- 4'1 v 4'2 is known and r, HI 1- t/J and r, H2 1- t/J are unknown THEN push the goals to show f, H1 1- t/J and f, H2 1- t/J and produce MCA (Case-Analysis :Goal t/J

:Cases (<pi, 4'2))

This production introduces new subgoals and motivates them by producing the MCA.

Since more specific rules treat common communicative standards used in mathematical presentations, they are assigned lower costs, i.e. C(P3) < C(P2) (cf. equation 1).

Moreover, it is supposed that each user knows all nat­ ural deduction (ND) rules. This is reasonable, since ND-rules are the least abstract possible logical rules in proofs. Hence, for each production p that is defined such that its goal is justified by an ND-rule in the proof, the probability Pp that the application of pleads to the goal to explain that proof step equals one. Therefore, since CASE is such an ND-rule, P(Pa) = 1.

Before examining more closely an example explana­ tion of a proof, we look at a production reacting to a user interaction. Consider the case that the user in­ forms the system that he did not understand a step of the derivation. The analyzer receives the user 's message and pushes the goal to backtrack to the node n whose ex­ planation was not understood. This goal can be fulfilled by the following production:

(P4) IF The current goal is to backtrack to node n THEN push the subgoals tore-explain the fact inn and to revise the assumption , that the justification J used in its last explanation was known .

A further production (P5) , which is omitted here due to space restrictions , performs the revision by decreasing the base-level activation of J.

In order to elucidate how a proof is explained by Prex let us consider the following situation:

• The following nodes are in the current proof:
• CASE( La, L1 , L2)
• the current goal is to show the fact in L3,
• the rules HYP, CASE, DefU, and U-Lemma are known ,
• the fact in Lo is known , the facts in H1 , L1 , H2, and L2 are unknown.

Label Antecedent Succedent Ju stification ~ ~aEUVaEV h H1 H1 ~ a E U HYP L1 H1 ~ a E U u V Defu(Hl) H2 H2 ~ a E V HYP L2 H2 f-a E U u V Defu(H2) L3 f-a E U U V U-Lemma(Lo)

The only applicable production is (P1). Since U­ Lemma is more abstract than CASE and both are known , it is chosen to instantiate (P1) . Hence, the dialog planner produces the MCA

(Derive :Reasons (a E U V a E V) :Conclusion a E U U V :Method U-Lemma)

that can be verbalized as "Since a E U or a E V, a E U u V by the u-Lemma."

Suppose now that the user interrupts the explanation throwing in that he did not understand this step. The analyzer translates the user's interaction into the new goal to backtrack to L3 , which is pushed on the goal stack. This goal is processed by (P4) pushing the sub­ goals to re-explain the fact in L3 and to revise the as­ sumption, that U-Lemma is known. The latter is ful­ filled by (P5) by decreasing the base-level activation of U-Lemma below the ret rieval threshold. This leaves the goal to ( re-)explain the fact in L3 on the top of the goal stack.

Now, since CASE is the most abstract known rule jus­ tifying the current goal , both decomposing productions (P2) and (P3) are applicable. Recall that the conflict resolution mechanism chooses the production with the highest utility E (cf. equation 1) . Since P (P3 ) = 1 and Pp ::; 1 for all productions p, P (P3) ~ P (P2) . Since the application of (P2) or (P3) would serve the same goal,

Therefore, the dialog planner chooses (P3) for the expla­ nation, thus producing the MCA

(Case-Analysis :Goal a E UUV :Cases (a E U,a E V ))

that can be realized as "To prove a E U U V let us consider the cases that a E U and a E V ," and then explains both cases. The whole dialog takes place as follows:

R rex : Since a E U or a E Vf a E U U V by the U-Lemma. User: Why does this follow? R rex: To prove a E U U V let us consider the cases that a E U and a E V. Let a E U. Then a E U U V by the definition of U. Let a E V. Then a E U U V by the defini t ion of u.

This example shows how a production and an instanti­ ation are chosen by Prex. While the example elucidates the case that a more detailed ~xplanation is desired , the system can similarly choose a more abstract explanation if needed. Hence, modeling the addressee's knowledge in ACT-R allows Prex to explain the proof adapted to the user's knowledge by switching between the its levels of abstraction as needed.

Having in mind that the MCAs and the explaining productions are derived from PROVERB 's macroplan­ ner, it is no surprise that Prex's dialog planner produces text plan equivalent to PROVERB . But while the proof must be provided to PROVERB on an appropriate level of abstraction to satisfy the user , P rex determines for each proof step which level of abstraction it considers as the most appropriate for the respective audience. More­ over, P rex can react to interactions by the user and re­ vise both its assumptions about the addressee and its planning decisions.

5 Conclusion and Future Work

In this paper, we proposed to combine the traditional design of a dialog planner with a cognitive architecture in order to strive for an optimal user adaptation. In the interactive proof explaining system P rex, the dialog planner is based on the theory of cognition ACT-R.

Starting from certain assumptions about the ad­ dressee's knowledge (e.g. which facts does he know, which definitions, lemmas, etc.) bui lt up in the user model during previous sessions, the dialog planner de­ cides on which level of abstraction to begin the expla­ nation. Since ACT-R traces the user 's cognitive states during the explanation , the dialog planner can choose an appropriate degree of abstraction for each proof step to be explained. Furthermore, it can react to user interac­ tions and revise the user model. The rationale behind this architecture should prove to be useful for explana­ tion systems in general.

Moreover, since this architecture can predict what is salient for the user and what he can infer, it could be used as a basis to decide whether or not to include optional information [Walker and Rambow, 1994].

Prex is still in an experimental stage. It goes already beyond PROVERB's capabilities, since it can not only produce textbook style proofs but also plan explanations tailored to the respective user and react to interactions. We plan to extend the presentation component to mul­ timodality supporting graphics , text , and speech. It should consist of the following subcomponents:

A multi modal microplanner plans the scope of the sen­ tences and their internal structure, as well as their graph­ ical arrangement . It also decides, whether a graphical or a textual realization is preferred. Textual parts are passed on to a linguistic realizer that generates the sur­ face sentences. Then a layout component displays the text and graphics, while a speech system outputs the sentences in speech. Hence, the system should provide the user with text and graphics, as well as a spoken out­ put. The metaphor we have in mind is the teacher who expl ains what he is writing on the board .

Currently, we are examining the knowledge compila­ tion mechanism of ACT-R that could enable the system to model the user's acquisition of proving skills. This could pave the way towards a tutorial system that not only explains proofs, but also teaches concepts and prov­ ing methods and strategies.

Moreover, we are planning experiments with users of different levels of expertise in mathematics to evaluate the system.

Acknowledgements

Many thanks go to Jorg Siekmann , Frank Pfenning, Ken Koedinger, and Christian Lebiere for their help in my re­ search. Frank Pfenning, Carsten Schiirmann and Chris Scarpinatto read earlier drafts of this paper . I also want to thank the anonymous reviewers for their useful com­ ments.