Automated Geometry Theorem Proving for Human-Readable Proofs

1 Introduction

Geometry is a key, mandatory subject in the secondary school curriculum. An important part of geometry learning is proof writing [Schoenfeld, 1994; Hanna, 1995] which helps train students' logic and deductive reasoning skills. Because of this, it is also one of the most challenging subjects for students. The standard format of a geometry proof problem consists of a given geometry figure, a set of provided constraints and a goal to prove. Students are asked to write a step-by-step deduction

1 The term "K-12" is commonly used in the United States and Canada to collectively refer to primary and secondary education.

Given: Square ABCD, AP = PD, ∠PAD = 15◦

Goal: △PBC is equilateral

using Euclidean axioms. Figure 1 depicts an example problem. The task becomes more difficult when a proof requires auxiliary constructions - adding lines/arcs to the problem figure to help discover a proof - because finding appropriate constructions can be very challenging as one could add any geometric elements anywhere in the problem figure. 2

Due to the aforementioned reasons, we envision that a powerful automated geometry proof system can benefit students, because it provides a foundation to help them practice their problem-solving skills. It can also facilitate the current nascent paradigm shift in education toward massively online and personalized learning, targeting the K-12 students.

Background and Related Work Although computer-based geometry learning tools have been successfully applied in education, many of these systems focus on simple tasks, such as drawing and calculation, and do not deal with geometry proofs (e.g. Cabri II Plus, Sketchpad, and Geometry Expression). The few exceptions [Gao and Zhu, 1999; Janiˇci´c, 2006; Narboux, 2007] are all limited by their underlying geometry theorem proving algorithms. For example, GeoProof [Narboux, 2007] and GEX [Gao and Zhu, 1999] adopt algebraic methods [Wu, 1986; Kutzler and Stifter, 1986; Buchberger et al., 1988] for geometry theorem proving. Although these methods are powerful, they rely on algebraic theories and can only decide the validity of geometry statements [Jiang and Zhang, 2012]. GCLC [Janiˇci´c, 2006] is built on top of the area method [Chou et al., 1993], which utilizes a specialized set of nonstandard axioms unfamiliar to students learning standard Euclidean geometry. For the above reasons, none of the systems is suitable for general K-12 students.

2 The interested reader may attempt the problem in Figure 1. Trigonometry is not needed.

The goal of our work is to help students learn geometry proof reasoning, thus our primary design objective is proof readability. By readable proofs, we mean proofs that are formulated using Euclidean geometry axioms taught in schools. The most challenging technical obstacle that we face is auxiliary construction, which is necessary for many problems. Matsuda et al. [Matsuda and Vanlehn, 2004] propose the first technique for auxiliary construction. Their idea is to only add elements to satisfy premises of a postulate whose consequence "matches" a goal. Although Matsuda et al. have made an impressive first step toward generating human-readable proofs using standard Euclidean axioms, their approach is ineffective and can cause combinatorial explosion when multiple construction steps are needed.

Template-based Geometry Theorem Proving To address the weaknesses of prior systems, we introduce a general template matching-based approach to tackle the auxiliary construction challenge for geometry theorem proving. Our key observation is that problem solving typically involves the use and trained familiarity with a number of important problem solving strategies. At the high-level, we (1) distill a set of strategies in the form of template figures from studying around 20 problems frequently used for competition training, and (2) develop a template matching scheme to recover templates from a given figure.

We have realized our approach as a new automated geometry theorem prover, iGeoTutor and extensively evaluated it. Our problem corpus has 77 problems in total, including ones cited in prior work and from Math competitions. Evaluation results show that iGeoTutor is very effective - it solves all but two problems in under two minutes each. Moreover, its construction process is significantly more efficient than GRAMY's on the same problem set (cf. Table 2, Section 3.2 for the detailed comparison). We have also performed a test pilot with 12 high school students, and found iGeoTutor is effective in helping student to learn geometry proof. Based on all the evaluation results, we expect iGeoTutor will impact K-12 geometry education by helping students become strong problem solvers and self learners.

Contributions Our main contributions are:

• We propose a novel, template matching-based approach that is powerful and produces human-readable proofs.
• We realize our approach in iGeoTutor, which can effectively solve nearly all problems in our collection using six simple templates.
• We present details of our extensive evaluation of iGeoTutor's performance in solving geometry proof problems and its effectiveness in helping students learn.

The remainder of this paper is organized as follows. Section 2 describes our methodology and approach in designing iGeoTutor, and Section 3 details our evaluation results. We conclude in Section 4 with a discussion of future work .

2 Methodology and Approach

