On Multi-Step Theorem Prediction via Non-Parametric Structural Priors

日期: 2026-03-05
arXiv: 2603.04852
代码: 无（暂未公开）
领域: LLM推理
关键词: theorem prediction, structural prior, ICL, formal geometry, priority graph

一句话总结

Pri-TPG 通过定理优先级图编码解决方案结构的时间依赖关系，结合 ICL 扩展在多步定理预测中达到 89.29% 准确率，匹配训练型方法（88.36%）且较 Vanilla ICL（26.29%）提升 63%。

研究背景与动机

1. 领域现状：多步定理预测（给定几何条件，预测下一步应用什么定理）是自动化推理的核心挑战，训练型方法（如 FGeo-HyperGNet）需要大量标注数据。
2. 现有痛点：(1) Vanilla ICL 在多步推理中严重退化（结构漂移）——随着推理步数增加，模型逐渐偏离正确的推理路径；(2) 搜索空间大（~200 个定理），随机探索效率极低。
3. 核心矛盾：多步推理需要对定理间的依赖关系有结构化理解，但 ICL 仅通过示例隐式学习，缺乏显式的结构约束。
4. 切入角度：从解决方案痕迹中提取定理优先级图——显式编码"定理 A 常在定理 B 之后使用"的结构信息，压缩搜索空间。

方法详解

整体框架

Pri-TPG 三步：(1) 从训练集解决方案中构建定理优先级图（DAG）；(2) 给定当前状态，用优先级图约束候选定理集合（~200 → ~30）；(3) 在约束集合上用 ICL + 多模态检索选择定理。

关键设计

1. 定理优先级图（Priority Graph）：

   • 从解决方案痕迹中提取：如果定理 B 在定理 A 之后出现，建立边 A→B
   • 非参数方法——直接从数据统计，无需训练
   • 搜索空间压缩：\(O(|\mathcal{L}|) \to O(|\mathcal{L}_{qt}|)\)，约 90% 压缩（~200 → ~30）

2. 结构漂移识别：

   • 发现 Vanilla ICL 在长链推理中的系统性退化
   • 前几步正确率高但随步数增涨快速下降
   • 优先级图约束有效防止偏移到无关定理

3. 多模态检索：

   • 利用问题的几何图形和条件文本做双模态检索
   • 从训练集中找到结构相似的问题作为 ICL 示例

实验关键数据

主实验

方法	FormalGeo7K 准确率	Geometry3K 准确率	类型
Vanilla ICL	26.29%	-	无训练
FGeo-HyperGNet	88.36%	92.5%	训练型
Pri-TPG (GPT-5.2)	89.29%	95.16%	无训练

难度分层（FormalGeo7K）

难度	L1	L2	L3	L4	L5	L6
Pri-TPG	99.16%	95.2%	88.1%	72.3%	55.0%	30%
Vanilla ICL	45%	30%	18%	10%	5%	2%

关键发现

• Pri-TPG 无需训练即匹配训练型 SOTA（89.29% vs 88.36%）
• vs Vanilla ICL +63% 绝对提升，证明结构先验的关键作用
• 搜索空间 90% 压缩（~200 → ~30）大幅降低 ICL 难度
• 难题（L6）仍然困难（30%），但 Vanilla ICL 几乎为零（2%）

亮点与洞察

• 非参数先验 + ICL 的优雅结合：用数据统计的结构先验指导 LLM 的 ICL，两者互补
• 结构漂移的识别很有价值：解释了为什么 ICL 在多步推理中退化——不是能力不足而是搜索空间过大导致偏移
• 搜索空间压缩思路可推广：在其他需要多步决策的任务（规划、定理证明）中，类似的先验约束同样适用

局限性 / 可改进方向

• 优先级图从训练集统计，对分布外定理组合可能不适用
• 仅验证了几何定理预测，其他数学领域待验证
• 难题性能仍有较大提升空间
• 依赖 GPT-5.2 等强 LLM

评分

• 新颖性: ⭐⭐⭐⭐ 定理优先级图+ICL的非参数方案新颖实用
• 实验充分度: ⭐⭐⭐⭐ 多数据集+难度分层+消融
• 写作质量: ⭐⭐⭐⭐ 结构清晰，问题分析到位
• 价值: ⭐⭐⭐⭐ 对自动化推理有启发意义