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\cite{FormalGeo}, which models GPS as a Markov Decision Process\cite{MDP}. 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.

翻译：类人自动演绎推理一直是数学与人工智能交叉领域中最具挑战性的开放性问题之一。本文是本系列工作的第三篇。我们构建了一个名为FGeoDRL的神经符号系统，用于自动执行类人几何演绎推理。其中，神经部分是一个基于强化学习的AI智能体，能够从形式化环境的反馈中自主学习解题方法，无需人工监督。它利用预训练的自然语言模型建立定理选择的策略网络，并采用蒙特卡洛树搜索进行启发式探索。符号部分是一个基于几何形式化理论和FormalGeo\cite{FormalGeo}的强化学习环境，该环境将GPS建模为马尔可夫决策过程\cite{MDP}。在该形式化符号系统中，问题的已知条件和目标构成状态空间，定理集构成动作空间。借助FGeoDRL，我们实现了可读且可验证的几何问题自动化求解。在formalgeo7k数据集上进行的实验达到了86.40%的解题成功率。该项目可在https://github.com/PersonNoName/FGeoDRL获取。