Rewarding Novel Deductions: Solver-guided Process Supervision for Logical Reasoning¶

会议: NeurIPS 2026
arXiv: 2609.34660
论文: https://arxiv.org/abs/2609.34660
领域: Reasoning
关键词: 逻辑推理、过程监督、SMT求解器、强化学习、新颖性奖励

一句话总结¶

本文提出基于 SMT 求解器过程监督的强化学习框架 Spring，通过验证中间推理步的形式化有效性、状态一致性与非冗余新颖性来发放密集过程奖励并惩罚矛盾，在 ZebraLogic、AR-LSAT 与 Knights and Knaves 上显著超越纯结果奖励和符号基线。

研究背景与动机¶

大语言模型（LLM）在各类推理任务中取得了长足进展，但在需要严格约束跟踪、全局一致性保持和长程多步演绎的结构化逻辑推理问题上仍面临严峻挑战。这类任务不同于开放式文本生成，不仅要求最终答案完全正确，而且要求中间推理链条中的每一步演绎都保持逻辑完备、语义自洽且层层递进。然而，当前模型（尤其是参数量在 4B 及以下的小型 LLM）极易生成表面连贯但充满自相矛盾、重述前提或循环空转的推理轨迹，导致长链条演绎频繁崩溃。

针对这一困境，现有神经符号方法（如 SatLM、Logic-LM、LINC 等）主要将 LLM 视作语义解析器，在模型将自然语言完整形式化为求解器规范后，完全交由 SAT/SMT 或一阶逻辑定理证明器进行末端求解或后验验证。此类范式受制于初始形式化质量的脆弱瓶颈，未能深入干预模型内部逐步生成推理步骤的认知过程。与此同时，主流强化学习方法大多仅针对最终答案的对错提供稀疏的结果奖励（Outcome-only Reward），对具有逻辑缺陷或侥幸猜对答案的推理过程缺乏辨别力，这在逻辑推理场景下显得过于粗粒度。

解决该问题的核心在于如何为模型的多步演绎轨迹提供细粒度、低延迟且数学严谨的过程级逻辑反馈。本文的切入角度是：不再仅仅将求解器当作下游黑盒推理引擎，而是将其提升为强化学习训练期的过程监督裁判，实时评估每一步演绎的信息增益与完备性。核心 idea：利用 SMT 求解器在训练期动态验证中间推理步，形式化定义不被既有状态蕴含的「新颖推理步」与破坏可满足性的「矛盾步」，据此构建兼顾推理有效性、新颖信息增益与全局解相容性的过程奖励，指导模型生成短紧凑、高自洽的逻辑推理链条。

方法详解¶

整体框架¶

Spring 框架将逻辑推理任务形式化为过程监督的强化学习优化问题，模型接收自然语言前提与全局领域约束，自回归生成解析后的语法前提、交错式推理轨迹（自然语言解释与可执行形式化逻辑命题交替出现）以及最终解答。训练期，系统首先将模型解析的语法前提注入 Z3 求解器构建基础状态空间；若初始理论可满足且存在唯一解，求解器便沿推理时间步动态追踪已接受的非矛盾命题集合，逐一判定各步演绎是有效演绎、重言式、新颖步还是矛盾步；最后将上述符号判定与格式、解析率和最终准确率组合为标量奖励，在群体相对策略优化（GRPO）下驱动策略演进。

整体框架的协同计算与验证数据流如下图所示：

%%{init: {'flowchart': {'rankSpacing': 24, 'nodeSpacing': 28, 'padding': 6, 'wrappingWidth': 400}}}%%
flowchart TD
    A["输入逻辑问题<br/>自然语言线索与领域公理"] --> B["生成结构化推理输出<br/>解析语法前提 + 交错推理链 + 最终解答"]
    B --> C["基础求解器状态构建<br/>验证初始基底理论可满足性与唯一解"]
    C -->|可满足 SAT| D["逐逻辑步符号验证<br/>识别有效性/新颖步/矛盾步/重言式"]
    C -->|不可满足 UNSAT| E["低阶保底惩罚结算<br/>仅计算格式与解析基础奖励"]
    D --> F["过程级密集奖励塑形<br/>新颖步加权 + 解一致性奖励 - 矛盾惩罚"]
    E --> G["群体相对策略优化 (GRPO)<br/>组内优势归一化与策略截断更新"]
    F --> G

