Formal Representation and Solution of Plane Geometric Problems

Authors: xiaokai  zhang
na  zhu
cheng  qin
yang  li
tuo  leng
zhenbing  zeng
Venue: NeurIPS_cc_2024_Workshop_MATH-AI
Published: 2024-09-18 09:06:08

Abstract: 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.

Main paper: 
 introduction: 
 Geometric problem solving (GPS) has always been a long-standing challenge [22, 30, 13] in the fields of mathematical reasoning and artificial intelligence, owing to the cross-modal forms of knowledge and the absence of automated solving methods. A typical geometric problem consists of a textual problem description and a geometric diagram. GPS requires solvers to possess multimodal fusion and reasoning capabilities, which have attracted much attention recently. Existing works mostly construct a neuro-symbolic system for GPS. Deductive Database (DD) methods [14, 40, 24] parse the problem text and diagram into formal language and then solve the problem by logical reasoning. Program sequence generation (PSG) methods [5, 36, 29] encode the problem text and diagram, input the encoding into a decoder, and generate a program sequence, which is then executed by a program executor.However, existing methods focus on the research of the neural part while neglecting the symbolic part. First, existing methods fail to achieve a human-like problem-solving process. DD methods cannot eliminate redundant theorems, and PSG methods lack mathematical rigor. This not only undermines the readability of the solutions but also limits their application in mathematics education. Second, existing methods lack research on geometry formalization theory. This not only fails to ensure the consistency of the solver's reasoning process but also hinders the expansion of symbolic systems. Defining new theorems requires modifying the solver's code, making it difficult to represent more complex problems, such as problems at International Mathematical Olympiad (IMO) level. Furthermore, existing datasets are small in scale and cannot serve as benchmarks for training and evaluating large language model (LLMs). Some datasets are poorly annotated or contain errors, making them unsuitable as a unified benchmark. To address these issues, we develop FormalGeo, a consistent geometry formal system based on rigorous geometry formalization theory [37] . We further construct the formalgeo7k dataset, which contains 7,000 geometric problems. All problems are annotated with problem text, problem diagrams, formal descriptions, and solutions, as shown in Fig. 1 . This dataset can serve as a benchmark for various tasks, such as GPS, geometric diagram parsing (GDP), geometric relation extraction (GRE), geometric problem formalization and the evaluation of LLMs reasoning abilities.To assess the dataset difficulty, we experiment with several methods and the best method only achieves 86.40% problem solving success rate (PSSR). This shows that formalgeo7k presents a challenge for future research. 
formalgeo7k dataset: 
 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 code and datasets are open-source and available at https://github.com/FormalGeo/FormalGeo. Refer to Appx. D for instructions on how to use pip to build FormalGeo formal systems and download formalgeo7k.We build FormalGeo, a consistent geometry formal system based on rigorous geometry formalization theory [37] . FormalGeo incorporates diagrammatic reasoning, algebraic computation, relational reasoning, and logical operations into a unified framework of geometry predicate logic, whose syntax is similar to first-order predicate logic. Within this formal framework, we can transform geometric diagrams and text into a consistent formal language, which not only maintains good readability but can also be mechanically processed by computer. The final solution of geometric problems can be represented as hypergraph, where conditions serve as hypernodes and theorems as hyperedges, thus transforming into a human-like solution. In addition, FormalGeo uses geometry definition language (GDL) to define new predicates or theorems and uses condition declaration language (CDL) to describe geometry problems, making it extremely convenient to extend the formal system and represent complex problems. Details of GDL are provided in Appx. A. A formal representation and solution of a 2022 IMO geometry problem can be found in Appx. B.Our formalgeo7k Dataset contains 7,000 plane geometric problems, sourced from the Geometry3K [14] (40.69%), GeoQA [5] (53.38%), and GeoQA+ [3] (2.93%). Our annotation task can be divided into four parts: 1. Standardizing the style of problem texts (English and Chinese). For problems lacking English or Chinese descriptions, we add the missing descriptions. 2. Redrawing geometric diagrams using GeoGebra and saving the .gbb files, which contains detailed positional information of the geometric elements. 3. Annotating geometric diagrams and texts using FormalGeo formal language. 4. Adding the theorem sequences required to solve the geometric problems.Once the problems are annotated, we assign a different annotator to review and verify the correctness of the annotations. Finally, all problems are input into a symbolic solver FGPS [38] to check the correctness of the syntax, ensure that the annotated theorems can solve the problem and eliminate redundant theorems. By treating the intermediate results of a problem as a new goal, we can decompose a geometric problem into multiple sub-problem, automatically expanding the number of problems to tens of thousands. This results in a dataset with a smoother difficulty curve, and the number of problems becomes sufficient for training and evaluating LLMs.Sixteen trained graduate master's students participated in the dataset annotation tasks. The annotation and reviewing process took approximately 1,500 person-hours.Our dataset has 7,000 geometric problems. Each problem text (English) has a maximum of 444 characters and a minimum of 58 characters, with an average problem text length of 114.22. The construction CDL describes the topological structure of a geometric problem, and the number of its statements roughly reflects the complexity of the geometric diagram. The average length of construction CDL statements is 5.97. Both text CDL and image CDL describe the conditions of the geometric problem, with the average number of statements being 4.02 and 2.87, respectively. In the text CDL, the most frequently occurring predicates are Equal (61.04%), IsCentreOfCircle (9.67%), PerpendicularBetweenLine (8.69%), ParallelBetweenLine (4.92%), and IsTangentOfCircle (3.22%). In the diagram CDL, The proportions of Equal, PerpendicularBetweenLine, and ParallelBetweenLine are 80.95%, 12.16%, and 6.89%, respectively. The number of theorems required for GPS serves as an measure of the difficulty of the problem. Each problem involves a maximum of 28 theorems and a minimum of 1 theorems, with an average theorem number of 4.34. The detailed statistical information can be found in Appx. C. 
