Reinforcement Learning for Geometry Problems

Planimetry problems from the school curriculum are often formulated in terms of metric relations between objects defined in the problem statement. Meanwhile, geometry problems from mathematical competitions usually require students to expand given configuration in nontrivial ways to be able to generate a correct solution. The emerging constructions can be naturally represented in the form of graphs where vertices and edges are assigned labels from some finite alphabet. Existing systems of automatic theorem proving are based on algebraic methods and fundamentally different from how students approach geometry problems. In our work, we define an infinite geometry knowledge graph and develop a software framework to represent some optimization problems as rl-environments. We also propose an agent architecture that is able to deal with graph-structured observations.