Non-Parametric Structural Priors for Geometry Theorem Prediction

Multi-step theorem prediction is a central challenge in geometry problem solving. Existing neural–symbolic approaches rely heavily on supervised parametric models, which exhibit limited generalization to evolving theorem libraries. In this work, we explore training-free theorem prediction through the lens of in-context learning (ICL). We identify a critical scalability bottleneck, termed Structural Drift: as reasoning depth increases, the performance of vanilla ICL degrades sharply. We attribute this to the LLM’s inability to recover latent topological dependencies, leading to unstructured exploration. To address this issue, we propose Theorem Precedence Graphs, which encode temporal dependencies from historical solution traces as directed graphs, and impose explicit topological constraints that effectively prune the search space during inference. Coupled with retrieval-augmented graph construction and a stepwise symbolic executor, our approach enables LLMs to act as structured planners without any gradient-based optimization. Experiments on the FormalGeo7k benchmark show that our method achieves 89.29\% accuracy, substantially outperforming ICL baselines and matching state-of-the-art supervised models. These results indicate that explicit structural priors offer a promising direction for scaling LLM-based symbolic reasoning.

Solving multi-step geometry problems requires making many decisions in the right order — like navigating a road with many intersections. One wrong turn makes it hard to find the correct path forward. Current AI methods rely on supervised training, which struggles when new theorems are introduced. We developed a training-free approach that uses large language models (LLMs) as structured problem-solvers without any gradient-based optimization. The key insight is learning from history: we build Theorem Precedence Graphs that record how previous solutions successfully navigated through geometric problems. These graphs act as a guide, showing the LLM which theorems work well together and in what order. Additionally, we incorporate a symbolic solver that provides real-time feedback at each step, allowing the AI to verify correctness and adjust its reasoning accordingly — similar to learning from both a mentor's past experiences and immediate feedback. Across multiple geometry problem datasets, our method achieves strong results, substantially outperforming existing approaches. In the education sector, this means AI tutoring systems could better guide students through complex geometric reasoning, explaining not just the answer but the logical sequence of steps needed to reach it.