Interactive, Intelligent Tutoring for Auxiliary Constructions in Geometry Proofs
This addresses a specific problem for K-12 students in geometry education by providing an interactive tutoring system, though it is incremental as it builds on existing automated provers and tutoring systems.
The paper tackles the challenge of teaching students to find auxiliary constructions in geometry proofs by introducing the Advanced Geometry Proof Tutor (AGPT), which leverages an automated prover to interactively guide students, and a pilot study with 78 high school students shows AGPT is as effective as human tutors and more effective than state-of-the-art solvers.
Geometry theorem proving forms a major and challenging component in the K-12 mathematics curriculum. A particular difficult task is to add auxiliary constructions (i.e, additional lines or points) to aid proof discovery. Although there exist many intelligent tutoring systems proposed for geometry proofs, few teach students how to find auxiliary constructions. And the few exceptions are all limited by their underlying reasoning processes for supporting auxiliary constructions. This paper tackles these weaknesses of prior systems by introducing an interactive geometry tutor, the Advanced Geometry Proof Tutor (AGPT). It leverages a recent automated geometry prover to provide combined benefits that any geometry theorem prover or intelligent tutoring system alone cannot accomplish. In particular, AGPT not only can automatically process images of geometry problems directly, but also can interactively train and guide students toward discovering auxiliary constructions on their own. We have evaluated AGPT via a pilot study with 78 high school students. The study results show that, on training students how to find auxiliary constructions, there is no significant perceived difference between AGPT and human tutors, and AGPT is significantly more effective than the state-of-the-art geometry solver that produces human-readable proofs.