Synthesizing Geometry Constructions
Abstract
In this paper, we study the problem of automatically solving
ruler/compass based geometry construction problems. We first introduce
a logic and a programming language for describing such constructions
and then phrase the automation problem as a program synthesis
problem. We then describe a new program synthesis technique based on
three key insights: (i) reduction of symbolic reasoning to concrete
reasoning (based on a deep theoretical result that reduces
verification to random testing), (ii) extending the instruction set of
the programming language with higher level primitives (representing
basic constructions found in textbook chapters, inspired by how humans
use their experience and knowledge gained from chapters to perform
complicated constructions), and (iii) pruning the forward exhaustive
search using a goal-directed heuristic (simulating backward reasoning
performed by humans). Our tool can successfully synthesize
constructions for various geometry problems picked up from high-school
textbooks and examination papers in a reasonable amount of time. This
opens up an amazing set of possibilities in the context of making
classroom teaching interactive.