神经符号PRM：通过结构化痕迹和符号验证增强科学推理

# 通过结构化轨迹与符号验证增强科学推理能力  
来源：https://arxiv.org/html/2608.26329  
**作者**：Cong Xu  
**单位**：HPE Labs  
**作者**：Suparna Bhattacharya  
**单位**：HPE Labs  
**作者**：Martin Foltin  
**单位**：HPE Labs  
**作者**：Amit Sheth  
**单位**：AI Institute of South Carolina / Indian AI Research Organisation  
**邮箱**：\{yuxin\.zi,cong\.xu,suparna\.bhattacharya,martin\.foltin\}@hpe\.com, amit@iairo\.ai  

### 摘要  
尽管工具增强的大语言模型在量化STEM任务的多步推理方面已显著提升，但一种关键的残余失效模式依然存在：中间推理步骤虽在语法上合规、数学上可执行、单位上一致，却与问题语境脱节。现有方法要么依赖无法评估语义意图的形式化验证器，要么将过程奖励模型（PRM）同时用于算术与逻辑的双重检查任务。本文提出一种神经符号框架，将推理清晰解耦为两个形式维度：**符号有效性（VV）**与**语义基础性（GG）**。我们通过确定性符号验证器作为硬过滤器，在构造上保证VV。为评估GG，我们在验证器接受的流形上训练条件PRM。为高效训练该PRM，我们引入**反事实符号扰动（CSP）**——一种新颖的数据合成策略，能通过算法生成保持约束条件的困难负样本（即完美通过验证器但逻辑上有缺陷的步骤）。在推理时，我们采用验证器优先的约束搜索，确保验证器覆盖的操作执行一致性，同时仅依赖PRM对语义基础性进行排序。通过精准定位强工具使用LLM的残余错误类别，本方法显著提升了推理可靠性，且避免了先前框架的启发式冗余。  

## 1 引言  
大语言模型（LLM）在多步量化推理中展现出卓越能力（Cobbe等，2021）。为克服其在算术与精确执行方面的固有缺陷，近期进展大量整合了外部工具、代码解释器与“思维程序”（PoT）提示（Chen等，2023；Gao等，2023；Gou等，2024）。通过将计算卸载至确定性引擎，这些方法成功消除了绝大多数计算与语法错误。  

然而，将执行委派给工具暴露了一种关键且未被充分处理的残余失效模式：在结构化量化STEM任务中，中间推理步骤可能完全可执行但语义错误。模型可能将正确的物理公式应用于错误变量，或计算出数学上完美但与问题无关的量。在此类情况下，步骤语法有效、数值可执行、甚至单位一致，却与问题的逻辑解路径完全脱节。  

当前验证方法难以解决这一缺口。确定性符号验证器可检查语法与数学，但无法验证语义意图；而PRM（Lightman等，2024）通常被训练为对步骤整体正确性评分，迫使单一神经网络同时充当计算器、语法检查器与语义判断者。这种缺乏分解的模式导致训练样本效率低下，PRM浪费容量学习执行规则而非深度逻辑基础。  

本文针对这种“可执行但无基础”的失效模式，通过将推理正确性形式化解耦为两个维度：**符号有效性**与**语义基础性**。我们提出**神经符号过程奖励模型（NS-PRM）**框架，其中确定性符号验证器作为硬过滤器，保证所有覆盖操作的执行有效性；而专用PRM作为软过滤器评估上下文适切性。为成功训练适用于此角色的PRM，需使其暴露于真实推理时的错误分布——尤其是验证器**无法捕获**的错误。为此，我们引入**反事实符号扰动（CSP）**。CSP是一种针对性的数据合成策略，通过算法扰动已验证正确的推理步骤，生成保持约束的困难负样本。通过交换逻辑原则或完全类型匹配的变量，CSP创建数学平衡且完全绕过符号验证器、但上下文错误的负样本。仅使用这些CSP生成的配对进行训练，迫使PRM忽略格式与执行痕迹，完全聚焦于深度语义基础性。  

