本文提出了一种无需训练的长程推理方案 Pri-TPG，通过引入结构先验解决大语言模型在几何证明任务中出现的"结构漂移"问题。
从内容检索到结构检索，一种 Training-free 的长程推理方案
大语言模型做数学证明时，有一个很反常的现象：
问题一旦变长，模型的表现往往不是缓慢下降，而是迅速崩溃。
在 FormalGeo7K 几何推理基准上，Vanilla ICL 在浅层问题 L1 上还能达到 52.19% 的准确率，但到了 L3，只剩下 7.89%；在更长的 L5 和 L6 推理任务上，准确率直接降到 0。
而加入结构先验之后，Pri-TPG 在同样使用 GPT-5 mini 的情况下，整体准确率从 26.29% 提升到了 84.42%。使用 GPT-5.2 时，最终达到 89.29%。
论文将这种普通 ICL 随推理深度增加而快速失效的现象称为：
Structural Drift，结构漂移。
这个概念揭示了一个重要问题：
LLM 可能知道每一个定理是什么意思，却不知道这些定理应该按照什么顺序被组织起来。
于是，一个比"如何训练出更强模型"更具体的问题出现了：
能不能不更新模型参数，而是给 LLM 提供一套外部结构，让它只在更可能正确的证明路径中进行搜索？
这就是论文 Non-Parametric Structural Priors for Geometry Theorem Prediction 想解决的问题。
论文信息卡
| 项目 | 内容 |
|---|---|
| 论文标题 | Non-Parametric Structural Priors for Geometry Theorem Prediction |
| 核心方法 | Pri-TPG |
| 研究任务 | 多步几何定理预测 |
| 技术路线 | RAG + Theorem Precedence Graph + Symbolic Execution |
| 核心特点 | Training-free，无需针对定理预测任务进行梯度训练 |
| 主要数据集 | FormalGeo7K、Geometry3K、GeoQA |
| 主要结果 | FormalGeo7K 上达到 89.29% |
| 核心关键词 | Structural Drift、Structural Prior、LLM Planner、Neural-Symbolic Reasoning |
一句话概括：
Pri-TPG 不直接检索答案，而是检索相似问题的证明结构，再用这些结构约束 LLM 的下一步动作。
01. 几何证明为什么本质上是一个搜索问题？
一道人类看来并不复杂的几何题，对自动推理系统来说，往往不是单步问答，而是一个连续决策过程。
例如，一条完整证明可能需要依次完成：
证明两条边相等
↓
判断三角形全等
↓
得到对应角相等
↓
构造相似三角形
↓
推出目标比例这里的关键不只是"选择一个正确的定理"。
更重要的是：
当前选择的定理，必须建立在此前已经得到的事实之上。
如果某个定理的前置条件还没有满足，那么即使它在语义上与目标相关，也不能被执行。
从形式上看，一道几何题可以被描述成：
初始状态 S₀
↓ 使用定理 a₁
状态 S₁
↓ 使用定理 a₂
状态 S₂
↓
……
↓
最终状态 Sₜ 满足目标 g符号执行器能够检查每一步是否合法，但它无法自动告诉模型：
在数百条定理中，下一步最应该选哪一条？
假设定理库中有 300 条定理，一条证明需要 H 步，那么在最朴素的情况下，搜索空间会接近：
300ᴴ推理链越长，错误分支越多。
因此，几何证明的难点不只是知识不足，而是：
如何在指数级增长的候选路径中，持续找到有效的下一步。
02. Structural Drift：知道定理，却不知道证明结构
最直接的想法，是使用 In-Context Learning。
给 LLM 几个历史证明示例，让它模仿示例，逐步选择定理。
但论文发现，Vanilla ICL 在浅层问题上尚且有效，随着证明长度增加，性能会快速坍塌。
作者认为，原因在于普通 ICL 获得的是"内容示例"，却没有获得显式的"结构约束"。
| LLM 可能知道的内容 | LLM 未必掌握的结构 |
|---|---|
| 勾股定理是什么 | 当前是否满足勾股定理的前置条件 |
| 三角形全等有哪些判定方式 | 哪一种判定应该先使用 |
| 哪些定理与角度、长度相关 | 哪些定理在当前状态下不可执行 |
| 某条定理与目标语义相近 | 这条定理是否位于正确证明路径上 |
| 如何生成下一步解释 | 失败后应切换到哪条分支 |
可以把问题进一步压缩成两句话：
定理语义相关，不等于当前状态可执行。选对局部步骤，不等于维护全局证明结构。
普通 ICL 更像是在整个定理库上进行平坦选择。
每一步都面对大量候选，越往后走，早期的小错误越容易不断放大，最终使整条证明偏离正确路径。
这就是 Structural Drift。
03. Pri-TPG：检索的不是知识，而是证明结构
传统 RAG 通常在做什么？
输入问题
↓
检索相关文本或知识
↓
放入 Prompt
↓
让 LLM 生成答案它解决的是：
模型应该知道什么？
Pri-TPG 的做法不同。
它检索的是与当前问题相似的历史几何题，再从这些题的证明轨迹中提取：
- 哪些定理经常出现；
- 哪些定理通常先出现；
- 哪些定理通常在另一些定理之后使用；
- 哪些局部推理结构可能适用于当前问题。
因此，Pri-TPG 更接近：
输入问题
↓
检索相似证明
↓
提取定理使用顺序
↓
构建定理优先图
↓
约束下一步推理两者的区别可以概括为：
| 传统 RAG | Pri-TPG |
|---|---|
| 检索事实、段落、文档 | 检索历史证明轨迹 |
| 回答"应该知道什么" | 回答"应该先做什么、后做什么" |
| 结果以文本形式加入 Prompt | 结果被转化为图结构 |
| 主要增强内容 | 主要约束行动空间 |
| Content-Augmented | Structure-Augmented |
所以，Pri-TPG 的关键并不是简单增加检索，而是：
把检索结果从"内容上下文"进一步转化为"推理结构"。
04. 什么是 Theorem Precedence Graph？
Pri-TPG 的核心结构叫作：
Theorem Precedence Graph，定理优先关系图。
它是一张有向图。
| 图元素 | 含义 |
|---|---|
| 节点 (v) | 一条定理 |
| 边 () | 定理 (u) 产生的结果，可支持后续使用定理 (v) |
| 边权重 | 该定理转移在相似历史证明中出现的频率 |
| START 节点 | 表示证明开始时更可能优先使用的定理 |
例如，一条局部路径可能是：
等腰三角形判定
↓
等腰三角形性质
↓
角相等
↓
相似三角形判定相比直接从 300 条定理中任意选择，TPG 会告诉模型：
你刚刚使用了某个定理，那么接下来更合理的候选，通常位于它在图中的后继节点。
TPG 并不是一条固定证明链。
它更像一个局部导航图：
| 固定证明链 | TPG |
|---|---|
| 只能沿一条路径执行 | 可以保留多个可行后继 |
| 接近模板复制 | 更接近结构约束 |
| 对变化较敏感 | 允许 LLM 在局部图中选择 |
| 缺乏灵活性 | 保留一定规划自由度 |
论文指出，在 FormalGeo7K 的实验中，经过候选过滤后，每一步的定理数量大约可以从 300 条缩小到 30 条，相当于单步缩减约 90% 的搜索空间。
05. Pri-TPG 并不是只使用一张静态图
如果只是统计所有历史证明中的定理顺序，再构建一张全局图，会有一个明显问题：
不同题目需要的定理结构并不一样。
圆、三角形、平行四边形、长度计算、角度证明，对应的证明路线差别很大。
因此，Pri-TPG 对结构先验进行了逐层细化。
系统从全局定理库出发，通过检索、图构建和符号验证，逐步将搜索空间缩小到当前状态下最可能有效的一小组定理。
三层结构先验
| 层级 | 输入 | 主要操作 | 解决的问题 |
|---|---|---|---|
| Global Prior | 所有历史证明轨迹 | 统计全局定理先后关系 | 建立领域级结构 |
| Query-Adaptive Prior | 当前问题及相似历史题 | 构建问题相关候选池与局部 TPG | 排除与当前题目无关的定理 |
| State-Aware Prior | 当前符号状态和上一步动作 | 符号剪枝、结构定位、候选排序 | 排除当前不可执行或结构不合理的动作 |
第一层：Global Prior
全局先验来自所有历史证明轨迹。
它回答的是：
在整个数据集中，哪些定理之间经常存在先后关系？
这一层提供的是领域级结构。
但它过于宽泛，因为全局图中包含大量与当前问题无关的定理。
第二层：Query-Adaptive Prior
Pri-TPG 会根据当前问题检索相似历史题。
检索条件包括：
| 输入模态 | 作用 |
|---|---|
| 题目文本 | 捕捉语义和目标类型 |
| 几何图像 | 捕捉图形结构 |
| 初始形式化状态 | 捕捉已经成立的符号事实 |
系统使用多模态编码器将这些信息映射到统一向量空间，再从训练集中检索 Top-K 个相似问题。
接着，它会提取这些相似问题使用过的定理，并合并对应的 TPG，形成当前问题专属的：
候选定理集合 Lq
查询相关图 Gq这一层回答的是：
对这道题来说，哪些定理和哪些定理顺序更可能有用？
如果某个必须使用的定理没有被检索出来，那么无论 LLM 推理能力多强，后续都不可能完成证明。
论文中不同检索规模的结果如下：
| Top-K | Total | Easy | Medium | Hard |
|---|---|---|---|---|
| 15 | 71.86 | 83.37 | 52.96 | 28.69 |
| 30 | 79.00 | 94.39 | 61.64 | 30.33 |
| 100 | 80.29 | 95.32 | 64.30 | 30.33 |
| 200 | 84.42 | 96.14 | 73.05 | 40.98 |
随着 K 增大，整体性能持续提升，尤其是中高难度问题。原因是长链证明需要召回更多专门定理，一旦漏掉关键定理，后续规划便无法完成。
第三层：State-Aware Prior
即使某条定理出现在相似题中，也不代表它现在可以使用。
因此，Pri-TPG 会根据每一步的当前状态继续剪枝。
| 机制 | 做法 | 作用 |
|---|---|---|
| Symbolic Pruning | 检查候选定理的前置条件是否满足 | 排除数学上不可执行的动作 |
| Structural Localization | 优先保留上一步定理在图中的后继节点 | 保持局部推理连贯 |
| Candidate Prioritization | 根据目标、图结构和历史进行排序 | 将高价值候选优先交给 LLM |
最终，系统会从：
全局定理库
↓
问题相关定理集合
↓
当前状态可执行的定理
↓
当前图位置合理的定理不断缩小搜索空间。
06. LLM、图和符号执行器分别负责什么？
Pri-TPG 不是纯 LLM 系统，也不是纯符号搜索系统。
它是一套神经—符号闭环。
| 组件 | 角色 | 主要职责 |
|---|---|---|
| LLM | Planner | 从候选定理中选择下一步 |
| TPG | Structural Prior | 提供定理先后关系，缩小动作空间 |
| Symbolic Solver | Executor / Verifier | 检查前置条件、执行定理、更新状态 |
| Retrieval Module | Retriever | 从历史题中召回相关证明结构 |
| Current State | Environment State | 记录当前已知事实和新增事实 |
整个循环是：
LLM 选择定理
↓
符号执行器验证并执行
↓
更新当前状态
↓
根据新状态重新过滤图和候选
↓
LLM 再次选择这与典型 Agent 的工作方式高度相似：
| Agent 范式 | Pri-TPG 对应组件 |
|---|---|
| Think | LLM 分析候选 |
| Act | 选择一条定理 |
| Environment Feedback | 符号执行器返回结果 |
| Update State | 更新符号事实 |
| Replan | 根据新状态重新选择 |
所以，虽然论文的任务是几何证明，但它研究的其实也是一个更一般的 Agent 问题：
如何让 LLM 在动作空间很大、规则严格、反馈明确的环境中进行长程规划？
07. 候选定理不是简单按相似度排序
Pri-TPG 不只是把检索到的定理列出来。
它还会依据三类信息进行候选排序：
| 评分项 | 含义 | 直觉 |
|---|---|---|
| (s_{goal}) | 候选定理与最终目标的相关性 | 更接近目标的定理优先 |
| (s_{graph}) | 候选定理与当前图位置的结构关系 | 上一步定理的后继优先 |
| (s_{hist}) | 历史重复和失败惩罚 | 避免循环和重复无效尝试 |
整体形式为：
候选得分 = 目标相关性 + 图结构相关性 - 历史重复惩罚这套评分不会替代 LLM 做最终决策，而是把更可能有效的候选排到前面，再让 LLM 结合题目、状态和历史轨迹进行判断。
08. 为什么必须是闭环，而不能一次生成完整证明？
作者还设计了一个 Single-pass 版本。
这个版本仍然拥有 query-adaptive TPG，但要求 LLM 一次性生成完整定理序列，符号执行器只在最后验证。
结果如下：
| 方法 | Overall | Easy | Medium | Hard |
|---|---|---|---|---|
| Vanilla ICL | 26.3 | 39.7 | 6.9 | 0.0 |
| Single-pass | 34.3 | 53.3 | 5.7 | 0.0 |
| Pri-TPG | 84.3 | 96.1 | 73.0 | 41.0 |
即使已经有了结构先验，Single-pass 在 Hard 任务上仍然为 0。
这说明，仅靠一次性规划无法应对长链证明中的中途错误。
| Single-pass | Iterative Pri-TPG |
|---|---|
| 一次生成完整序列 | 每次只选择一步 |
| 最后统一验证 | 每一步立即验证 |
| 中途无法修正 | 可以根据反馈重规划 |
| 错误会沿整条链累积 | 错误能被及时截断 |
| 长程任务容易崩溃 | 中长程任务明显更稳定 |
形式推理必须是闭环的：
规划
↓
执行
↓
反馈
↓
修正
Single-pass 即使拥有 query-adaptive prior，在 Hard 任务上仍然为 0；逐步符号反馈对于中长链证明至关重要。
一句话总结：
图结构解决"往哪里走"，符号反馈解决"走错以后怎么办"。
09. 实验到底证明了什么？
真正精读实验，不应该只看谁的分数更高。
更重要的是：
每个实验在验证哪一个研究假设？
Pri-TPG 的实验可以组成一条清晰的证据链。
主实验结果
| 方法 | 是否训练 | Total | L1 | L2 | L3 | L4 | L5 | L6 |
|---|---|---|---|---|---|---|---|---|
| Vanilla ICL（GPT-5 mini） | 否 | 26.29 | 52.19 | 23.67 | 7.89 | 5.10 | 0.00 | 0.00 |
| Pri-TPG（GPT-5 mini） | 否 | 84.42 | 98.54 | 93.09 | 78.20 | 64.33 | 58.06 | 23.33 |
| Pri-TPG（GPT-5.2） | 否 | 89.29 | 99.16 | 96.28 | 87.92 | 77.07 | 66.13 | 30.00 |
| FGeo-HyperGNet | 是 | 88.36 | 96.24 | 91.76 | 87.59 | 82.17 | 56.45 | 56.67 |
从表中可以看到：
- Pri-TPG 在 L1 至 L5 上表现很强；
- Vanilla ICL 随深度增加快速崩溃；
- Pri-TPG 在 L6 上仍有明显下降；
- 训练式专门模型在极长链推理上仍保有优势。
证据链一：RAG 与 TPG 分别做了什么？
| 设置 | Iterative | RAG | TPG | Total | Hard |
|---|---|---|---|---|---|
| Vanilla ICL | ✓ | ✗ | ✗ | 26.29 | 0.00 |
| w/o TPG | ✓ | ✓ | ✗ | 72.64 | 22.95 |
| Pri-TPG | ✓ | ✓ | ✓ | 84.42 | 40.98 |
这组实验说明：
| 模块 | 主要贡献 |
|---|---|
| RAG | 缩小候选定理范围 |
| TPG | 组织定理先后关系 |
| Iterative Feedback | 支持中途纠错 |
RAG 将性能从 26.29% 提升到 72.64%，说明候选缩小非常重要。
TPG 又将性能从 72.64% 提升到 84.42%，说明：
找到相关定理，不等于知道这些定理该如何组织。
证据链二：结构先验越精确，效果越好
| 设置 | Total | Easy | Medium | Hard |
|---|---|---|---|---|
| Vanilla ICL | 26.29 | 39.65 | 6.86 | 0.00 |
| Global Prior | 29.71 | 40.70 | 14.89 | 4.10 |
| Query-Adaptive Prior | 58.43 | 72.40 | 41.61 | 18.85 |
| State-Aware Pri-TPG | 84.42 | 96.14 | 73.05 | 40.98 |
这组结果说明，单纯使用全局图帮助有限。
真正明显的提升来自：
- 让结构与当前问题相关；
- 让结构与当前状态相关。
因此，结构先验不是越大越好，而是：
越贴近当前问题和当前推理状态越好。
证据链三：方法是否依赖特定 LLM？
| Backbone | Total | Easy | Medium | Hard |
|---|---|---|---|---|
| DeepSeek v3.2 | 83.57 | 95.56 | 72.10 | 39.34 |
| GPT-5 mini | 84.42 | 96.14 | 73.00 | 40.98 |
| Claude 4.5 Sonnet | 87.07 | 97.31 | 77.54 | 48.36 |
| Gemini 3.0 Pro | 88.43 | 97.54 | 81.56 | 48.36 |
| GPT-5.2 | 89.29 | 97.89 | 83.92 | 48.36 |
不同模型的绝对成绩存在差异，但接入 Pri-TPG 后都取得了较强表现。
这意味着 Pri-TPG 更像一个可插拔的外部推理脚手架，而不是某个模型专属技巧。
总结卡：
RAG 解决"候选有哪些"，TPG 解决"候选如何组织"，Symbolic Feedback 解决"错误如何被及时发现"。
10. 89.29% 应该如何正确理解？
89.29% 是一个很强的结果，但需要注意它的评估边界。
| 评估条件 | 具体设置 |
|---|---|
| 输入形式 | 使用 ground-truth formal inputs |
| 主要评估内容 | 定理规划与符号搜索 |
| 是否包含完整自动形式化 | 否 |
| 每题时间限制 | 600 秒 |
| 最大推理步数 | 20 |
| Top-K 检索规模 | 200 |
| 最大恢复尝试 | 3 |
| 是否多次调用 LLM | 是 |
论文为了隔离"推理与搜索能力"，直接向所有方法提供了正确的形式化输入。
也就是说，系统并不是从完全原始的自然语言和几何图片开始，独立完成全部形式化过程。
更准确地说：
89.29% 主要衡量的是在正确形式化表示已经给定的情况下，系统进行定理规划和符号搜索的能力。
因此：
Training-free 不等于没有成本，也不等于端到端系统已经完全解决。
这里的"非参数"也不是指整个系统没有参数模型。
| 系统仍然依赖 | 是否存在 |
|---|---|
| 预训练 LLM | 是 |
| 多模态 Embedding 模型 | 是 |
| 历史证明数据库 | 是 |
| 针对定理预测的额外梯度训练 | 否 |
所谓 non-parametric，主要是指：
定理预测策略没有被重新训练进模型权重，而是以外部检索图和结构先验的形式在推理时提供。
11. 论文明确承认了哪些局限？
| 局限 | 具体表现 |
|---|---|
| 推理效率较低 | 多步规划需要反复调用 LLM |
| 极长链任务仍然困难 | L6 上准确率明显下降 |
| TPG 偏局部 | 主要编码局部 precedence，而非完整全局深度 |
| 单步错误影响大 | 某一步失败可能破坏后续整个证明链 |
| 仍依赖基础模型能力 | 更强 backbone 通常带来更高绝对性能 |
这些局限说明：
Pri-TPG 很好地缓解了局部无结构搜索，但没有彻底解决全局长程一致性。
12. 我的进一步判断
下面这些问题并非论文全部明确提出，而是基于其方法设计和实验结果进一步延伸出的判断。
1. TPG 是逻辑依赖图，还是经验顺序图？
论文将边 (u \rightarrow v) 描述为定理之间的前置依赖。
但图主要从历史解题轨迹中构建。
| 严格逻辑依赖 | 历史经验顺序 |
|---|---|
| A 是 B 的必要前提 | A 经常在 B 之前出现 |
| 具有较强因果含义 | 可能只是数据偏好 |
| 跨数据集更稳定 | 可能受证明风格影响 |
| 可以形式化验证 | 可能只是统计共现 |
历史轨迹中 A 在 B 前面出现，不一定意味着 A 是 B 的严格必要条件。
也可能只是：
- 这是数据集中常见的证明习惯；
- 训练集更偏好某条证明路线；
- 还存在其他合法顺序；
- 两条定理只是高频共现。
因此，一个值得继续验证的问题是：
TPG 学到的究竟是因果依赖，还是高频路径模板？
2. 局部结构一致，不等于全局证明一致
Pri-TPG 主要根据上一步定理的后继节点进行结构定位。
| 局部优势 | 潜在问题 |
|---|---|
| 保持连续步骤连贯 | 可能限制跨分支跳转 |
| 减少无效后继 | 可能错过替代证明路线 |
| 降低短程搜索难度 | 不保证最终可达目标 |
| 利用历史局部规律 | 可能难以处理回溯 |
局部合理的连续步骤，不一定最终通向目标。
这也是 L6 等极长链任务仍然困难的重要原因之一。
3. 失败会影响排序，但不会真正更新图
Pri-TPG 会对重复和失败定理施加 history penalty。
但这种机制主要是在当前推理过程中调整候选排序。
| 当前机制 | 更进一步的结构学习 |
|---|---|
| 对失败定理降权 | 定位导致失败的节点或边 |
| 避免重复尝试 | 更新图结构本身 |
| 当前任务内生效 | 可以跨任务积累经验 |
| 局部排序调整 | 全局信用分配 |
它还没有真正做到：
根据一次失败，反向定位图中哪一个节点或哪一条边有问题，并更新整体结构。
4. 高召回率与推理成本之间仍有矛盾
实验显示，K 越大，准确率越高，尤其是在中高难度任务中。
| 更大的 K | 更小的 K |
|---|---|
| 关键定理更不容易遗漏 | 检索成本更低 |
| 候选覆盖率更高 | 候选集合更紧凑 |
| 长链任务更有保障 | 更容易漏掉关键定理 |
| 后续排序压力更大 | 对检索质量要求更高 |
如何在：
- 更小检索规模；
- 更低调用成本；
- 更高关键定理召回率
之间取得平衡，仍然是一个工程与研究问题。
13. 从 Pri-TPG 到 Dynamic Self-Evolving TPG
Pri-TPG 当前解决的是：
如何从历史成功轨迹中提取局部结构先验，帮助 LLM 缩小搜索空间。
但它还没有充分解决：
推理失败之后，如何定位错误，并更新整张图的全局结构？
一个自然的后续方向是：
Dynamic Self-Evolving TPG
即：
利用成功与失败轨迹，让定理优先图在推理过程中持续更新。
Pri-TPG 与 Dynamic TPG 的区别
| 维度 | Pri-TPG | Dynamic Self-Evolving TPG |
|---|---|---|
| 主要数据来源 | 历史成功轨迹 | 成功轨迹 + 失败轨迹 |
| 图的状态 | 推理时构建，但结构主要来自历史 | 在当前推理中持续更新 |
| 失败处理 | 对失败动作降权 | 对节点、边和子路径进行信用分配 |
| 搜索方式 | 局部结构引导 | 局部引导 + 全局回溯 |
| 学习目标 | 避免无结构探索 | 学会修正错误结构 |
| 全局一致性 | 有限 | 作为核心优化目标 |
一个可能的流程是：
LLM 按照当前 TPG 推理
↓
符号执行器发现路径失败或目标不可达
↓
定位最早导致后续不可完成的节点或边
↓
对相关局部结构进行反向信用分配
↓
降低错误边权重，提升替代路径权重
↓
更新 TPG
↓
重新规划对应的研究问题可以写成：
Can an LLM agent use failed reasoning trajectories to perform backward credit assignment over a theorem precedence graph, thereby improving global consistency in long-horizon theorem proving?
中文表达为：
能否利用失败推理轨迹，对定理优先图进行反向信用分配，从而提升长程定理证明中的全局一致性？
进一步可以探索：
| 方向 | 可能作用 |
|---|---|
| 基于树搜索的全局回溯 | 在失败后切换到替代分支 |
| 图上的价值传播 | 把最终结果反向传播到节点和边 |
| 节点级信用分配 | 判断哪个定理选择产生关键影响 |
| 边级信用分配 | 判断哪种定理转移不可靠 |
| 成败轨迹联合建模 | 同时学习应该做什么和不应该做什么 |
| 不确定性驱动扩展 | 在高不确定位置扩大搜索 |
| 层级图或超图 | 表达更复杂的多定理依赖关系 |
真正的下一步，也许不是构建更大的静态推理图，而是让图能够从失败中自我修正。
14. 总结：从内容增强走向结构增强
Pri-TPG 表面上是一篇几何定理预测论文。
但它真正传递的思想是：
LLM 推理失败，有时并不是因为模型不知道答案，而是因为它面对的行动空间过大，缺少稳定的结构导航。
这篇论文通过三层机制解决这个问题：
| 模块 | 解决的问题 |
|---|---|
| RAG | 找到与当前题目相关的定理 |
| TPG | 组织这些定理之间的先后关系 |
| Symbolic Feedback | 在每一步执行后验证、更新并重新规划 |
它把 LLM 从一个自由生成器，变成了一个受结构约束的高层规划器。
其核心转变可以概括为：
| 过去 | Pri-TPG 所代表的方向 |
|---|---|
| 检索知识 | 检索结构 |
| 一次生成 | 闭环执行 |
| 无约束推理 | 结构化搜索 |
| 只利用成功示例 | 未来进一步利用成败反馈 |
| 模型内部记忆策略 | 外部可解释结构先验 |
当然，Pri-TPG 仍然主要解决局部定理顺序问题。
在极长证明中，它依然面临：
| 仍未解决的问题 | 表现 |
|---|---|
| 全局一致性不足 | L6 性能明显下降 |
| 回溯能力有限 | 主要依赖局部后继 |
| 失败信息利用不充分 | 只降权，不更新图 |
| 推理成本较高 | 多次 LLM 调用和大规模检索 |
但这恰恰说明，这篇论文不是研究终点，而是一个很好的起点。
未来的长程 Agent，可能不仅需要更强的模型、更大的上下文和更多工具，还需要一种能够：
从历史中提取结构，在执行中验证结构，并从失败中更新结构的自进化推理系统。
而这，可能才是 Pri-TPG 留给 Agent 研究最值得继续追问的问题。
版权所有
版权归属：