benchmark methods: 
 We tested several methods on formalgeo7k. It is important to note that most SOTA models for GPS are trained in specific symbolic environments (such as those provided by Geometry3K [14] or GeoQA [5] ), and adapting them to the FormalGeo would require significant manual effort. Therefore, we only compare methods using the FormalGeo environment. All methods use annotated text CDL and image CDL as input to the model. Parsing CDL from the original problem diagram and text is still a challenge, and we leave it for future work.Forward Search [38] . This is a purely symbolic approach. It starts from the initial conditions of the problem and continuously apply theorems to derive new conditions until the goal is achieved. We run the forward search method using four different strategies (breadth-first, depth-first, random and beam) and presented the results of the best strategy (random). The maximum search depth is set to 15, the beam size to 20, and the timeout for each problem is set to 600 seconds.Backward Search [38] . This is a purely symbolic approach. It begins with the problem-solving goal, expands it into multiple sub-goals, and repeats this process until all sub-goals are resolved. The best strategy for the backward search is breadth-first, with the other parameters set the same as in the forward search. We run the search method on two Intel i9-10900X processors, one AMD Ryzen 9 5900X, and one AMD Ryzen 9 7950X, using multiple processes while maintaining a CPU utilization rate of 80%. The total duration of the search is approximately 3 days. FGeo-TP [9] . This method utilizes the language model to predict the theorem sequences for GPS, reducing the search complexity. We chose BART-base [10] as the theorem predictor. The training epochs were set to 20, with an initial learning rate of 3 × 10 -5 . After theorem prediction, we ran the backward search method using a random strategy.FGeo-DRL [40] . This method leverages a pre-trained natural language model to establish a policy network for theorem selection and employ monte carlo tree search for heuristic exploration. We chose DistilBERT [21] as the policy network to learn how to select a theorem from a 234 action space for the current problem step. The implementation details and training methods are consistent with those in the original paper.HyperGNet [39] . This method builds a neural-symbolic system to effectively embed geometry knowledge and automatically perform human-like geometric problem solving. We train HyperGNet on a single GeForce RTX 4090. During the model's training phase, we optimize the model parameters using the Adam algorithm, with a learning rate of 10 -5 , batch size of 64 and training epochs of 50. Executing a single training session of the neural network only require approximately 30 minutes.To provide a more detailed comparison of different models' capabilities, we divided the dataset into 6 levels based on the length of the theorem sequence l required to solve the problem: It is evident that the longer the theorem sequence required to solve the problem, the higher the difficulty and the lower PSSR. We can see that, compared to traditional search methods, heuristic search combined with deep learning techniques has significantly improved the problem-solving success rate. FGeo-DRL achieved the highest overall PSSR, but its performance on solving difficult problems was lacking. HyperGNet, while slightly behind FGeo-DRL in overall PSSR, performed better on more challenging problems.EQUATION 
