I nter- GPS : Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning (2021)

Abstract: Geometry problem solving has attracted much attention in the NLP community recently. The task is challenging as it requires abstract problem understanding and symbolic reasoning with axiomatic knowledge. However, current datasets are either small in scale or not publicly available. Thus, we construct a new large-scale benchmark, Geometry3K, consisting of 3,002 geometry problems with dense annotation in formal language. We further propose a novel geometry solving approach with formal language and symbolic reasoning, called Interpretable Geometry Problem Solver (Inter-GPS). Inter-GPS first parses the problem text and diagram into formal language automatically via rule-based text parsing and neural object detecting, respectively. Unlike implicit learning in existing methods, Inter-GPS incorporates theorem knowledge as conditional rules and performs symbolic reasoning step by step. Also, a theorem predictor is designed to infer the theorem application sequence fed to the symbolic solver for the more efficient and reasonable searching path. Extensive experiments on the Geometry3K and GEOS datasets demonstrate that Inter-GPS achieves significant improvements over existing methods. The project with code and data is available at https://lupantech.github.io/inter-gps .

## introduction geometry problem solving is a long-standing challenging task in artificial intelligence and has been gaining more attention in the nlp community recently @xcite @xcite . solving geometry problems is an essential subject in high-school education for the development of students' abstract thinking. as an example shown in figure 1 , given problem text in triangle abc, @xmath0. find cd. choices: a. 6.0 b. 6.5 c. 7.0 d. 8. in natural language and a corresponding diagram, one needs to identify the geometric relations, apply theorem knowledge, and conduct algebraic calculations to derive the numerical value of the answer. psychologists and educators believe that solving geometric problems requires high-level thinking abilities of symbolic abstraction and logical reasoning @xcite . however, if algorithms take the raw problem content, it might encounter challenges to understand the abstract semantics and perform human-like cognitive reasoning for inferring the answer in the geometry domain. a formal language is composed of words from a well-formed alphabet based on a specific set of rules and is commonly used in the fields of linguistics and mathematics. therefore, our proposed geometry solver parses the problem inputs into formal language descriptions (see examples in figure 1 ) before solving the problems. to translate the problem text and diagrams to formal descriptions, existing methods @xcite @xcite highly depend on human annotations like symbols in diagrams as the intermediate results. also, these methods fail to provide the explicit reasoning processes when predicting the answer. for example, @xcite simplifies the problem solving task to an optimization problem to pick one that satisfies all constraints from choice candidates. fur-thermore, most current datasets are either small in scale or not publicly available @xcite , which further hinders the research of geometry problem solving. to overcome these challenges, we first construct a new large-scale benchmark, called geometry3k, to assess algorithms' performance of geometry problem solving. the geometry3k dataset consists of 3,002 multi-choice problems as well as covers diverse geometric shapes and problem goals. in contrast with existing work, we also annotate each problem text and diagram with unified structural descriptions in formal language. this paper further presents a novel geometry solving approach with formal language and symbolic reasoning, called interpretable geometry problem solver (inter-gps). inter-gps (figure 4 ) develops an automatic parser that translates the problem text via template rules and parses diagrams by a neural object detector into formal language, respectively. in contrast to parameter learning, inter-gps formulates the geometry solving task as problem goal searching, and incorporates theorem knowledge as conditional rules to perform symbolic reasoning step by step. it demonstrates an interpretable way to tackle the task. also, we design a theorem predictor to infer the possible theorem application sequence in inter-gps for the efficient and reasonable searching path. extensive experiments on the geometry3k and geos datasets show inter-gps achieves large improvements over existing methods. our contributions are three-fold: (1) we introduce a large-scale diverse benchmark of geometry problem solving, geometry3k, which is densely annotated with formal language; (2) we develop an automatic problem parser to translate the problem text and diagram into formal language; (3) we propose a novel interpretable problem solver that applies symbolic reasoning to infer the answer. ## geometry formal language a geometry problem p is defined as a tuple (t, d, c), in which t is the input text, d is the diagram image and @xmath1, c 2 , c 3 , c 4 } is the multiplechoice candidate set in the format of numerical values. given the text t and diagram d, an algorithm is required to predict the correct answer c @xmath2. we formally describe the problem in the geometric domain language ω, a set of literals composed of predicates and arguments. basic terms used in the geometry problem solver are defined as follows. definition 1. a predicate is a geometric shape entity, geometric relation, or arithmetic function. definition 2. a literal is an application of one predicate to a set of arguments like variables or constants. a set of literals makes up the semantic description from the problem text and diagrams in the formal language space ω. definition 3. a primitive is a basic geometric element like a point, a line segment, a circle, or an arc segment extracted from the diagram. ## geometry problem parser our proposed inter-gps takes the problem text and diagrams as inputs and translates them into formal language descriptions automatically via the text parser (section 5.1) and the diagram parser (section 5.2), respectively. ## geometry problem solver unlike existing methods @xcite @xcite , inter-gps achieves the explicit symbolic reasoning with the theorem knowledge base and the humanreadable search process, shown in figure 4 . ## conclusion solving geometry problems is one of the most challenging tasks in math question answering. in this paper, we propose a large-scale benchmark, geom-etry3k, which consists of 3,002 high-school geometry problems with dense descriptions in formal language. we further propose a novel geometry solving approach, interpretable geometry problem solver (inter-gps), which parses the problem as formal language from an automatic parser and performs symbolic reasoning over the theorem knowledge base to infer the answer. also, a theorem predictor with a low-first search strategy is designed to generate the reasonable theorem application sequence. experiment results show that inter-gps outperforms existing state-of-the-art methods by a large margin. in the future, we plan to extend our work in other math question answering tasks and explore more general symbolic reasoning models.