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.

翻译：当代人工智能技术在几何问题求解与自动演绎证明中的应用，始终是数学与人工智能交叉领域的重大挑战。本文是我们系列研究的第四篇工作。在前期研究中，我们建立了名为FormalGeo的几何形式化系统，并标注了约7000道几何问题，形成了FormalGeo7k数据集。尽管FGPS（形式化几何问题求解器）能够实现可解释的代数方程求解和类人演绎推理，但受限于搜索策略的复杂性，常出现超时现象。本文引入FGeo-TP（定理预测器），利用语言模型预测几何问题求解所需的定理序列。我们比较了BART、T5等不同Transformer架构在定理预测中的有效性，通过实施FGPS搜索过程剪枝，提升了几何问题求解性能。实验结果表明，经语言模型增强的FGeo-TP在FormalGeo7k数据集上的解题成功率显著提升，从39.7%跃升至80.86%。此外，FGeo-TP在不同难度等级的问题求解中，均表现出求解时间与搜索步数的显著降低。