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

多步定理预测是自动推理的核心挑战。现有神经符号方法依赖监督参数模型，泛化性受限。本文探索通过上下文学习进行免训练定理预测，发现“结构漂移”瓶颈：随推理深度增加，性能急剧下降。归因于大语言模型无法恢复潜在拓扑依赖。为此，提出“定理优先图”，将历史求解轨迹编码为有向图并施加拓扑约束以剪枝搜索空间。结合检索增强构建与逐步符号执行器，使大模型无需梯度优化即可作为结构化规划器。在 FormalGeo7k 基准上准确率达 89.29%，显著优于基线并媲美最先进监督模型。