Search

Human-like automatic deductive reasoning has always been one of the most challenging open problems in the interdisciplinary field of mathematics and artificial intelligence. This paper is the third in a series of our works. We built a neural-symbolic system, named FGeo-DRL, to automatically perform human-like geometric deductive reasoning. The neural part is an AI agent based on deep 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 geometric problem solving (GPS) as a Markov Decision Process (MDP). In the formal symbolic system, the symmetry of plane geometric transformations ensures the uniqueness of geometric problems when converted into states. Finally, the known conditions and objectives of the problem form the state space, while the set of theorems forms the action space. Leveraging FGeo-DRL, 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%. [ABSTRACT FROM AUTHOR]

Geometric problem solving (GPS) has always been a long-standing challenge in the fields of automated reasoning. Its problem representation and solution process embody rich symmetry. This paper is the second in a series of our works. Based on the Geometry Formalization Theory and the FormalGeo geometric formal system, we have developed the Formal Geometric Problem Solver (FGPS) in Python 3.10, which can serve as an interactive assistant or as an automated problem solver. FGPS is capable of executing geometric predicate logic and performing relational reasoning and algebraic computation, ultimately achieving readable, traceable, and verifiable automated solutions for geometric problems. We observed that symmetry phenomena exist at various levels within FGPS and utilized these symmetries to further refine the system's design. FGPS employs symbols to represent geometric shapes and transforms various geometric patterns into a set of symbolic operation rules. This maintains symmetry in basic transformations, shape constructions, and the application of theorems. Moreover, we also have annotated the formalgeo7k dataset, which contains 6981 geometry problems with detailed formal language descriptions and solutions. Experiments on formalgeo7k validate the correctness and utility of the FGPS. The forward search method with random strategy achieved a 39.71% problem-solving success rate. [ABSTRACT FROM AUTHOR]