关键设计¶

1. 基础求解器状态构建：确保问题语义规范可满足且具备唯一解 针对模型在将自然语言线索转化为形式化逻辑时容易引入格式破损或前提冲突的问题，Spring 在进入逐步验证前首先执行基础求解器状态构建。设输入包含自然语言线索集合 $\mathcal{C}$ 和全局结构规则 $\Gamma_{\mathrm{dom}}$（例如变量取值范围、唯一性与互斥性约束）。策略网络 $\pi_\theta$ 首先生成解析后的语法前提 $\hat{\mathcal{C}}=(\hat{C}_1, \ldots, \hat{C}_m)$，求解器构建基底理论： $$ \Gamma_{\mathrm{base}} = \Gamma_{\mathrm{dom}} \cup \hat{\mathcal{C}} $$ 系统调用 Z3 求解器严格核验 $\Gamma_{\mathrm{base}}$ 的可满足性及其是否具有唯一解。这一门控机制设定了满足性指示标量 $s_{\mathrm{sat}} \in \{0, 1\}$：若解析出的前提系统本身即产生不可满足（UNSAT）或存在多解语义漂移，则立即判定为不可兼容轨迹，切断后续细粒度过程奖励，仅保留基础格式与解析分值。这保证了后续步级逻辑判断始终在一个语义自洽、良定义的真实命题空间中进行。

2. 逐逻辑步符号验证：形式化判别推理步的有效性、新颖性与矛盾性 在基底状态完备的条件下，求解器对轨迹中提取的形式化推理步 $z_t$ 进行细粒度逻辑分类。记 $\mathcal{P}_{t-1}^{\mathrm{nc}}$ 为截至 $t-1$ 步已接受的非矛盾形式化推理步集合，当前累计推理上下文为 $\Gamma_{\mathrm{ctx}}^{(t)} = \Gamma_{\mathrm{base}} \cup \mathcal{P}_{t-1}^{\mathrm{nc}}$。求解器逐一核定四大逻辑性质： - 有效步（Valid Step）：$z_t$ 必须被基底理论严格逻辑蕴含，即 $\Gamma_{\mathrm{base}} \cup \{z_t\}$ 可满足且 $\Gamma_{\mathrm{base}} \cup \{\neg z_t\}$ 不可满足。 - 重言式（Tautological Step）：若仅由领域结构公理即可导出 $z_t$（即 $\Gamma_{\mathrm{dom}} \cup \{\neg z_t\}$ 不可满足），说明该步未利用任何问题特异线索，判定为无实质推理推进的空转步并予以剔除。 - 新颖步（Novel Step）：一个有效且非重言式的命题 $z_t$，若既不能被历史推理状态蕴含（令 $P_{t-1} = \bigwedge_{z \in \mathcal{P}_{t-1}^{\mathrm{nc}}} z$，满足 $P_{t-1} \not\Rightarrow_{\Gamma_{\mathrm{dom}}} z_t$），且不与任何原始前提 $C_i \in \mathcal{C}$ 等价，则被裁决为新颖步。在约束求解视角下，这意味着 $\Gamma_{\mathrm{dom}} \cup \mathcal{P}_{t-1}^{\mathrm{nc}} \cup \{z_t\}$ 与 $\Gamma_{\mathrm{dom}} \cup \mathcal{P}_{t-1}^{\mathrm{nc}} \cup \{\neg z_t\}$ 均保持可满足，表明该步真实缩减了可行解空间。 - 矛盾步（Contradictory Step）：若 $\Gamma_{\mathrm{ctx}}^{(t)} \cup \{z_t\}$ 导致求解器不可满足，则判定 $z_t$ 与已有前提或历史推断发生逻辑冲突。

