Proof Verbalization as an Application of NLG

1 Introduction

PROVERB is a text planner that verbalizes natural deduction (ND) style proofs [Gentzen, 1935; Huang, 1994b). Several similar attempts can be found in previ­ ous works. The system EXPOUND [Chester, 1976) is an example of direct translation: Although a sophisticated linearization is applied on the input ND proofs, the steps are then translated locally in a template driven way. ND proofs were tested as inputs to an early version of MUM­ BLE [McDonald, 1983), the main aim however, was to show the feasibility of the architecture. A more recent attempt can be found in THINKER [Edgar and Pelletier, 1993), which implements several interesting but isolated proof presentation strategies. PROVERB therefore can be seen as the first serious attempt to build a compre­ hensive system that produces adequate argumentative texts from ND style proofs.

Although a multitude of architectures have been proposed for NLG systems, PROVERB employs a pipe line architecture consisting of three parts, like most application-oriented systems. The architecture of PROVERB is illustrated in Fig. 1 1 .

·xiaorong Huang's current email address is: xMIFormalSys.ca

1 In the field of NLG the first two components are called "planners," since they make decisions that will be executed

The macroplanner of PROVERB accepts as input a natural deduction style proof, and produces proof com­ municative acts which are structured into hierarchical attentional spaces. To do so, it uses a strategy which combines hierarchical planning and focus-guided naviga­ tion.

More detailed linguistic decisions are made by the microplanner. It makes reference choices, chooses be­ tween linguistic resources for domain concepts, combines and reorganizes such resources into paragraphs and sen­ tences. As the representation which supports all these operations, the microplanner of PROVERB adopts a variation of Meteer's Text Structure, which is also its output.

Our realizer, TAG-GEN, is a syntactic generator based on the grammar formalism TAG [Kilger and Finkler, 1995).

Section 2 and Section 3 are devoted to the macroplan­ ner and the microplanner, respectively. Section 4 con­ tains a complete example. Finally, we shall conclude this paper with a discussion in Section 5.

by the realization component. Many approaches differ signif­ icantly from general definitions of planner in AI. In particu­ lar, approaches towards microplanning often resemble more rule-based systems.

2 Macroplanning: Hierarchical Planning and Focus-Guided Navigation

Most current text planners adopt a hierarchical plan­ ning approach [Hovy, 1988; Moore and Paris, 1989; Dale, 1992; Reithinger, 1991]. Nevertheless there is psychological evidence that language has an unplanned, spontaneous aspect as well [Ochs, 1979]. Based on this observation, Sibun [Sibun, 1990] implemented a system for generating descriptions of objects with a strong do­ main structure, such as houses, ships and families. While a hierarchical planner recursively breaks generation tasks into subtasks, local organization navigates the domain object following the local focus of attention.

PROVERB combines both of these approaches within a uniform planning framework [Huang, 1994a]. The hi­ erarchical planning splits the task of presenting a partic­ ular proof into subtasks of presenting subproofs. While the overall planning mechanism follows the RST-based planning approach [Hovy, 1988; Moore and Paris, 1989; Reithinger, 1991], the planning operators more resem­ ble the schemata in schema-based planning [McKeown, 1985; Paris, 1988]. Local navigation operators simulate the unplanned aspect, where the next conclusion to be presented is chosen under the guidance of a local focus mechanism.

The two kinds of planning operators are treated dif­ ferently. Since hierarchical planning operators embody explicit communicative norms, they are given a higher priority. Only when none of them is applicable will a local navigation operator be chosen.

2.1 Proof Communicative Acts

Proof communicative acts (PCAs) are the primitive ac­ tions planned by the macroplanner of PROVERB. Like speech acts, they can be defined in terms of the commu­ nicative goals they fulfill as well as their possible verbal­ izations. An example of a simplistic one conveying the derivation of a new intermediate conclusion is the PCA

(a EF, F ~�)

(Derive Reasons: Method: def-subset Conclusion: a EG)

Depending on the reference choices, the following is a possible verbalization:

"Since a is an element ofF and F is a subset of G, a is an element of G by the definition of subset."

