Formal Representation and Solution of Plane Geometric Problems

Geometric problem solving has always been a long-standing challenge in the fields of mathematical reasoning and artificial intelligence. In this paper, we present formalgeo7k, a geometric problem dataset based on rigorous geometry formalization theory and consistent geometry formal system, serving as a benchmark for various tasks such as geometric diagram parsing and geometric problem solving. All problems are annotated with problem text, problem diagram, formal descriptions, and solution. Combining symbolic solver and deep learning techniques, we can achieve human-like, traceable and explainable solutions, which are stored in a hypergraph for graph-related tasks. We experiment with various methods and the best method achieves only 86.40% on formalgeo7k. This shows that formalgeo7k presents a challenge for future research.