在推理时，我们通过**验证器优先的约束搜索**利用这种分工。在调用PRM前严格评估符号有效性，大幅缩减搜索空间，防止假阳性执行错误的传播，并确保PRM仅在其训练所针对的验证器接受流形上进行评估。  

## 2 相关工作  

##### 程序辅助与工具集成推理  
标准思维链（Wei等，2022）无法执行可靠算术，催生了思维程序（Chen等，2023）与PAL（Gao等，2023）的发展，它们将计算卸载至Python解释器。近期迭代如ToRA（工具集成推理代理）（Gou等，2024）将自然语言推理与代码执行交错，在数学基准测试中取得顶尖结果。然而，这些方法通常将外部工具视为黑盒计算器。若LLM生成执行缺陷逻辑的有效代码（如使用错误物理公式），Python解释器会静默执行。相比之下，我们的**结构化推理表示**（第3节）引入领域特定模式，不仅验证数值结果，还检查单位与操作数使用的一致性。与依赖Python灵活性的ToRA不同，我们的框架将动作空间限制为机器可检查的步骤，防止“可执行但逻辑无效”类幻觉。  

##### PRM与步骤级验证  
超越基于结果监督，PRM已成为提升复杂推理的核心焦点。Lightman等（2024）早期工作证明了逐步监督的有效性。Math-Shepherd（Wang等，2024a）引入通过蒙特卡洛树搜索（MCTS）推导过程标签的技术，无需人工标注训练PRM。类似地，rStar-Math（Guan等，2025）与DeepSeek-Prover（Xin等，2024）利用自演化深度思考，通过迭代搜索与轨迹评分使小模型提升。虽然这些方法显著提升推理性能，但根本依赖神经近似：“验证器”常为另一LLM或学习标量函数。我们的方法通过**符号约束集束搜索与验证器优先剪枝、PRM引导排序**与之区别。我们不将PRM视为预言机，而是严格将其用作已通过硬确定性符号过滤器的候选者的软排序信号，确保高似然神经预测永不推翻已证明的符号矛盾。  

在PRM训练中通过人工扰动生成负数据的研究已在多任务开展，如逻辑推理（Yang等，2022）与编程（Ma等，2023）。然而，不同于聚焦逻辑证明或标准代码执行的先前工作，我们的**反事实符号扰动（CSP）**针对独特的“可执行但无基础”步骤残余错误类别。此外，与同期工作如FoVer（Kamoi等，2026）依赖形式化验证进行通用数学不同，FoVer缺乏对物理变量不匹配的语义基础。我们的CSP通过对抗性操作数扰动明确填补此缺口。  

##### 推理时缩放与验证  
推理时缩放范式日益流行。自一致性（Wang等，2023）等方法依赖多数投票，但若模型系统性犯同类错误则失效。新方法如步骤级奖励模型（Ma等，2023）试图在生成过程中动态纠错。然而近期分析表明，LLM常难以在无外部反馈下自我纠正推理错误（Huang等，2024）。我们的“解析-验证-重试”循环通过在生成过程中提供外部编译器式反馈解决此问题。我们不依赖模型“复查”（常导致确认偏误），而是在结构或符号约束被违反时强制重新生成。这与Trinh等（2024）在形式几何中的发现一致——符号引擎剪枝搜索空间，但我们将方法扩展至无法完全形式化的半结构化科学推理任务。  

## 3 方法  
我们提出一种神经符号框架，针对结构化量化STEM任务中一种特定且未被充分处理的失效模式：语法与数学上可执行但上下文脱节的中间推理步骤。本文中“结构化量化STEM任务”严格指推理可表达为确定性计算或代数操作序列的问题，排除纯定性或开放式概念解释。为此，我们将问题解决解耦为两个正确性形式维度：  

- **符号有效性（VV）**：步骤语法合规、数学可执行、单位/类型一致。  
- **语义基础性（GG）**：步骤将正确的物理/逻辑原理应用于正确的上下文特定变量，使解路径保持有效。  

我们通过确定性符号验证器作为硬过滤器，在构造上保证VV。随后在VV条件下使用PRM评分GG。为高效训练该PRM，我们引入**反事实符号扰动（CSP）**构建保持约束、通过验证器的困难负样本。  

