SUFFI-GPSC: Sufficient Geometry Problem Solution Checking with Symbolic Computation and Logical Reasoning

Logical reasoning and computational solving skill play a vital role in geometry problem solving (GPS). The development of large-scale language models has facilitated the progress of artificial intelligence (AI) systems capable of solving math word problems and proving theorems. These models have achieved remarkable results across various geometry problem datasets, attracting significant attention in natural language processing community. However, it remains a challenge to effectively evaluate the logical correctness in the process of solution steps answered by the model due to the diversity of solution approaches. Therefore, we propose a powerful approach that can check the logical sufficiency of the solving process of given geometry problems step by step with symbolic computation and logical reasoning, called Sufficient Geometry problem solution checking (Suffi-GPSC). Suffi-GPSC divides the tasks into two categories, one focuses on equation expressions and checks whether the target equations are true with symbolic computation under the preconditions that contain a large number of equations. The other focuses on geometric relationships and checks whether the goal relation can be deduced within limited steps with logical reasoning by considering known facts as conditions and axiomatic knowledge as conditional rules. Inspired by the mainstream, a theorem predictor based on transfer text-to-text transformer(T5) has been designed to generate the theorem sequences for a more efficient and rational reasoning process. Extensive experiments on the Geometry3K dataset demonstrate that Suffi-GPSC achieves remarkable improvements.