# FGeo-TP: A Language Model-Enhanced Solver for Geometry Problems

arXiv: https://arxiv.org/abs/2402.09047 · HTML: https://mlsanity.com/paper/2402.09047/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 15 of its 29 references that are in the map.
- First posted on arXiv 14 Feb 2024.

## Builds on (most cited first, 15 of 15)

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BART: Denoising Sequence-to-Sequence Pre-training for Natural Language Generation, Translation, and Comprehension](https://mlsanity.com/paper/1910.13461/) (2019)
- [Sequence to Sequence Learning with Neural Networks](https://mlsanity.com/paper/1409.3215/) (2014)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning](https://mlsanity.com/paper/2105.04165/) (2021)
- [Deep symbolic regression: Recovering mathematical expressions from data via risk-seeking policy gradients](https://mlsanity.com/paper/1912.04871/) (2019)
- [GeoQA: A Geometric Question Answering Benchmark Towards Multimodal Numerical Reasoning](https://mlsanity.com/paper/2105.14517/) (2021)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expression](https://mlsanity.com/paper/2212.02746/) (2022)
- [Symbolic Regression via Neural-Guided Genetic Programming Population Seeding](https://mlsanity.com/paper/2111.00053/) (2021)
- [A Neural Network Solves, Explains, and Generates University Math Problems by Program Synthesis and Few-Shot Learning at Human Level](https://mlsanity.com/paper/2112.15594/) (2021)
- [CoLAKE: Contextualized Language and Knowledge Embedding](https://mlsanity.com/paper/2010.00309/) (2020)
- [MWP-BERT: Numeracy-Augmented Pre-training for Math Word Problem Solving](https://mlsanity.com/paper/2107.13435/) (2021)
- [PGDP5K: A Diagram Parsing Dataset for Plane Geometry Problems](https://mlsanity.com/paper/2205.09947/) (2022)

## Built on by (most cited first, 1 of 1)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)

## Abstract (arXiv)

The application of contemporary artificial intelligence techniques to address geometric problems and automated deductive proof has always been a grand challenge to the interdiscipline field of mathematics and artificial Intelligence. This is the fourth article in a series of our works, in our previous work, we established of a geometric formalized system known as FormalGeo. Moreover we annotated approximately 7000 geometric problems, forming the FormalGeo7k dataset. Despite the FGPS (Formal Geometry Problem Solver) can achieve interpretable algebraic equation solving and human-like deductive reasoning, it often experiences timeouts due to the complexity of the search strategy. In this paper, we introduced FGeo-TP (Theorem Predictor), which utilizes the language model to predict theorem sequences for solving geometry problems. We compared the effectiveness of various Transformer architectures, such as BART or T5, in theorem prediction, implementing pruning in the search process of FGPS, thereby improving its performance in solving geometry problems. Our results demonstrate a significant increase in the problem-solving rate of the language model-enhanced FGeo-TP on the FormalGeo7k dataset, rising from 39.7% to 80.86%. Furthermore, FGeo-TP exhibits notable reductions in solving time and search steps across problems of varying difficulty levels.