There are also PCAs that predicate actions planned for further presentation and thereby update the global attentional structure. For instance, the PCA

creates two attentional spaces with A and B as the as­ sumptions, and Formula as the goal by producing the verbalization:

"To prove Formula, let us consider the two cases by assuming A and B."

2.2 Hierarchical Planning

Hierarchical planning operators represent communica­ tive norms concerning how the task of presenting a proof can be split into subtasks of presenting subproofs, and how the subproofs can be mapped onto some linear or­ der. Let us look at one such operator, which handles the goal of presenting a proof by case analysis. The corresponding schema of such a proof tree is shown in Fig. 2, where the subproofrooted by ? £4 leads to F V G, while sub proofs rooted by ? £ 2 and ? £3 are the two cases proving Q by assuming F or G, respectively. The appli­ cability encodes the two scenarios of case analysis, where we do not go into details. In both circumstances this op­ erator first presents the part leading to F V G, and then proceeds with the two cases. It also inserts certain PCAs to mediate between parts of proofs. This procedure is captured by the planning operator below (note that the verbalizations given are only one possible paraphrase):

Case-Implicit

• Precondition: ((task ?LI) V (local-focus ?£4)) 1\ (not-conveyed (?£2 ?£3))
• Acts:
• if? £ 4 has not been conveyed, then present? £ 4 (sub­ goal 1)
• a PCA with a verbalization: "First, let us consider the first case by assuming F."
• present ? £2 (subgoal 2)
• a PCA with a verbalization: "Next, we consider the second case by assuming G."
• present ? £3 (subgoal 3)
• mark ? £1 as conveyed
• features: (hierarchical-planning compulsory implicit)

The slot features indicates that this is a higher prior­ ity operator (compulsory) and should be chosen when a more implicit style is preferred by the user.

2.3 Planning as Navigation

The local navigation operators simulate the unplanned part of proof presentation. Instead of splitting presenta­ tion goals into subgoals, they follow the local derivation relation to find a proof step to be presented next .

The Local Focus The node to be presented next is suggested by the mechanism of local focus. In PROVERB, our local focus is the last derived step, while focal centers are semantic objects mentioned in the lo­ cal focus. Although logically any proof node which uses the local focus as a premise could be chosen for the next step, usually the one with the greatest semantic overlap with the focal centers is preferred. In other words, if one has proved a property about some semantic objects, one will tend to continue to talk about these particular ob­ jects, before turning to new objects. Let us examine the situation when the proof below is awaiting presentation.

Assume that node [1] is the local focus, {a, b} is the set of focal centers, [3] is a previously presented node and node [5] is the current task. [2] is chosen as the next node to be presented, since it does not (re)introduce any new semantic objects and its overlap with the focal centers ({a,b}) is larger than the overlap of [4] with the focal centers ( { b}). Due to space restrictions, no navigation operators are discussed in detail.

3 Microplanning: Choosing and Organizing Linguistic Resources

Many of the first NLG systems link their information structure to the corresponding linguistic resources either through predefined templates or via careful engineer­ ing for a specific application. Therefore their expressive power is restricted (see [Meteer, 1992] for an extensive discussion). First experiments with PROVERB using a simplistic microplanning mechanism resulted in very me­ chanical texts. According to our analysis, there are at least two linguistic phenomena that call for appropriate microplanning techniques.

3.1 Why is Microplanning Needed?

First, naturally occurring proofs contain paraphrases with respect to rhetorical relations, as well as to logi­ cal functions or predicates. For instance, the derivation of B from A can be verbalized as:

The logic predicate para(C1 , C2), also, can be verbalized as:

"The parallelism of the lines C1 and C2."

Second, without microplanning PROVERB generates text structured mirroring the information structure of the proof and the formulae. This means that every step of derivation included by the macroplanner is translated into a separate sentence, and formulae are recursively verbalized. As an instance of the latter, th~ formula

is verbalized as

"F is a set . . F is a subset of G."

although the following is much more natural:

"The set F is a subset of G."