This section presents the design of iGeoTutor. 3 Central to our system is a novel approach for auxiliary construction, that forms the foundation for our work. In particular, we introduce the concept of templates and template-matching scheme.

2.1 SystemArchitecture

Figure 2 shows the overall system architecture of iGeoTutor. We discuss the other key components in this section, and defer the discussion of the core component - the "Auxiliary Construction Engine" - to later sections. We next give a stepby-step description of iGeoTutor's workflow:

1. Parsing: iGeoTutor parses a given geometry figure from its pictorial representation to an internal representation using first-order predicates and store them in the Knowledge Base. This paper omits the details of this step as it is not the focus of this work.
2. Retrieving: The Reasoning Engine retrieves the facts from the Knowledge Base and derives new facts using Geometry Axioms and Arithmetic Reasoning rules.
3. Storing: iGeoTutor stores any derived facts to the Knowledge Base.
4. Checking: iGeoTutor checks whether the goal is in the Knowledge Base.
5. Result: Two cases:
6. (a) Producing: If the goal is in the Knowledge Base, iGeoTutor terminates and produces a proof.
7. (b) Consulting: Otherwise, it consults Auxiliary Construction Engine for additional facts according to the existing geometric configuration in the problem figure.
8. Constructing: iGeoTutor stores the facts about an auxiliary construction in the Knowledge Base and diverts its execution to step (2) and repeat.

3 In our current prototype, we focus on problems involving line segments and angles, and do not consider those involving circles, arcs, and solid geometry, which we leave for future work.

Knowledge Base Given a geometry diagram and a set of associated constraints, iGeoTutor uses first-order predicates for its internal representation. The predicates can be classified into three categories 4 :

• Geometrical elements, such as line(A,B) and angle(A,B,C);
• Position relation, such as parallel(line(A,B),line(C,D));
• Quantity relation, such as lineEqual(line(A,B),line(C,D)).

For example, the problem in Figure 1 is represented internally as follows:

• Given: square(A,B,C,D), line(A,P), line(B,P), line(C,P), line(D,P), lineEqual(line(A,P),line(D,P)) and angleEqual(angle(P ,A,D),15◦ ).
• Prove: equilateralTriangle(B,P,C).

Apart from the problem representation, the Knowledge Base also stores derived facts.

Geometry Axioms Geometry Axioms refer to definitions, postulates, and previously proved theorems within the scope of Euclidean geometry. Each axiom consists of premises and a consequence, which are represented internally using the predicates introduced earlier. For example, the "Side-Angle-Side" postulate can be expressed as the following Horn clause:

triangleCongruent(triangle(A,B,C),triangle(D,E,F )) ← triangle(A,B,C) ∧ triangle(D,E,F ) ∧ lineEqual(line(A,B),line(D,E)) ∧ lineEqual(line(B,C),line(E,F )) ∧

angleEqual(angle(A,B,C),angle(D,E,F )).

Arithmetic Reasoning This component refers to the arithmetic reasoning capability incorporated into iGeoTutor. In particular, we employ an off-the-shelf state-of-the-art SMT solver Z3 [De Moura and Bjørner, 2011; Microsoft Research, ] to resolve the arithmetic constraints when needed. We interface iGeoTutor and Z3 in three phases: (1) iGeoTutor converts all its quantitative predicates in the knowledge base to Z3 commands in Z3's script language; (2) the Z3 checker executes the Z3 script to infer additional quantitative constraints; and (3) we convert Z3 inferred constraints back to iGeoTutor's internal predicates to store in the Knowledge Base.

Reasoning Engine The Reasoning Engine applies the Geometry Axioms and the Arithmetic Reasoning rules on facts stored in the Knowledge Base to deduce additional facts. iGeoTutor employs forward chaining [Chou et al., 2000] to update the given constraints. For example, on the internal representation of the problem in Figure 1, the Reasoning Engine applies the aforementioned Horn clause of the "Side-Angle-Side" postulate to derive, among others, the following:

• triangleCongruent(triangle(A,B,P),triangle(D,C,P))
• lineEqual(line(B,P),line(C,P))

Clearly, the goal of the problem cannot be reached given the original problem figure; auxiliary constructions are needed. We explain next how we tackle this difficulty.

4 The interested reader may refer to http://www.cs.ucdavis.edu/ ∼su/igeotutor.html for the complete list of predicates and axioms.

2.2 Auxiliary Construction

This section describes our template-based technique for auxiliary construction. We introduce the six templates that we use, illustrate via examples how templates guide auxiliary construction, and present our detailed construction procedure.

2.2.1 Templates