3. 过程级密集奖励塑形：正向激励信息增益与终解相容性，强力惩罚逻辑冲突 传统的稀疏奖励无法引导模型探索高效的演绎路径。Spring 设计了融合步级逻辑质量与全局结果的分段奖励函数。定义新颖步信号 $r_{\mathrm{novel}}$、矛盾步发生频次惩罚 $r_{\mathrm{contra}}$、以及推理步集合 $\mathcal{Z}$ 与最终解答 $F$ 的联合相容性奖励 $r_{\mathrm{consistency}}$（要求 $\Gamma_{\mathrm{dom}} \cup \mathcal{Z} \cup \{F\}$ 保持可满足）。结合格式规范奖励 $r_{\mathrm{format}}$、语法解析成功奖励 $r_{\mathrm{parsed}}$ 和终局准确率 $r_{\mathrm{accuracy}}$，总奖励形式为： $$ R = \begin{cases} 0.15 \, r_{\mathrm{parsed}} + 0.10 \, r_{\mathrm{format}} + 0.60 \, r_{\mathrm{accuracy}}, & s_{\mathrm{sat}} = 0 \[6pt] r_{\mathrm{base}} + \bigl(0.5 + 0.5 \, r_{\mathrm{accuracy}}\bigr) \, r_{\mathrm{proc}}, & s_{\mathrm{sat}} = 1 \end{cases} $$ 其中基础项与过程项分别定义为： $$ r_{\mathrm{base}} = 0.15 \, r_{\mathrm{parsed}} + 0.10 \, r_{\mathrm{format}} + 0.60 \, r_{\mathrm{accuracy}} $$ $$ r_{\mathrm{proc}} = 0.40 \, r_{\mathrm{novel}} + 0.30 \, r_{\mathrm{consistency}} - 0.15 \, r_{\mathrm{contra}} $$ 该设计确保在保持主任务目标正确性的前提下，对产出高密度新颖演绎、推理链条与终解高度自洽的轨迹给予额外加权，同时对产生逻辑自闭与矛盾发散的轨迹施加严厉扣分。

一个完整示例¶

以 ZebraLogic 逻辑谜题为例（3间房屋、3名住户 Alice/Bob/Carol、3种宠物 Cat/Dog/Fish、3种饮品 Tea/Coffee/Juice）： 1. 前提解析与基底建立：模型解析线索“Alice 住在猫主人的紧邻左侧”、“Bob 住在喝茶的房子”、“2号房喝茶”等为 Z3 约束。Z3 校验 $\Gamma_{\mathrm{base}}$ 满足且唯一，触发 $s_{\mathrm{sat}} = 1$。 2. 第一步演绎（有效且新颖）：模型生成“由线索2和3可知，Bob 必住在 2 号房”。求解器判定该命题受理论蕴含且此前未知，判定为 Novel Step，记入 $r_{\mathrm{novel}}$ 累加，并将 House2 = Bob 并入已接受集合 $\mathcal{P}_1^{\mathrm{nc}}$。 3. 第二步演绎（有效且新颖）：模型生成“由线索1知 Alice 在猫主人左侧，故 Alice 不能在 3 号房”。求解器确认合法且未被蕴含，再次判定为 Novel Step，状态更新。 4. 劣质演绎判定对比：若模型此时生成重言式“2号房不能同时是 1 号房”，求解器根据领域公理判定为 Tautological Step，不计入新颖奖励；若模型在此处冒进猜想“Bob 喝咖啡”，求解器立即检测到其与“2号房喝茶且 Bob 在 2 号房”矛盾，判定为 Contradictory Step，触发 $r_{\mathrm{contra}}$ 惩罚扣分并拒绝并入历史集合。 5. 终解自洽交付：模型顺畅推导出完整排布表格，求解器复核全轨迹命题与答案联合可满足，授予满格 $r_{\mathrm{consistency}}$ 与 $r_{\mathrm{accuracy}}$。

损失函数 / 训练策略¶