related work: 
 The study of GPS has a long history, which can be broadly divided into algebraic methods and synthetic methods. Algebraic methods transform geometric problems into a system of algebraic equations consisting of polynomials and inequalities, such as Wu's method [27] , Gröbner basis methods [2] and elimination methods [26] . Synthetic methods encompass a wider range of approaches, including search-based methods [8, 16] , knowledge-based methods [7] , geometric invariants-based methods [34, 6] , and machine Learning and optimization methods [23, 1, 20] . GPS has seen further advancements in recent years. Existing methods predominantly integrate deep learning and symbolic reasoning to construct a neuro-symbolic system for solving geometric problems. DD methods parse the problem text and diagram into formal language and then solve the problem by logical reasoning.Representative DD methods include Inter-GPS [14] , GeoDRL [18] , AlphaGeometry [24] , FGeo [40, 9] and E-GPS [28] . PSG methods encode the problem text and diagrams, input the encoding into a decoder, and generate a program sequence, which is then executed by a program executor.Representative PSG methods include NGS [5] , Geoformer [4] , DPE [3] , PGPSNet [36] , SAC-GPS [17] , UniMath [12] , LANS [11] , DualGeoSolver [29] and adaptive learning model [32] . Several geometry formal systems and datasets have been developed. We compared existing datasets with formalgeo7k, as shown in Tab. 2. In addition to geometric problem solving, tasks such as geometric diagram parsing [35] and geometric formalization [15] have also begun to attract increasing attention. ✓ ✓ GEOS-OS [20] GPS 2,235 DD ✓ ✓ Geometry3K [14] GPS 3,002 DD ✓ ✓ GeoQA [5] GPS 5,010 PSG ✓ ✓ GeometryQA [25] GPS 1,398 PSG ✓ ✓ GeoRE [31] GRE 1,398 - - - - - - - - GeoQA+ [3] GPS 7,528 PSG ✓ ✓ UniGeo [4] GPS 14,541 PSG ✓ ✓ ✓ PGDP5K [35] GDP 5,000 - - - - - - - - PGPS9K [36] GPS 9,022 PSG ✓ ✓ GeoEval [33] GPS 5050 - ✓ ✓ ✓ formalgeo7k All 7000 DD ✓ ✓ ✓ ✓ ✓ ✓ ✓* All denotes GPS+GDP+GRE. The 8 comparative metrics are: Formalization Methods, ForWard solving, BackWard solving, Numerical Targets, Proving Targets, Formal System, Human-like Solutions and Complexity Ratings. 
conclusion: 
 Based on rigorous geometry formalization theory and a consistent geometry formal system, we developed formalgeo7k, a dataset containing 7,000 annotated geometry problems, including problem text, problem diagrams, formal descriptions, and solutions. formalgeo7k serves as a benchmark for various tasks such as geometric diagram parsing and geometric problem solving, directly benefiting both AI4MATH and AI4EDU research. Experimental results indicate that formalgeo7k presents a challenge for future research.  
 
 Appendix: FormalGeo formal languages are categorized into geometry definition language (GDL) and condition declaration language (CDL). The former is used to define relations, attributes, theorems, and other elements of a geometry formal system, while the latter is employed for declaring conditions and goals in geometric problems. This chapter introduces GDL. An example of CDL can be found in Appx. B.GDL can be divided into predicate definition language and theorem definition language.Predicate definition language is used to define geometric relations and geometric attributions. For-malGeo comprises 89 predicates, including 25 fundamental predicates (Tab. 4) built into the solver and 12 entities (Tab. 5), 31 entity relationships (Tab. 6), and 21 attributions (Tab. 7) defined using the predicate definition language.The detailed statements for defining a predicate is as shown in the Tab. 3, including the predicate name and point variable declaration, validity check declaration, multiple representations, and automatic expansion. Additionally, when defining attributes, it also includes symbolic form declaration.Theorems are defined using the geometry predicate logic, comprising two parts: premises and conclusions, as shown in the Tab. 8. FormalGeo defines 200 theorems.Based on rigorous geometry formalization theory and a carefully developed symbolic solver, For-malGeo can represent, verify, and solve IMO-level geometry problems. Fig. 2 shows the original problem from the 2022 IMO Problem 4 and its formalized description.The final solution of geometric problems can be represented as a hypergraph, where conditions serve as hypernodes and theorems as hyperedges, as shown in Fig. 3 . For this hypergraph, we can easily apply rule-based methods to transform it into a human-like solution, as illustrated in Fig. 4 . We can also use LLMs to convert it into a more readable solution, which we leave for future research. You can use pip to download and use our formalgeo7k dataset.$ conda create -n <your_env_name> python=3.10 $ conda activate <your_env_name> $ pip install formalgeo >>> from formalgeo.data import download_dataset, DatasetLoader >>> from formalgeo.solver import Interactor >>> from formalgeo.parse import parse_theorem_seqs >>> download_dataset(dataset_name="formalgeo7k_v2", datasets_path="your_datasets_path") >>> dl = DatasetLoader(dataset_name="formalgeo7k_v2", datasets_path="your_datasets_path") >>> solver = Interactor(dl.predicate_GDL, dl.theorem_GDL) >>> problem_CDL = dl.get_problem(pid=1) >>> solver.load_problem(problem_CDL) >>> for t_name, t_branch, t_para in parse_theorem_seqs(problem_CDL["theorem_seqs"]): solver.apply_theorem(t_name, t_branch, t_para) >>> solver.problem.check_goal() >>> from formalgeo.tools import show_solution >>> show_solution(solver.problem) 