As mentioned earlier, templates intuitively capture problem solving strategies. Templates can be adapted to solve particular classes of geometry problems. We represent each template by a common geometry shape that is used to illustrate one standard Euclidean axiom. Take the "IT2" template in Figure 3 for example, this template captures the strategy of exploiting the equivalence of a pair of angles or segments. A key challenge is how to discover these templates, which we discuss next.

We distill a small set of template figures from our close examination of around 20 training problems. We discover that over all these problem instances, any auxiliary construction that leads to an eventual proof is used mostly to realize some specific geometry shape. Perhaps quite surprisingly, only six shapes are used frequently. Figure 3 depicts these six template figures, which are quite basic. They all concern line or angle congruence, which in retrospect may not be surprising as the concept of congruence underlies most geometry proof problems. This study confirms our hypothesis that a few common, effective strategies exist for geometry proof problems. Next, we show how to use these templates to steer proof search.

2.2.2 Template-Matching Example

We use the example problem in Figure 1 to illustrate how to use the template figures to discover auxiliary constructions.

As mentioned in Section 2.1, the given problem figure suf-

• Template: Congruent Triangles
• Matching Instance: AB, △APD, AB = AD

• Auxiliary Construction: Find a point Q such that △AQB is congruent to △APD
• Realization: Introduce a point Q, with ∠BAQ = ∠PAD and AQ = AP , and connect BQ

fices to help derive BP = PC, but to prove BP = BC or PC = BC, we must add auxiliary constructions. First, assume that we decide to apply the "CT" template on the existing △APD and AB. To complete the "CT" template, we construct a new point Q to make △AQB congruent to △APD as shown in Figure 4. Second, assume that we decide to use the "IT2" template to complete an isosceles △AQP by connecting P and Q as depicted in Figure 5. With these constructions, we can discover a proof via forward-chaining.

Table 1 shows a short version of the proof iGeoTutor discovers by applying the "CT" template and the "IT2" template. There is an obvious alternative algebraic solution by utilizing tan 15◦ and the Pythagorean Theorem to calculate the length of BP. However, the sample proof discovered by iGeoTutor uses only standard Euclidean axioms (not any trigonometry), which is more elegant and suitable for students learning elementary geometry. Note that the problem has a number of alternative solutions; here we illustrate one of them.

Next, we focus on two important questions: (1) How to decide which template to apply? and (2) How to select the existing geometric elements to apply for the template? To this end, we introduce our template matching scheme next.

2.2.3 Template-Matching Scheme

We discuss our high-level template matching process first and then introduce key optimizations to make it practical.

5 "Corresponding Parts of Congruent Triangle are Congruent"

• Template: Isosceles Triangle (2)
• Matching Instance: AP , AQ, AQ = AP
• Construction: Complete the triangle △APQ
• Realization: Connect P and Q

High-Level Template Matching Process Let each template t be a pair 〈G, C〉, where G is the template figure and C the set of constraints satisfied by G. Let ℘(C) denote the power set of C. For each subset S ∈ ℘(C), construct the tuple Ts = 〈Gs, C \ S〉, where Gs is a sub-figure of G induced by S and \ is set difference.

At the high-level, a template matching step traverses S ∈ ℘(C) and unifies the constraints in each subset S against the constraints Cp from the current problem configuration, i.e. the constraints Cp and figure Gp. If a unification check succeeds, we overlay Gs on Gp to add any missing elements Gm from G and constraints C \ S; the pair 〈Gm, C \ S〉 constitute an auxiliary construction.

Key Optimizations We introduce two important heuristics to optimize the high-level search procedure. One prioritizes the search of the subsets, while the other opportunistically leverages the goal and any of its derived constraints for matching.

Optimization 1: Search Prioritization A template may induce a large number of subsets to unify against, thus it is important to order them such that the more "profitable" subsets are checked earlier. To this end, we develop two techniques.

First, for each template 〈G,C〉, we call a set S ∈ ℘(C) a minimum sufficient set iff

i.e., S is a minimal, logically equivalent subset of C. The intuition is that a minimum sufficient set induces a complete figure w.r.t. the template and should be matched first. For example, the constraints for the problem figure in Figure 5 unify with the minimum sufficient set (w.r.t. the "IT2" template) {AQ = AP}, specifying that two equivalent lines share a common end-point. In contrast, the matching example in Figure 4 is achieved via a non-minimum sufficient set. For matching purposes, minimum sufficient sets are given higher priorities than the other subsets.

Second, we introduce a ranking heuristic to target the nonminimum sufficient sets. The basic intuition behind the heuristic is to maximize "gain" of a subset - few added elements lead to many derived constraints. Thus, we define "gain" as the ratio of the number of derived constraints (from constraints induced by the added elements and the given constraints in the problem figure) and the number of added elements to realize a template figure. Our heuristic is to rank the non-minimum sufficient sets w.r.t. their "gain". Later, we show empirically that the heuristic is effective and performs better than the pure random ranking scheme.