Spring 采用群体相对策略优化（GRPO）结合分布式 DAPO 运行时架构进行强化学习训练。针对每个输入问题 $x$，策略模型 $\pi_\theta$ 采样一个包含 $G=8$ 条候选输出的样本组 $\{o_i\}_{i=1}^G$，其中每条输出 $o_i = (\tau_i, y_i)$ 经过求解器评测获得标量奖励 $r_i$。在组内计算优势值： $$ A_i = \frac{r_i - \bar{r}}{\sigma_r + \epsilon}, \quad \bar{r} = \frac{1}{G}\sum_{i=1}^G r_i, \quad \sigma_r = \sqrt{\frac{1}{G}\sum_{i=1}^G (r_i - \bar{r})^2} $$ 结合重要性权重比率 $\rho_i(\theta) = \frac{\pi_\theta(o_i \mid x)}{\pi_{\theta_{\mathrm{old}}}(o_i \mid x)}$，采用带截断的替代目标函数并加入相对冻结参考策略 $\pi_{\mathrm{ref}}$ 的 KL 散度正则化约束： $$ \mathcal{L}(\theta) = \mathbb{E}x \left[ \frac{1}{G} \sum(\cdot \mid x)\bigr) $$ 实验中超参数设定 }^G \min\bigl(\rho_i(\theta) A_i, \, \operatorname{clip}(\rho_i(\theta), 1-\delta, 1+\delta) A_i\bigr) \right] - \beta \, \mathrm{KL}\bigl(\pi_\theta(\cdot \mid x) \,|\, \pi_{\mathrm{ref}$\beta = 0.01$，采样温度为 0.8，推理评估温度设为 0.0，最长上下文窗口为 $8 \times 1024$ tokens。在 4 块 NVIDIA H200 GPU 上，Qwen3-4B-Thinking 单轮训练仅需约 45 分钟，早停机制耐心度设为 3 个 epoch。

实验关键数据¶

主实验¶

实验涵盖 ZebraLogic、AR-LSAT（涵盖排序 Ordering、分组 Grouping、匹配 Assignment）以及 Knights and Knaves（KnK）三个具有严格逻辑约束的基准评测集，横跨 Qwen3-1.7B、Qwen3-4B-Thinking、Phi4-Reasoning 和 Qwen3-8B 四种不同体量的大语言模型。主要模型在基准任务上的端到端求解表现如下表所示：

模型	方法	ZebraLogic 谜题准确率 (%)	ZebraLogic 单元格准确率 (%)	AR-LSAT 综合准确率 (%)	KnK 谜题准确率 (%)	KnK 人物准确率 (%)
Qwen3-1.7B	Base-NL	11.14	35.04	13.52	53.28	64.43
	OR-INT (最强仅结果)	36.00	46.09	37.12	73.57	80.54
	Logic-LM	12.85	33.16	15.58	3.57	22.51
	Spring (本文)	54.00	59.87	49.26	85.28	86.94
Qwen3-4B-Thinking	Base-NL	24.00	24.00	8.20	55.28	65.41
	OR-NL	67.28	68.30	33.48	74.28	84.66
	OR-INT	66.14	72.72	68.80	76.57	87.58
	Logic-LM	21.42	38.12	20.78	7.14	35.48
	Spring (本文)	73.71	81.52	73.61	88.71	94.21
Phi4-Reasoning	Base-NL	7.14	22.42	18.12	57.85	68.13
	OR-INT	49.00	53.54	32.07	81.42	88.13
	Logic-LM	20.00	36.75	18.61	9.28	40.12
	Spring (本文)	55.71	59.52	37.52	89.28	94.57
Qwen3-8B	Base-NL	47.42	50.13	33.56	56.00	68.49
	OR-INT	70.85	75.13	68.67	77.14	82.85
	Logic-LM	22.85	40.56	25.97	8.57	55.20
	Spring (本文)	77.85	79.41	75.56	93.14	96.05

消融实验¶

在 ZebraLogic 基准上针对 Qwen3-4B-Thinking 深入剥离新颖性奖励（$--\text{N}$）以及同时剥离新颖性奖励与矛盾惩罚（$--\text{NC}$），从成功推理轨迹（Solved traces）与失败轨迹（Failed traces）双重维度评估过程质量：

实验配置	谜题准确率 (%)	成功用例 SAT 率	成功轨迹步数 (Steps ↓)	成功有效步占比 (Valid/Parsed ↑)	失败轨迹步数 (Steps ↓)	失败用例矛盾率 (Contradictions/100步 ↓)
Spring (完整模型)	73.71	0.965	22.37	0.996	9.39	0.46
w/o 新颖性奖励 ($--\text{N}$)	61.42	0.941	35.20	0.988	49.10	6.77
w/o 新颖性与矛盾惩罚 ($--\text{NC}$)	66.14	0.814	34.82	0.953	11.23	2.52

关键发现¶

新颖步奖励是规避无效冗余与发散的核心驱动：当去除新颖性奖励（$--\text{N}$）后，模型在 ZebraLogic 上的谜题准确率剧烈下跌（Qwen3-1.7B 从 54.00% 暴跌至 19.28%，Qwen3-4B 从 73.71% 下滑至 61.42%）。消融表明，缺少新颖性引导的模型极易在已经证明的前提中反复横跳或陷入等价置换，导致成功用例的平均步数从 22.37 步激增至 35.20 步，失败用例更是失控发散至 49.10 步且矛盾率激增 14.7 倍（从 0.46 飙升至 6.77）。
小型模型受益尤为显著：在参数量仅 1.7B 的 Qwen3 上，Spring 相比原始无微调模型提升了 42.86 个百分点（ZebraLogic），相比纯结果奖励基线 OR-NL 依然大幅领先 15.43 个百分点，表明对小模型而言，严密的符号过程约束能弥补注意力长程漂移的固有缺陷。
符号推理的复杂度可扩展性瓶颈：随着 ZebraLogic 谜题规模从 Small（$2\times2$ 到 $4\times2$）扩展至 X-Large（$5\times5$ 到 $6\times6$），准确率从 91.5% 骤降至 20.4%，但 X-Large 下的 SAT 率（64.1%）依然显著高于谜题全对准确率。错误分析表明，84 例失败属于输出内部自洽但属性重复分配的“求解器自洽型非精确解”，说明超大规模组合空间下的搜索截断仍是严峻瓶颈。

亮点与洞察¶

将 SMT 求解器从推理后端转向训练期裁判：打破了以往神经符号工作将求解器仅仅作为最终解答执行器（容易因解析单点故障而全盘皆输）的惯性，利用 Z3 的逻辑蕴含和可满足性判定直接构建强化学习过程监督奖励，实现了符号精度对神经网络生成倾向的隐式内化。
数学化度量「新颖推理」消除奖励黑客：传统过程奖励模型（PRM）容易被人为冗余但看似合法的步骤所欺骗，Spring 通过严格的谓词逻辑判定定义新颖步（不被历史非矛盾前提集合蕴含且非重言式），从根本上遏制了模型通过反复生成已知公理刷取过程分数的作弊行为。
失败轨迹的极简截断效应：完整 Spring 训练出的模型在无法解决的难题上平均仅消耗 9.39 步即收敛或停止，而缺少新颖性与矛盾监督的模型会盲目生成长达 49 步的冗长幻觉，表明求解器过程奖励赋予了模型高度自律的逻辑边界感知。

局限与展望¶

依赖结构化符号表示的前置转化：当前框架的前提是自然语言问题能够可靠解析为可被 Z3 表达的命题逻辑或一阶理论，对于常识推理、情感分析等非形式化、难以公理化的开放域任务难以直接套用。
初始解析瓶颈依然存在：如果策略网络生成的第一阶段语法前提 $\hat{\mathcal{C}}$ 存在严重语法错误或产生不可满足的冲突约束，求解器基底状态将直接判定为失效（$s_{\mathrm{sat}}=0$），导致过程监督退化为粗粒度的解析保底奖励。
复杂组合空间下的收敛挑战：在超大规模变量和长跨度约束谜题（如 $6\times6$ ZebraLogic）中，模型容易收敛到局部满足局部约束但全局属性存在重复指派的局部极值点，未来可考虑将局部反例引导的抽象精化（CEGAR）机制融合进强化学习采样过程中。

评分¶

新颖性: ⭐⭐⭐⭐⭐ 首次提出利用 SMT 求解器定义并奖励新颖推理步的过程监督 RL 范式。
实验充分度: ⭐⭐⭐⭐⭐ 涵盖 3 大基准、4 类主流开源模型，轨迹长度、SAT 率与矛盾率等分析极为透彻。
写作质量: ⭐⭐⭐⭐⭐ 形式化数学定义极其严密自洽，图表与分析切中痛点。
价值: ⭐⭐⭐⭐⭐ 为解决推理大模型中的虚假逻辑空转与矛盾冗余提供了扎实可复现的神经符号训练范式。