Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Yiming He, Jia Zou, Xiaokai Zhang, Na Zhu, Tuo Leng

TL;DR

The paper tackles automated plane geometry problem solving by merging a language-model–based Theorem Predictor with the existing geometry solver FGPS to prune the search space. Using the FormalGeo7k dataset, the authors train Transformer models to predict theorem sequences, with BART-base achieving the best theorem-sequence matching. Incorporating predictions yields FGeo-TP, which reaches up to an $80.86\%$ problem-solving rate and significantly reduces solving time and search steps compared to FGPS. A hybrid approach combining FGeo-TP with FGPS provides additional gains, and future work will focus on improving predictor accuracy and evaluating on IMO-level geometry tasks.

Abstract

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.

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

TL;DR

The paper tackles automated plane geometry problem solving by merging a language-model–based Theorem Predictor with the existing geometry solver FGPS to prune the search space. Using the FormalGeo7k dataset, the authors train Transformer models to predict theorem sequences, with BART-base achieving the best theorem-sequence matching. Incorporating predictions yields FGeo-TP, which reaches up to an problem-solving rate and significantly reduces solving time and search steps compared to FGPS. A hybrid approach combining FGeo-TP with FGPS provides additional gains, and future work will focus on improving predictor accuracy and evaluating on IMO-level geometry tasks.

Abstract

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.
Paper Structure (15 sections, 3 equations, 4 figures, 7 tables)

This paper contains 15 sections, 3 equations, 4 figures, 7 tables.

Table of Contents

  1. Introduction
  2. Related Work
  3. Datasets for Geometry Problem Solving
  4. Geometry Problem Solving
  5. Pre-training Model In NLP
  6. Geometry Problem Solver
  7. FGPS
  8. FGeo-TP
  9. Experiment
  10. Theorem Sequence Prediction
  11. Experimental Results of FGeo-TP
  12. Solving Time and Step
  13. The Combined Approach of FGeo-TP and FGPS
  14. Conclusion
  15. Experimental Results

Figures (4)

  • Figure 1: An example from FormalGeo7k, including formal annotations.
  • Figure 2: The architecture of FGeo-TP
  • Figure 3: solving time(s) at different difficulty levels.
  • Figure 4: solving step at different difficulty levels.