Optimization 2: Goal-Directed Matching To complement the first optimization, we introduce another novel technique to further improve the accuracy and effectiveness of the template matching procedure. In particular, before template matching, the reasoning engine incorporates the problem goal into its knowledge base and performs exhaustive forward chaining until it derives no new facts (i.e. reaching the constraint closure). For template matching, all constraints in the closure are considered. Our insight is to exploit every fact associated with the given geometric figure. Note that this does not invalidate the soundness of our system because the goal and any goal-related facts are removed from the knowledge base in the actual reasoning phase - the sole purpose of this optimization is to aid template matching for discovering auxiliary constructions.

Putting Everything Together As shown in Algorithm 1, our construction search procedure is cast as depth-first search. It begins by attempting to find all matching templates through the function TemplateSearchProcedure w.r.t. the current problem configuration (line 4). While traversing each matched template, it synthesizes the respective auxiliary constructions and incorporates them to the original problem figure represented by knowledge (lines 5-7). Next, the reasoning engine exhaustively derives new facts (line 8). If it finds the goal, the construction procedure exits with the discovered proof (line 9). Otherwise, it invokes a recursive call to continue the search

(line 10). This procedure repeats until a proof is found.

Note that in the function TemplateSearchProcedure shown in Algorithm 2, FindingTruePropositions helps infer all facts after the goal has been incorporated (line 3). Subsequently BackwardMatching uses the goal and any goal-derived facts (along with the existing facts) to find and match templates (line 4). Finally it ranks and returns all matching templates (lines 6-7).

3 Evaluation

First, we present our empirical evaluation of iGeoTutor's effectiveness. It also includes a comparison with GRAMY, the previously state-of-the-art system. Second, we describe a field study for assessing iGeoTutor's effectiveness in helping students learn geometry proofs.

3.1 Test Corpus

