Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

FGeo-DRL: Deductive Reasoning for Geometric Problems through Deep Reinforcement Learning

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

TL;DR

This work addresses automated geometric deductive reasoning by uniting a geometric formal language with reinforcement learning. The authors introduce FormalGeo and the FormalGeo7k dataset and build FGeoDRL, a neural-symbolic agent that uses a pre-trained DistilBERT policy and Monte Carlo Tree Search within a formal geometry environment. Experiments on FormalGeo7k demonstrate readable, verifiable theorem sequences and substantial solving capability, illustrating the approach's interpretability and effectiveness. The framework provides a scalable, verifiable pathway for geometric problem solving and establishes FormalGeo7k as a valuable resource for future research in neural-symbolic geometry reasoning.

Abstract

The human-like automatic deductive reasoning has always been one of the most challenging open problems in the interdiscipline of mathematics and artificial intelligence. This paper is the third in a series of our works. We built a neural-symbolic system, called FGeoDRL, to automatically perform human-like geometric deductive reasoning. The neural part is an AI agent based on reinforcement learning, capable of autonomously learning problem-solving methods from the feedback of a formalized environment, without the need for human supervision. It leverages a pre-trained natural language model to establish a policy network for theorem selection and employ Monte Carlo Tree Search for heuristic exploration. The symbolic part is a reinforcement learning environment based on geometry formalization theory and FormalGeo, which models GPS as a Markov Decision Process. In this formal symbolic system, the known conditions and objectives of the problem form the state space, while the set of theorems forms the action space. Leveraging FGeoDRL, we have achieved readable and verifiable automated solutions to geometric problems. Experiments conducted on the formalgeo7k dataset have achieved a problem-solving success rate of 86.40%. The project is available at https://github.com/PersonNoName/FGeoDRL.

FGeo-DRL: Deductive Reasoning for Geometric Problems through Deep Reinforcement Learning

TL;DR

This work addresses automated geometric deductive reasoning by uniting a geometric formal language with reinforcement learning. The authors introduce FormalGeo and the FormalGeo7k dataset and build FGeoDRL, a neural-symbolic agent that uses a pre-trained DistilBERT policy and Monte Carlo Tree Search within a formal geometry environment. Experiments on FormalGeo7k demonstrate readable, verifiable theorem sequences and substantial solving capability, illustrating the approach's interpretability and effectiveness. The framework provides a scalable, verifiable pathway for geometric problem solving and establishes FormalGeo7k as a valuable resource for future research in neural-symbolic geometry reasoning.

Abstract

The human-like automatic deductive reasoning has always been one of the most challenging open problems in the interdiscipline of mathematics and artificial intelligence. This paper is the third in a series of our works. We built a neural-symbolic system, called FGeoDRL, to automatically perform human-like geometric deductive reasoning. The neural part is an AI agent based on reinforcement learning, capable of autonomously learning problem-solving methods from the feedback of a formalized environment, without the need for human supervision. It leverages a pre-trained natural language model to establish a policy network for theorem selection and employ Monte Carlo Tree Search for heuristic exploration. The symbolic part is a reinforcement learning environment based on geometry formalization theory and FormalGeo, which models GPS as a Markov Decision Process. In this formal symbolic system, the known conditions and objectives of the problem form the state space, while the set of theorems forms the action space. Leveraging FGeoDRL, we have achieved readable and verifiable automated solutions to geometric problems. Experiments conducted on the formalgeo7k dataset have achieved a problem-solving success rate of 86.40%. The project is available at https://github.com/PersonNoName/FGeoDRL.
Paper Structure (17 sections, 6 equations, 3 figures, 4 tables, 1 algorithm)

This paper contains 17 sections, 6 equations, 3 figures, 4 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Related Work
  3. Datasets for Geometry Problems Solving
  4. Reinforcement Learning for Geometry Problems Solving
  5. Geometry Formal System
  6. Geometry Formal Language
  7. FormalGeo7k Dataset
  8. Reasoner
  9. Environment
  10. Guidance
  11. Monte Carlo Tree Search
  12. Experiments
  13. Train Method
  14. Policy Network Datasets
  15. Baseline
  16. ...and 2 more sections

Figures (3)

  • Figure 1: Formal Language for Geometry Problems
  • Figure 2: The overall architecture of the FGeoDRL model framework.
  • Figure 3: Performance of different strategies on the dataset