用结构先验让大模型高效推理几何定理,无需训练也能精准预测。
Non-Parametric Structural Priors for Geometry Theorem Prediction
- 构建定理依赖图,显式约束推理路径,避免盲目搜索。
- 在FormalGeo7k上达89.29%准确率,超越无监督基线。
- 适合需要可解释、可扩展符号推理的AI数学系统开发者。
多步定理预测是几何问题求解的核心挑战。现有神经符号方法严重依赖有监督参数化模型,难以泛化到不断演化的定理库。本文探索无训练的定理预测,基于上下文学习(ICL)。我们发现关键瓶颈——结构漂移:随着推理深度增加,原始ICL性能急剧下降,常趋近于零。原因在于大模型无法恢复潜在拓扑依赖,导致无序探索。为此,我们提出定理前序图,将历史解题轨迹中的时序依赖编码为有向图,并在推理中施加显式拓扑约束以有效剪枝搜索空间。结合检索增强的图构建与分步符号执行器,我们的方法使大模型在无需梯度优化的情况下充当结构化规划器。在FormalGeo7k基准上的实验表明,该方法达到89.29%准确率,显著优于ICL基线,媲美最先进有监督模型。结果表明,显式结构先验为大模型符号推理的可扩展性提供了新方向。
原文摘要 · Abstract (English)
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, often collapsing to near zero. We attribute this failure 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.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品;中文卡片由大模型生成,请以原文为准。