Therefore, we came to the conclusion that an inter­ mediate level of representation is necessary that allows for flexible combinations of linguistic resources. In Sec­ tion 3.2 we describe how Meteer's Text Structure can be adopted as our central representation. Sections 3.3 and 3.4 are devoted to paraphrases and aggregation rules, two of the major tasks of our microplanner.

3.2 Text Structure in PROVERB

Text Structure was first proposed by Meteer [Meteer, 1992] in order to bridge the generation gap between the representation in the application program and the lin­ guistic resources provided by the language. Meteer's Text Structure is organized as a tree, in which each node represents a constituent of the text and is typed in terms of semantic categories.

The main role of the semantic categories is to provide vocabularies which specify type restrictions for nodes. They define how separate Text Structures can be com­ bined, and ensure that the planner only build express­ ible Text Structures. For instance, if tree A should be expanded at node n by tree B, the resulting type of B must be compatible to the type restriction attached to n. Following Panaget [Panaget, 1994], however, we split the type restrictions into two orthogonal dimensions: the ideational dimension in terms of the Upper Model [Bate­ man et al., 1990], and the hierarchy of textual semantic categories to be discussed below. Technically speaking, the Text Structure in PROVERB is a tree recursively composed of kernel subtrees or composite subtrees:

An atomic kernel subtree has a head at the root and arguments as children, representing basically a predi­ cate/argument structure.

Composite subtrees can be divided into two subtypes: the first has a special matrix child and zero or more adjunct children and represents linguistic hypotaxis, the second has two or more coordinated children and stands for parataxis.

Each node is typed both in terms of the Upper Model and the hierarchy of textual semantic categories. The Upper Model is a domain-independent property inher­ itance network of concepts that are hierarchically or­ ganized according to how they can be linguistically ex­ pressed. Fig. 3 shows a fragment of the Upper Model in PROVERB. For every domain of application, domain­ specific concepts must be identified and placed as an extension of the Upper Model.

The hierarchy of textual semantic categories is also a domain-independent property inheritance network. The concepts are organized in a hierarchy based on their textual realization. For example, the con­ cept clause-modifier-ranking! is realized as an adverb, clause-modifier-rankingll as a prepositional phrase, and clause-modifier-embedded as an adverbial clause. Fig. 4 shows a fragment of the hierarchy of textual semantic categories.

3.3 Paraphrasing in PROVERB

The mapping from the content to the linguistic resources now happens in a two-staged way. While Meteer asso­ ciates the application program objects (APOs) directly with so-called resources trees, we map APOs into Upper Model objects, which in turn are expanded to the Text Structures. A practical advantage of this two-stadged process is worth noting. Instead of having to construct resource trees for APOs, the user of our system only needs to define a mapping from the APOs to Upper Model objects (UMOs).

When mapping APOs to UMOs, the microplanner must choose among available alternatives. For exam­ ple, the application program object para, that stands for the logical predicate denoting the parallelism relation between lines, may map in five different Upper Model concepts. In the 0-place case, para can be mapped into object leading to the noun "parallelism," or quality, lead­ ing to the adjective "parallel." In the binary case, the choices are property-ascription that may be verbalized as "x and y are parallel," quality-relation that allows the verbalization as "x is parallel to y", or process-relation, that is the formula "x II y ."

The mapping of Upper Model objects into the Text Structure is defined by so-called resource trees, i.e. reified instances of Text Structure subtrees. The alternative resource trees of an Upper Model concept are assembled in its realization class.

With the help of a concrete example we shall illustrate how the Text Structure generator chooses among para­ phrases and avoids building inexpressible Text Struc­ tures via type checking.

Example We examine a simple APO derive(para(Cl,C2) ,B) . Note that B stands for a conclusion which will not be examined here.

In the current implementation, the rhetorical relation derive is only connected to one Upper Model concept derive, a subconcept of cause-relation. The realization class associated to the concept, however, contains sev­ eral alternative resource trees. The verbalization of two variations is listed below:

• B, since A.
• Because of A, B.

The resource tree of the first alternative is given in Fig. 5.

The logic predicate para(Cl, C2) can be mapped to one of the following Upper Model concepts, where we always include one possible verbalization:

• quality-relation(para, Cl , C2) (line C1 is parallel to C2)
• process-relation(para, Cl, C2) (C1IIC2)
• property-ascription(para, Cl/\ C2) (lines C1 and C2 are parallel)

The property-ascription version, in turn, can be realized in two forms, represented by the two resource trees in Fig. 6.

Figure 6: Textual Variations in form of Resource Trees

Type checking must ensure that the constructed Text Structure be compatible along both the ideational and the textual dimension. In this example, the combina­ tion of the tree in Fig. 5 and the first tree in Fig. 6 is compatible and will lead to the verbalization:

"B, since C1 and C2 are parallel."

The second tree in Fig. 6, however, can only be combined with another realization of derive, resulting in:

"Because of the parallelism of line C1 and line C2, B."

In our current system we concentrate on the mecha­ nism and are therefore still experimenting with heuristics that control the choice of paraphrases. One interesting rule is to distinguish between general rhetorical relations and domain specific mathematical concepts. While the former should be paraphrased to increase the flexibility, consistency of the latter helps the user to identify tech­ nical concepts.

3.4 Aggregation

Although paraphrase generation already increases the flexibility in the text, the default verbalization strategy will still expand the Text Structure by recursively de­ scending the proof and formula structure, and thereby produces linguistic structures isomorphic to that of a formula. To achieve the second verbalization of equa­ tion (1) in Section 3.1, however, we have to combine Set( F) and Subset(F, G) to form an embedded struc­ ture Subset(Set(F), G). This textual operation elimi­ nates one of the duplicates of F. We call it aggregation.

Aggregation rules operate on APOs, which, before mapped to UMOs, can be viewed as variables for UMOs (for convenience, we continue to refer to them as APOs). For instance, the embedded structure Subset( Set( F), G) documents a textual decision that no matter how Subset and Set are instantiated, the argument Fin Subset(F, G) will be replaced by Set(F). In this sense, our rules work with such variables at the semantic level of the Upper Model. So far, we have investigated three types of ag­ gregation, as illustrated in Fig. 7.

Semantic Grouping We use semantic grouping to characterize the merge of two parallel Text Structure objects with the same top-concept by grouping their ar­ guments. Two APOs are parallel in the sense that they have the same parent node. The general form of this type of rules can be characterized by the pattern as given below:

Rule Pattern A

P affib]

