Learning University Mathematics

1. Introduction

Learning University level Mathematics is a complex task for both people and machines and difficult to model for three main reasons:

1. Students can learn any branch of mathematics, and mathematics is continually developing. Any learning model therefore has to be open in its representation.
2. Pure Mathematics is a very large domain over 2000 years old, and this means that a large amount of knowledge has to be acquired.
3. Understanding Mathematics Proofs and solving problems requires the ability to be able to retrieve the appropriate result ·at each step, and this expertise only comes with experience.

The Mathematics Understander (MU), [Furse, 1994] is a computational model of how students learn Pure Mathematics from texts written in a notation known as the Formal Expression Language (FEL), [Furse, 1990]. FEL is a very expressive language and capable of representing almost all branches of pure mathematics. MU has read texts in both Classical Analysis and Group Theory. An extract from an FEL text is shown in Figure 1, where a definition, theorem and proof are shown in Classical Analysis.

MU has no built in knowledge of mathematical results, and acquires all its knowledge from the reading of texts. This knowledge is of two sorts:

1. The mathematics results: definitions of concepts, theorems and lemmas.
2. Features which index the mathematical results, and enable easy retrieval of the appropriate result.

The features provide an open form of representation thus enabling MU to learn in an open domain [see Furse, 1993].

Learning University Mathematics

Edmund Furse

Department of Computer Studies University of Glamorgan Pontypridd, Mid Glamorgan CF371DL UK efurse@uk.ac.glamorgan

Definition 2.4 of converges «s >>converges to a iff Vc. > 0 3m Vn > m I s - a I < f. n n Lemma 2.1.1 not («(-1t>> converges to 1) Proof 1 RIP not («(-1t>> converges to a) 2 Suppose to the contrary «(-1t>> converges to 1 3 => Vc. > 0 3m Vn > m I (-lt- 1 I < c. by definition of converges 4 ::::>3m Vn > m I (-lt- 11 < 1 by substituting E = 1 Sletn= 2m+ 1 6 :::>n is odd 7 => Ht =- 1 8:::>1(-1t-11 = 1-21 sincea=b=> la-11 = lb-11 9=2 10 => 2 < 1 by combining steps 4 and 9 11 =>contradiction 12QED Figure 1. Input to MU in FEL.

2. The Mathematics Task

The mathematics task consists of checking proofs and solving problems using the knowledge of mathematical results that has been already been acquired. Clearly there is more to understanding a mathematics text than this but this is the scope of MU's understanding.

A knowledge of the mathematical results is not sufficient either to check proofs or solve problems since there are many results that could be applied at any one step. It is also necessary to have some control knowledge with to choose the appropriate result. In theorem proving systems, such as Ammon [1992], this is often done by heuristics, but in MU the choice of result is largely driven by perceptual features.

MU performs proof checking just by use of its features to retrieve the appropriate result. As explained in the next section through the experience of checking proofs and solving problems the features change in their representation, so that gradually more specific features emerge which enable important results to be easily retrieved, thus overcoming the combinatorial choice. This also ensures that MU goes faster rather than slower with more knowledge, as the specialised features ensure that retrieval is faster .

In problem solving, MU uses four general purpose heuristics to give overall control: 1. Break a problem up into parts; 2. Suppose the left hand side; 3. Expand definitions; 4. Simplify expressions. A verbatim solution of MU using these heuristics to solve a problem in Group Theory is shown in Figure 2. The simplification process uses the CMS to control which results are applied. The above heuristics are not sufficient to solve all problems in mathematics, and research has shown that there is a need for specialised heuristics as well as the features used by MU. Morgan et al [1995] show how the heuristics can be learned from the analysis of worked examples.

3. Learning and the CMS

MU's learning is a ll performed by the Contextual Memory System (CMS) which controls all the storage and retrieval of the mathematical results in terms of dynamic features. Because of the open learning requirement, there are no built in features. Rather the CMS uses built in feature creation mechanisms to generate a large number of features from the input.

The CMS performs its learning in two stages:

1. Initial encoding of the mathematical results when MU reads the FEL statement in terms of features.
2. Continual updating of the features through the experience of proof checking and problem solving.

Feature creation works on a parsed form of the input. For example, the definition of abelian in Fig. 2 is parsed as (~ (abelian (cap g)) (and (group (cap g))

(forall (variables a b)

(propn (~(and (member a (cap g)) (member b (cap g))) (=(*a b) (* b a)))))))

If this is treated as a tree, features can be constructed as subtrees. Formally, features are defined by:

<feature> ::= <posi tion><specifier><type><term>

<position>::= LHS- I RHS- I null

<position> ::= LHS-<position> I RHS-<position>

<specifier> ::= IS- I HAS-

<type> ::= FORM- I TERM-

Since the <term> is as open as the input, this results in an infinite feature space. In this example there are many features including general features such as: has-form-[= _a_b], is-form-[~ _a_b ], has-form­ [member_a_b] and more specialised features such as: lhs-has-form-[ abel ian_[ cap _a]], rhs-has-form­ [and_[group _a]_b] is-form-[~_[ abelian_a]_[and_b_c]] and only about 10 features are used for the first encoding.

The initial encoding into features of a result may not be very efficient as at the time it is impossible to know which features will turn out to be salient. With subsequent experience, proof checking and problem solving will provide probes with which to do retrieval from the CMS. Often such retrievals will recall a result which cannot be applied to the current step, as well as the correct result, and these are termed failures. The CMS learns from this experience in three ways:

1. Features which were used in the searching using the probe but are not currently linked to the found item are termed 'uncomputed features'. These features are now linked to the item.
2. Features which index the found item but not the failures are termed 'useful features', and have their energies increased as well as the st:rength of the link.
3. It is also possible to create new features, unknown at the time to the CMS, which distinguish the found item from the failures.

Definition of abelian

G is abelian iff G isa group and Va,b E Gab= ba Problem 2.3.3 Prove ( G isa group and Va, b a E G and bE G ~ (ab)2 = a2b2) ~ G is abelian Suppose G isa group and Va, b a E G and bE G ~ (ab)2 = a2b2 RTP G is abelian RTP G isa group and Va, b a E G and b E Gab = l:>a by definition of abelian Part 1 RTP G isa group Follows logically QED Part 1 Part 2 Suppose a E G and b E G RTPab= ba Now (ab)2 = a2b2 ~ (ab)(ab) = (aa)(bb) since x2 = xx ~ a((ba)b) = a((ab)b) since (ab)(cd) = a((bc)d) ~ (ba)b = (ab)b since ab = ac ~ b = c ~ ba = ab since ba = ca ~ b = c QED Part 2

Figure 2. MU's Solution to a Problem.

4. Conclusion

MU shows that it is possible to model the learning of a very large and open domain. The solution is to use an arbitrary set of features built from the environment for initial encoding, and let experience dictate how the features should be revised to improve performance.