Our test corpus contains 77 problems in total (please refer to http://www.cs.ucdavis.edu/∼su/igeotutor.html for the full list of problems and their descriptions). The problems have been gathered from various sources, including 22 from the work on GRAMY [Matsuda and Vanlehn, 2004] 6 for comparison. The rest of the problems are from an archive of classical geometry proof problems online [Liu, 2011] and two Chinese textbooks [Shen, 2006; Zhou, 2004], both of which are popular practice materials for the Chinese Mathematics Olympiad. A number of the problems involve arithmetic calculations. As mentioned earlier, iGeoTutor supports arithmetic, but not trigonometry, and restricts its search for auxiliary constructions to rely only on the supplied constraints when given a measurement problem, i.e. a problem that asks for the size of an angle or the length of a segment.

3.2 Evaluation Setup and Results

iGeoTutor runs on a workstation with a third generation Intel Core i7-3770 processor and 16GB RAM. We present two sets of results: (1) general results on all 77 problems, and (2) detailed results on the 22 problems from GRAMY.

3.2.1 iGeoTutor Performance

First, out of the 77 problems, iGeoTutor solves 75 in under two minutes each (we defer to Section 3.4 to discuss the two problems that iGeoTutor fails to solve). All constructions are accomplished using the six templates from Section 2. For each of the successfully solved problems, iGeoTutor matches three or fewer templates before discovering a proof. Moreover, 17 problems are solved only by incorporating their goals, demonstrating the importance of our goal-directed search heuristic.

Second, Table 2 presents detailed results for both iGeoTutor and GRAMY on the 22 problems from GRAMY. We discuss the results for iGeoTutor first. In the table,

• Depth refers to the depth of iGeoTutor's construction search procedure (Algorithm 1). In parentheses, we also specify each construction's matching type: (1) m for matching via a minimum sufficient set, and (2) n for matching via a non-minimum sufficient set. For example,

6 The original list contains 32 problems, but nine are from textbooks that we do not have access to, and one requires trigonometry.

• "3(n,n,m)" for P022 indicates that it requires 3 constructions, with the first two being "n" and the last "m".
• Length refers to the number of axiom applications until the first successful templating matching attempt (i.e. all premises of a template matching are satisfied).
• States refers to the total number of states expanded before reaching a proof. In general, for geometry theorem proving, a state consists of a problem figure, all true propositions associated with the figure's geometrical elements, and goals to prove. For iGeoTutor, the traversered states correspond to the different instantiations of template matching for auxiliary construction.
• Time refers to the total time in seconds that iGeoTutor takes to produce a proof.
• Gain refers to the performance gain of our search prioritization heuristic over when it is disabled (i.e. using purely random search).

From the table, it is clear that iGeoTutor performs well and the search prioritization heuristic is effective.

3.2.2 iGeoTutor vs. GRAMY

Since GRAMY shares the same high-level goal as iGeoTutor and is the previously state-of-the-art system, we evaluate how the two systems compare. Table 2 also includes GRAMY's performance results on the identical problem set. The performance numbers for GRAMY are extracted from its publication [Matsuda and Vanlehn, 2004], where '-' indicates unavailable data.

Because the GRAMY system is unavailable and it was evaluated on older hardware, we do not include any of its timing data, but rather focus on the other data that reflect the complexity of its proof search for a fair comparison. Thus, we focus on the common, similar metrics as in iGeoTutor: "Depth",

"Length", and "States". In particular, (1) Depth refers to the total number of invocations of GRAMY's construction procedure before it finds a proof as its proof procedure is formalized as a breadth-first search [Matsuda and Vanlehn, 2004], (2) Length refers to the number of axiom applications needed to realize the first successful construction, and (3) States refers to the total number of expanded states before finding a proof. Because GRAMY also employs backward chaining, so state changes are not only due to attempted constructions but also changes in the problem goal (by adding sub-goals).

iGeoTutor successfully solved all four problems that GRAMY failed to solve (marked by '7') - two (P002 and P003) took little time and had relatively simple proof search, while the other two (P004 and P022) took relatively longer and had more complex proof search. Table 2 also shows that iGeoTutor's proof search is significantly more effective. For example, in terms of the number of expanded states, the most direct measure on search complexity, iGeoTutor exhibits orders of magnitude improvement over GRAMY.

3.3 Pilot Study

Participants For the study, we have recruited 12 students from the local high school. All students are in ninth grade, the typical grade level for the Geometry standards in California.

Procedure First, the participants took a pre-test. Then, they used iGeoTutor to explore those problems they failed to solve on the pre-test. Finally they took a post-test. Both the pre-test and post-test contain three geometry proof problems (please refer to http://www.cs.ucdavis.edu/∼su/igeotutor.html for the two tests). Each participant was given 30 minutes to complete each of the three parts of the study.

Results Figure 6 summarizes the results of our study. Specificially, it shows each student's performance improvement on the post-test over the pre-test: dark bars illustrate improvement measured in terms of successfully solved problems, while gray bars illustrate improvement measured in terms of correctly identified constructions. We have run a paired t test to compare each participant's performance (in terms of number of solved problems) across the two test sets. The results show that students' post-test performance is significantly better than that of the pre-test [t(10) = 2.3834, p = 0.0384], thus indicating that iGeoTutor clearly helps students learn.

3.4 iGeoTutor's (In)Completeness

As aforementioned, iGeoTutor failed to solve two (P073 and P076) of the 77 problems (please refer to http://www.cs.ucdavis. edu/∼su/igeotutor.html for details on these two problems). This section discusses the reasons for iGeoTutor's proof search to be incomplete and possible solutions. We identify two sources of incompleteness:

Missing Axioms For P076, iGeoTutor found two constructions that could successfully lead to the solution (∠BAC = 40◦ ). iGeoTutor failed even with the right auxiliary constructions because it was unable to exploit a property of four points on a circle to derive ∠ACE = ∠ADE. As mentioned earlier, iGeoTutor is only given the axioms for dealing with non-circle problems and therefore it fails to solve the problem that requires circle-related axioms. A simple solution is to equip iGeoTutor with all elementary geometry axioms.

Missing Templates The six templates that we distilled from around 20 problems are sufficient to help solve nearly all problems in our corpus. We do not, however, claim that iGeoTutor's construction search procedure is complete. P073 is the only problem from the corpus that iGeoTutor fails to solve due to incomplete templates - one step of the construction is not covered by the six templates. However, the figure was very similar to "OT" and could be considered its variant, which may be obtained by relaxing the midpoint constraint for "OT". For cases like this, one possible direction is to support a set of shape variants for each template while fixing some original constraints. This would allow more flexible and effective problem solving strategies.

4 Conclusion

This paper has presented a novel, practical template-based construction search algorithm for automated geometry theorem proving. Our evaluation demonstrates its power in geometry problem solving and its effectiveness in helping students to learn geometry proof. For future work, we plan to explore three main directions. First, we plan to utilize statistical predictions trained on our problem corpus to suggest good candidates for template matching. Second, we would like to extend our work to support problems that involve circles and arcs, and in solid geometry. Third, we plan to further evaluate and refine our system in real learning environments, and improve students' learning experience.