Reviews: review: title: title: The paper introduces a new unified dataset for geometric problems field
main_review: main_review: The paper presents a valuable contribution to the field of geometric problem-solving by providing a large, well-annotated dataset and demonstrating its potential as a challenging benchmark.

Pros:
+ The paper acknowledges and addresses the gap of missing symbolism in existing datasets and builds a unified benchmark.
+ The authors also use FGPS to verify the correctness of the syntax
+ The paper details how the dataset is constructed.

Cons:
- The paper doesn’t discuss the potential reason why existing works don’t perform well on the new dataset.
- It would be great if tasks such as GPS, GDP, and GRE can be evaluated individually against formalgeo7k to demonstrate the effectiveness of the new dataset.
title: title: Review of formalgeo-7k
main_review: main_review: The paper introduces FormalGeo, a consistent geometry formal system grounded in rigorous geometry formalization theory. Building upon this framework, the authors present formalgeo7k, a dataset comprising 7,000 plane geometric problems annotated with problem texts, diagrams, formal descriptions, and solutions. The dataset aims to serve as a benchmark for tasks such as geometric diagram parsing and geometric problem solving (GPS).

It is an interesting work and formalgeo-7k can be a significant contribution to evaluating VLMs and other models in solving geometry problems as it has a decent amount of data points and provides human-like solutions.

My concerns about this work are the clarity of metrics used and the motivation of the work. For instance, While the paper mentions that annotations were reviewed for correctness, it does not specify the criteria or the inter-annotator agreement metrics. Information about the quality control measures would add credibility to the dataset. Furthermore, there is no mention of whether the dataset, the FormalGeo system, or the symbolic solver FGPS are publicly available. Accessibility is crucial for a benchmark dataset to facilitate widespread research and validation. Also, while the authors mentioned that this dataset can be used to evaluate LLMs, they have not tested these models. Finally, the authors can better motivate their work by providing useful insights driven by testing different models on their dataset.

While this paper is a good contribution to the workshop, in future venues and conferences, I would like to see how humans perform against formalgeo-7k, how comprehensible the solutions are for humans, how clear and accurate its annotations are, and how different metrics available in this dataset (as mentioned in Table 2.) can be used to gain detailed insights into the relative strength of used models.
title: title: This paper  introduces formalgeo7k, a dataset designed to address challenges in geometric problem-solving through rigorous formalization and a consistent geometry formal system. It serves as a benchmark for tasks like geometric diagram parsing and problem-solving.
main_review: main_review: Pros:
1. A large dataset of geometry problems is provided in this paper, which may benefit for this field.

2. It demonstrates detailed comparisons between several deductive methods on this dataset, which may offer valuable insights for other researchers.

Cons:
1. This dataset is only composed of several existing easy datasets, and more difficult and diverse geometry datasets are required in this field.

2. Novel proving methods should be presented not just evaluating existing deductive engines.

3. Limited technical contributions.
title: title: Large dataset for geometric problem with a new representation method
main_review: main_review: The main contribution of this paper is the new geometric problem dataset, formalgeo7k. The dataset contains enough examples for LLM training. It also includes advanced geometry problems. Along with the new dataset, the authors also suggested a new representation method. I agree that the new representation method is more readable. The paper claimed that the new representation method creates consistent solver reasoning process. I can see how this might be the case however it would be better to have a comparison metrics on this. In the experiment section, I appreciate that the authors provided the success rate vs. theorem sequence length. It would be nice to see the performance sliced by other factors. For table 2, it would be better if the actual performance on each tasks for each dataset is provided instead of a check mark.

Overall I think the paper still contribute a lot to the field for the nicely annotated dataset. The experiment section could be more detailed and extended to better prove the benefits of the new representation method. However, it does provide enough info for potential users of the datasets.