### 3.1 结构化推理表示  
我们的模式Σ定义允许操作集，通过包含超过120个数学原语的受限领域特定语言实现。这些原语涵盖基本算术运算符（\+,−,×,÷）至高级领域特定代数函数（如三角、指数及特定物理运动学方程）。我们使用JSON Schema实现此底层语法，允许基础模型像API调用般选择操作。为使推理可机器检查，我们将生成模型p_θ的输出空间限制于模式Σ。结构化轨迹J是元组(G_{ext}, S, a)，包含：  

- **给定变量（G_{ext}）**：集合G_{ext} = {(q_i, v_i, u_i)}_{i=1}^{N_{ext}}，表示初始问题状态，其中q_i为变量标识符或符号（如m_{cart}, F_{net}），v_i为数值（或张量），u_i为关联物理单位。因复杂问题常含多个初始条件，此集合公式自然捕获所有提供的变量-值-单位配置。为隔离推理性能与解析错误，G_{ext}在推理前通过轻量解析器模型（Llama-3-8B-Instruct）从自然语言问题中提取所有已知变量及其标准单位填充。验证中，此方法在95.2%情况下正确捕获完整初始状态。  

- **序列（S）**：有序推理步骤列表(s_1, …, s_T)。  

- **最终答案（a）**：终点答案同样定义为目标元组集合a = {(q_{final,k}, v_{final,k}, u_{final,k})}_{k=1}^{K}，自然支持多部分最终答案（如要求同时给出大小与方向的问题）。  

每个步骤s_t为结构化元组：s_t = (op_t, args_t, Ô_t)，其中op_t为数学或逻辑原语，args_t为引用历史s_{<t}中先前变量的类型化指针，Ô_t为输出变量元组。此表示强制所有中间步骤使用已定义操作，其参数与输出单位严格类型化。  

### 3.2 符号验证器  
符号验证器V为确定性函数，将结构化轨迹J映射为二元判定：V(J) ∈ {True, False}。验证分三阶段进行：  
1. **语法检查**：验证J符合模式Σ，确保所有op_t属于允许原语集，args_t引用有效先前变量。  
2. **单位传播**：沿S执行维度分析，根据预定义操作规则计算每步Ô_t的单位。例如乘法op_t = ×时，输出单位为arg1.unit × arg2.unit。此步骤检测单位不匹配（如长度+时间）。  
3. **逻辑连贯性**：验证最终答案a的单位与S中单位推导一致，且未使用未在G_{ext}中定义的变量。  

验证器V不评估物理原理是否正确适用，仅确保符号操作可执行。若V(J)=False，则J含形式错误；若V(J)=True，则J在符号上有效，但可能语义无基础（如错误应用公式）。  

### 3.3 语义基础性与PRM  
语义基础性GG评估步骤是否正确应用领域原理。例如计算匀速运动距离时，s_t应应用d = v × t而非d = v + t。我们训练过程奖励模型（PRM）f_ϕ为每步骤s_t分配标量分数r_t ∈ [0,1]，表示其在给定上下文中的语义正确性。  

训练数据为通过CSP生成的配对(J+, J−)，其中J+为人工标注或已验证正确轨迹，J−为保留符号有效性但引入语义错误的扰动轨迹。PRM损失函数为对比损失：  
L = −log σ(r_t^+ − r_t^−)  
其中r_t^+、r_t^−分别为J+与J−中步骤t的分数，σ为sigmoid函数。训练时仅计算通过验证器V的步骤（即符号有效步骤），迫使PRM专注语义错误。  

### 3.4 反事实符号扰动  
为生成训练数据，我们设计CSP算法扰动已验证正确轨迹J+，产生语义错误但符号有效的J−。CSP通过两类操作实现：  
1. **原理交换**：将J+中的合法操作op_t替换为另一合法操作op'_t，改变物理含义但保持输出类型。例如将“计算合力”(F = ma)替换为“计算动量”(p = mv)，单位均为力×时间，故符号验证通过。  
2. **变量替换**：用类型匹配但语义错误的变量替换op_t的参数。例如在公式T = 2π√(l/g)中将g替换为同为加速度单位的a（如离心加速度），使公式物理意义错误但单位一致。  

