基于非参数结构先验的多步定理预测

多步定理预测是几何问题求解中的核心挑战。现有神经符号方法严重依赖监督式参数模型，这类模型对不断演化的定理库泛化能力有限。在这项工作中，我们通过上下文学习（ICL）的视角探索免训练的定理预测。我们识别出一个关键的可扩展性瓶颈，称为结构漂移（Structural Drift）：随着推理深度增加，原始ICL的性能急剧退化，常常崩塌至接近零。我们将这一失败归因于LLM无法恢复潜在拓扑依赖，导致非结构化探索。为解决该问题，我们提出Theorem Precedence Graphs，将历史解题轨迹中的时间依赖编码为有向图，并施加显式拓扑约束，在推理时有效剪枝搜索空间。结合检索增强的图构建和逐步符号执行器，我们的方法使LLM能够在没有任何基于梯度优化的情况下充当结构化规划器。在FormalGeo7k基准上的实验表明，我们的方法达到89.29%的准确率，显著优于ICL基线，并与最先进的监督模型相当。这些结果表明，显式结构先验为扩展基于LLM的符号推理提供了一个有前景的方向。