P[al + P[b]

The syntax of our rules means that a Text Structure of the form above the bar will be transformed into one of the form below the bar. Viewing Text Structure as a tree, P[a] and P[b] are both sons of+, they are merged together by grouping the arguments a and b under an­ other operator EB· In the first rule below, + and EB are identical.

Rule A.l (Predicate Grouping)

where + can be either a logical 1\ or a logical V, and P stands for a logical predicate. The following example

P[ar + Pfbl Pa+b illustrates the effect of this rule. Set(F) 1\ Set( G) "F is a set . G is a set." are aggregated to: Set(F 1\ G) "F and G are sets."

The rule covers the predicate grouping rule reported in [Dalianis and Hovy, 1993]. This is also the best place to explain why we apply aggregation before choosing con­ crete linguistic resources. If the two occurrences of Set are instantiated differently, this rule will be blocked.

By instantiating +, EB and P in pattern A to differ­ ent logical connectives and derivation relations, we have altogether five rules in this category. The correctness of the rules in this category with respect to the infor­ mation conveyed is guaranteed by the semantics of the corresponding Upper Model.

Semantic Embedding The next category of aggre­ gation rules handles parallel structures which are not identical. In this case, some of them may be converted to embedded structures, as is done by the following rule.

Rule B.l (Object Embedding)

We will not discuss the preconditions of this rule in detail, but only illustrate its effect by an example. Get­ ting as input two APOs in a conjunction that contain a common APO F:

Set( F) 1\ Subset(F, G)

"F is a set and F is a subset of G."

rule B.1 aggregates them by removing one redundant F : Subset(Set(F), G)

"The set F is a subset of G."

Actually, for mathematical texts we have only used two embedding rules, the other being the dual of rule B.1 where P and Q change their places.

Pattern-based Optimization rules Rules in the third category involve more complex changes of the textual structure. They could be understood as some domain-specific communicative conventions, and must be explored in every domain of application. See [Fiedler, 1996] for details.

4 A Complete Example

In this section, we present a short example of PROVERB's output. The input is a machine-found proof for a theorem taken from a mathematical text­ book. A user may choose the style of the output text by tuning two parameters: implicit vs. explicit, abstract vs. detailed. Given abstract and explicit as options, the macroplanner generates the following sequence of PC As:

(THEOREM Reasons (group(F, * ), subgroup(U, F, *), unit(F, 1, * ), unit(U, 1u , * )) , Conclusion 1u == 1) (PROOF) (ATTENTION-BEGIN) (ASSUME Conclusion group(F,*)) (ASSUME Conclusion subgroup(U,F, *)) (ASSUME Conclusion unit(F, 1, * )) (ASSUME Conclusion unit(U, 1u, * )) (ATTENTION-BEGIN) (ATTENTION-BEGIN) (DERIVE Reasons unit(U, 1u, *), Conclusion (DERIVE Conclusion 3x.x EU) (ATTENTION-END) (BEGIN-ASSUME-CHOICE-1 Conclusion U1 EU, (ATTENTION-BEGIN) Parameters u1 , x) (DERIVE Reasons group(F,+), Conclusion semigroup(F, * )) (DERIVE Conclusion 1u == 1) (ATTENTION-END) (END-ASSUME-CHOICE-1 Conclusion 1u = 1, Parameters U1) (ATTENTION-END) (ATTENTION-END) (QED) 1u EU)

Note that the PCAs are segmented into a hierarchy of attentional spaces, which is used to make reference decisions [HtJ.ang, 1997]. The microplanner maps this se­ quence of PCAs via Upper model objects into a Text Structure, which is used as linguistic specification of the text. It also aggregates Upper Model objects and paraphrases the concepts by combining various resource trees. Finally, our realization component TAG-GEN produces the following text:

Theorem:

Let F be a group, let U be a sul>group ofF, and let 1 and 1u be unit elements ofF and U. Then 1u equals 1. Proof:

Let F be a group, let U be a subgroup ofF, and let 1 and 1u be unit elements ofF and U.

Because 1u is an unit element of U, 1u E U. Therefore, there is x such that x E U.

Let u1 be such an x . Since u1 E U and 1u is an unit element of U, u1 * 1u = u1 . Since F is a group, F is a semigroup. Since U is a subgroup ofF, U C F. Because U C F and 1u E U, 1u E F . S1milarly, because u1 E U and U C F, u1 E F . Then, 1u is a solut10n of u1 * x = u1 .

Because u1 E F and 1 is an unit element ofF, u1 * 1 = u1. Since 1 is an unit element of F, 1 E F. Then, 1 is a solution Of U1 *X= U1 .

Therefore, 1u equals 1. This conclusion is independent of the choice of u1 . ·

Please note the variation in the text, in the structure of the sentences, and in using mathematical symbols vs. words. Moreover aggregation techniques reduced redun­ dancies as in the sentence "let 1 and 1u be unit elements ofF and U."

5 Outlook

This paper examines PROVERB as an integration of so­ phisticated linguistic technologies for a concrete applica­ tion. The system works particularly well with textbook size examples and runs fully automatically for every new example. The output texts are close to detailed proofs in textbooks and are basically accepted by the community of automated reasoning. To benefit from the microplan­ ing techniques which significantly improve the fluency of text, however, linguistic resources must be introduced with each new domain of application. We are working on an interface to simplify this process.

Although developed for a specific application, we be­ lieve the main rationales behind of our system ar­ chitecture are useful for natural language generation in general. The combination of hierarchical planning with focus-guided navigation provides an effective way of factoring out domain-dependent presentation knowl­ edge from more general NLG techniques. While the macroplanning operators are designed for this specific domain, the framework and the rules of our microplan­ ner represents domain-independent techniques.

With the increase of the number of examples tested, some of them over several pages, our experience already suggests some immediate adjustment and improvement of the techniques and strategies, in particular concerning the linearization in macroplanning, heuristic threshold values for discourse segmentation and reference choices, and the treatment of articles.