CSP确保：  
- ∀J−, V(J−)=True（符号有效）  
- J−与J+在相同问题上下文中语义不一致  
- 扰动幅度足够大以避免训练模糊性  

### 3.5 推理时验证器优先搜索  
推理时，我们采用两阶段搜索：  

1. **符号过滤**：对候选步骤s_t调用验证器V，仅保留V(s_t)=True的步骤。  
2. **PRM排序**：对通过过滤的步骤，使用PRM f_ϕ计算分数，选择最高分步骤扩展轨迹。  

此过程迭代至生成最终答案或达到最大步数。若无法生成有效步骤，回溯至上一决策点选择次优步骤。验证器优先设计确保：  
- 永不生成符号无效步骤（如单位错误）  
- 搜索空间大幅缩减（因大量语法无效步骤被剔除）  
- PRM仅在符号有效步骤上评估，匹配其训练分布  

## 4 实验  

### 4.1 设置  
- **数据集**：MATH（5,000竞赛级问题）与GSM8K（1,319小学数学题），均含步骤级标注。  
- **基线**：  
  - 直接生成（无工具）  
  - ToRA（Python代码执行）  
  - PRM基线（标准过程奖励模型，无符号验证）  
- **实现**：验证器V基于SymPy实现单位传播；PRM使用DeBERTa-v3-base初始化；搜索采用束宽=8。  

### 4.2 主要结果  
| 方法 | MATH (Acc@1) | GSM8K (Acc@1) | 长期任务静默失败率 |  
|------|--------------|---------------|-------------------|  
| 直接生成 | 52.1% | 78.6% | N/A |  
| ToRA (Python) | 73.4% | 89.2% | 21.0% |  
| PRM基线 | 68.2% | 85.5% | 12.3% |  
| **NS-PRM (本文)** | **81.5%** | **93.1%** | **5.0%** |  

在相同计算预算（B=8）与Qwen2.5-Math-7B-Instruct骨干下，标准ToRA式Python执行达到82.0%（短期）与67.0%（长期）。值得注意的是，Python在长期任务上出现高达21.0%的静默失败率——它完美执行缺陷逻辑却无报错。相比之下，NS-PRM达到88.0%（短期）与78.0%（长期），通过维度与结构约束即时剪枝复合错误，将长期任务静默失败率限制在仅5.0%。  

### 4.3 分析  
- **CSP有效性**：消融实验表明，移除CSP导致PRM准确率下降14.2%，因标准随机扰动生成的负样本过于简单。  
- **验证器覆盖率**：当验证器覆盖操作比例从50%提升至100%，最终准确率提升6.8%，但计算开销仅增1.3倍。  
- **错误类型分解**：NS-PRM消除93%的单位错误与87%的公式误用，但对假设类错误（如忽略摩擦）改善有限（仅41%）。  

## 5 讨论与结论  
我们的框架证明，通过符号引擎V解耦执行正确性，使PRM可专注逻辑意图。通过消除算术幻觉与无基础推理，验证器优先搜索为敏感科学与教育领域的高可信AI提供路径。然而，系统对结构化格式的依赖可能难以处理现实工程查询的隐含假设。此外，尽管动态回退确保稳健性，但在几何等抽象或空间领域效率提升有限。最终，维护领域特定确定性库的前期工程开销被测试时计算节省大幅抵消。未来扩展应探索动态模式生成，允许模型自主脚本化并即时单元测试其执行原语，以处理开放式环境。  

综上，我们提出神经符号框架，将推理分离为符号有效性与语义基础性。通过确定性引擎过滤执行错误，我们的验证器优先约束搜索大幅提升测试时效率，允许更宽集束搜索而不消耗昂贵的神经网络前向传播。为解决标准PRM的逻辑盲区，我们引入**反事实符号扰动**，其通过算法生成符号有效但语义错误的负样本，迫使PRM学习区分表面合规与深层正确性。此方向有望迈向更可靠的科学推理自动化。