GeoTree: A Dynamic Tree-Based Geometry Problem Solver Through LLM-Symbolic Reasoning

Geometry problem solving (GPS) requires high-level symbolic and logical reasoning based on geometry theorem knowledge to arrive at the answer. Despite the remarkable advances achieved by Large Language Models (LLMs) in various problem-solving tasks, they still struggle to perform rigorous multi-step geometry reasoning, which is essential for GPS. In this paper, we propose a dynamic tree-based geometry problem solver named GeoTree, which combines a knowledgeable LLM with a rigorous symbolic solver to perform geometry reasoning cooperatively. Specifically, an iterative multi-step geometry reasoning process is performed dynamically based on a tree-like structure, thereby emulating divergent and deliberate human problem-solving thinking. Each geometry reasoning step is completed collaboratively through four components, consisting of Theorem Seeker, Symbolic Solver, Evaluator, and Controller. First, Theorem Seeker prompts LLMs to seek out candidate theorems with their inherent geometry theorem knowledge. Subsequently, Symbolic Solver applies the theorems on the known conditions to obtain new additional conditions. Then, Evaluator assesses the availability of the theorems and prompts LLMs to judge the usefulness of these new conditions for the problem target, which serves as the heuristic guidance for subsequent reasoning. Finally, Controller determines the termination state, which decides whether to continue invoking the other three components for further attempts. Extensive experiments on Geometry3K demonstrate the superiority of GeoTree in accuracy, efficiency, and explainability.