Source-linked AI summary
Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning
Pan Lu, Ran Gong, Shibiao Jiang, Liang Qiu, Siyuan Huang, Xiaodan Liang, Song-Chun Zhu
TL;DR
Geometry problem solving lacks large, public datasets and requires abstract understanding with symbolic reasoning. The paper introduces Geometry3K and Inter-GPS, which automatically formalize inputs and search with theorem-based symbolic reasoning; experiments show large improvements over existing methods. Inter-GPS remains limited by parsing errors, an incomplete theorem set, and difficulty with complex combined-shape or shaded-area problems.
Problem
Geometry problem solving requires abstract understanding and symbolic reasoning, but existing methods rely on human annotations or lack explicit reasoning, while datasets are often small or unavailable.
Method
The paper constructs Geometry3K and develops Inter-GPS, which automatically parses text and diagrams into formal language and performs step-by-step theorem-based symbolic reasoning with predicted theorem sequences.
Results
Inter-GPS outperforms existing state-of-the-art methods by a large margin on the Geometry3K and GEOS datasets.
Takeaways & Limitations
Geometry3K supplies dense formal annotations, while Inter-GPS provides an interpretable symbolic approach to geometry problem solving.
Takeaways & Limitations
Inter-GPS can fail with inaccurate parsing, incomplete theorem coverage, nested or uncertain text references, and complex combined shapes or shaded areas.
Abstract
from arXiv · showhide
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.
1 Introduction
Geometry problem solving requires abstract understanding, theorem application, and symbolic reasoning, while existing datasets and methods have important limitations. The paper addresses these gaps with Geometry3K and Inter-GPS, an automatic, interpretable solver using formal language and symbolic reasoning.
- Geometry problem solving requires identifying geometric relations, applying theorem knowledge, and performing algebraic calculations from text and diagrams.
- Existing methods depend heavily on human annotations and often do not expose explicit reasoning processes when predicting answers.
- Many current geometry datasets are small or unavailable publicly, hindering research progress.
- Geometry3K contains 3,002 diverse multiple-choice problems with unified formal-language annotations for both text and diagrams.
- Inter-GPS automatically parses text and diagrams into formal language, applies theorem-based symbolic reasoning step by step, and predicts theorem sequences for efficient search.
- The paper contributes a benchmark, an automatic problem parser, and an interpretable solver that applies symbolic reasoning to infer answers.
2 Related Work
Prior geometry problem-solving resources are limited in scale, problem diversity, or availability, while earlier approaches emphasize theorem proving, formalization, parsing, or implicit solving. Interpretable symbolic reasoning provides a contrasting direction for mathematical problem solving.
- Existing geometry datasets are often small or limited in problem types, and GEOS++ and GEOS-OS were not publicly available.
- Geometry3K provides 3,002 SAT-style problems spanning diverse graph and goal types with dense formal-language descriptions.
- Earlier automated geometry research focused on theorem proving, problem synthesis, diagram parsing, and problem formalization.
- Interpretable math-solving work either generates intermediate structures or translates problems into symbolic language for iterative logical reasoning.
3 Geometry Formal Language
The paper represents geometry problems in a formal domain language whose literals encode semantic descriptions from text and diagrams. This language defines geometric entities, relations, arithmetic functions, and primitives for symbolic solving.
- A geometry problem is represented by input text, a diagram image, and four numerical multiple-choice candidates, with the algorithm predicting the correct candidate.
- The formal language domain Ω consists of literals formed from predicates and arguments.
- A predicate denotes a geometric shape entity, geometric relation, or arithmetic function.
- A literal applies one predicate to variables or constants, and sets of literals describe problem semantics from text and diagrams.
- A primitive is a basic geometric element such as a point, line segment, or circle.
- The formal language defines 91 predicates, with example predicate and literal templates listed in Table 1.
4 Geometry3K Dataset
Geometry3K is a new large-scale geometry benchmark designed to address limitations in existing datasets through diverse problems and dense formal-language annotations.
- Dataset Collection: Geometry3K contains 3,002 SAT-style problems collected from two high-school textbooks, covering diverse graph and goal types.
- Dataset Collection: Unlike existing datasets, Geometry3K annotates each problem with dense formal-language descriptions connecting textual and visual content.
- Dataset Statistics: The dataset is split into training, validation, and test sets with ratios of 0.7:0.1:0.2.
- Dataset Statistics: Geometry3K includes 6,293 text literals and 27,213 diagram literals, with text predicates more evenly distributed than diagram predicates.
- Comparisons with Existing Datasets: Less than 1% of Geometry3K problems are solvable without diagrams, compared with 80.5% for GEOS, indicating stronger dependence on visual information.
5 Geometry Problem Parser
Inter-GPS automatically converts problem text and diagrams into formal-language descriptions using rule-based text parsing and neural diagram analysis.
- Parser Overview: Inter-GPS translates problem text and diagrams into formal-language descriptions automatically through separate text and diagram parsers.
- Text Parser: The text parser maps the problem word sequence into literals composed of predicates and variables.
- Text Parser: Inter-GPS uses regular expressions for rule-based text parsing and compares this approach with a BART semantic parser.
- Diagram Parser: The automatic diagram parser detects varied diagram symbols without human intervention, including parallel, perpendicular, and isosceles relations.
- Diagram Parser: The diagram pipeline extracts geometric primitives with Hough Transformation, detects symbols and text regions with RetinaNet, and recognizes text using MathPix.
- Diagram Parser: Symbol grounding uses Euclidean distance together with geometric constraints, such as matching parallel symbols to lines with equal slopes.
6 Geometry Problem Solver
Inter-GPS solves geometry problems through interpretable symbolic search: it builds a formal relation set, applies theorem rules, and uses theorem prediction and heuristic ordering to guide inference.
- Symbolic Geometry Solver: Inter-GPS performs explicit symbolic reasoning with a theorem knowledge base and a human-readable search process.
- Symbolic Geometry Solver: The solver takes a relation set R and theorem knowledge base KB as inputs and outputs the numeric solution g* for the problem goal g.
- Symbolic Geometry Solver: The relation set is initialized from parsed text and diagram literals, then expanded with literals derived from geometric-shape definitions.
- Symbolic Geometry Solver: Each theorem is represented as a conditional rule whose conclusion updates the current relation set when its premise matches.
- Symbolic Geometry Solver: After several theorem applications establish equations involving the unknown goal, the solver computes the goal by solving those equations.
- Search Strategy: Because random brute-force theorem search is inefficient, Inter-GPS first uses predicted theorems, then searches lower-order theorems before higher-order theorems.
- Theorem Predictor: The theorem predictor generates a pseudo-optimal theorem sequence token by token from the formal problem description using a transformer-based sequence-to-sequence model.
- Search Strategy: The search stops when it finds the goal or reaches the maximum permitted number of steps.
7 Experiments
Experiments on Geometry3K and GEOS evaluate Inter-GPS against neural baselines, search strategies, literal sources, and failure cases. Inter-GPS benefits from symbolic reasoning and predicted theorem sequences, while parsing and theorem coverage remain limitations.
- Implementation Details: Inter-GPS uses 17 geometry theorems, generates positive theorem sequences with 100 attempts, and permits at most 100 search steps.The theorem predictor uses a six-layer transformer with 12 attention heads and hidden size 768.
- Comparisons with Baselines: 57.5% overall accuracy on Geometry3K significantly exceeds all neural baselines, and Inter-GPS achieves state-of-the-art performance on GEOS.Using ground-truth formal language improves Inter-GPS accuracy by 20.8%.
- Search Strategies: The final predicted-theorem-plus-low-first strategy achieves the best overall accuracy, while prediction reduces average solving steps to 6.5.The strategy applies predicted theorems first and lower-order theorems in remaining search steps.
- Problem Parsers and Literal Sources: 57.5% accuracy with generated literals shows a small gap from ground-truth text literals, whereas annotated diagram literals improve accuracy by 17.5%.The results indicate stronger performance from the text parser than from the diagram parser.
- Searching Step Distribution: 65.97% of correctly solved problems are solved in two steps and 70.06% in five steps using the final Predict+Low-first strategy.The distribution is reported for correctly solved problems.
- Neural Geometry Solvers: Neural baselines perform poorly on Geometry3K, while replacing inputs with ground-truth formal annotations improves the Q+I baseline by 9.2%.The discussion attributes the baseline difficulty to limited data and dense implicit representations for logical reasoning.
- Failure Cases: Inter-GPS can fail because of inaccurate parsing, an incomplete theorem set, ambiguous or multiple diagram primitives, nested expressions, and complex combined shapes or shaded areas.These cases affect diagram parsing, text parsing, and symbolic solving.
8 Conclusion
The paper introduces Geometry3K, a 3,002-problem benchmark with dense formal-language descriptions, and Inter-GPS, which combines automatic parsing, theorem knowledge, and symbolic reasoning. Experiments report that Inter-GPS outperforms existing state-of-the-art methods by a large margin.
- Conclusion: Geometry3K contains 3,002 high-school geometry problems with dense formal-language descriptions.The benchmark is introduced as a large-scale resource for geometry problem solving.
- Conclusion: Inter-GPS automatically parses problems into formal language and performs symbolic reasoning over a theorem knowledge base to infer answers.A theorem predictor with low-first search generates theorem application sequences.
- Conclusion: Inter-GPS outperforms existing state-of-the-art methods by a large margin.The conclusion reports this outcome across the paper’s experiments.
Ethical Impact
The Geometry3K problems are collected from online open sources. The authors state that the work may inspire research in symbolic reasoning and interpretable models and facilitate education.
- Ethical Impact: Geometry3K problems are collected from online open sources.The dataset’s source is described in the ethical-impact discussion.
- Ethical Impact: The authors suggest that the work may inspire research in symbolic reasoning and interpretable models and facilitate education.This is presented as a potential impact of the work.
A Appendix
The appendix defines a geometry-language vocabulary of 91 predicates with corresponding literal templates, organized into six categories for formal descriptions.
- Geometry Language: The geometry language defines 91 predicates and corresponding literal templates.The templates use $ to denote an undetermined shape.
- Predicate Categories: The predicates are grouped into geometric shapes, unary attributes, general attributes, binary relations, A-IsXOf-B relations, and numerical attributes and relations.The six groups are documented in Tables 10–15.
- Predicate Categories: The appendix provides 20 predicates for geometric shapes and 9 for unary geometric attributes.These categories correspond to Tables 10 and 11.
- Predicate Categories: The appendix provides 17 predicates for general geometric attributes and 12 for binary geometric relations.These categories correspond to Tables 12 and 13.
- Predicate Categories: The appendix provides 15 predicates for A-IsXOf-B relations and 18 for numerical attributes and relations.These categories correspond to Tables 14 and 15.