Rewarding Novel Deductions: Solver-guided Process Rewards for Logical Reasoning

📄 arXiv: 2609.34660v1 📥 PDF

作者: Muhammad Asif Ali, Wenqing Wang, Huan Wang, Mohammad Raza

分类: cs.CL

发布日期: 2026-09-28

💡 一句话要点

提出SPRING以解决小规模LLM逻辑推理问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 逻辑推理 语言模型 过程奖励 中间推理 SMT求解器 新颖推理步骤 模型训练 推理准确性

📋 核心要点

  1. 现有方法在逻辑推理中主要关注最终答案的正确性，缺乏对中间推理过程的有效监督，导致小规模LLM产生不一致和脆弱的推理轨迹。
  2. SPRING通过引入SMT求解器作为中间推理步骤的验证器，提供过程级监督，鼓励生成新颖且有效的推理步骤。
  3. 在ZebraLogic、AR-LSAT和Knights and Knaves等基准测试中，SPRING在推理准确性上显著优于基线模型，提升幅度可达64.93分。

📝 摘要（中文）

逻辑推理仍然是大型语言模型（LLMs）面临的主要挑战，尤其是在需要精确约束跟踪和多步推理的结构化问题上。现有方法主要优化最终答案的正确性，对中间推理过程的监督较弱。本文提出SPRING（基于求解器的过程奖励用于新颖逻辑推理步骤生成），利用SMT求解器作为中间推理步骤的验证器，提供过程级监督。SPRING引入了新颖推理步骤的概念，设计了过程奖励以鼓励新颖的推理进展，同时惩罚矛盾和无信息的推理步骤。实验结果表明，SPRING在多个逻辑推理基准上表现优异，显著提升了推理准确性。

🔬 方法详解

问题定义：本文旨在解决小规模LLM在逻辑推理中面临的中间推理过程监督不足的问题，现有方法往往只关注最终结果，导致推理过程中的不一致性和冗余性。

核心思路：SPRING的核心思路是利用SMT求解器对中间推理步骤进行验证，提供过程级的奖励机制，鼓励生成新颖且有效的推理步骤，进而提升逻辑推理的整体质量。

技术框架：SPRING的整体架构包括三个主要模块：首先是输入的逻辑问题解析，其次是通过SMT求解器验证中间推理步骤，最后是基于过程奖励更新模型参数，形成闭环反馈。

关键创新：SPRING的主要创新在于引入了新颖推理步骤的概念，定义为在逻辑上有效且与当前推理状态一致的步骤，且未被之前的推理所暗示，这一设计显著提升了推理的有效性。

关键设计：SPRING在损失函数中加入了过程奖励，具体包括对新颖推理步骤的正向奖励和对矛盾推理步骤的惩罚，确保模型在训练过程中能够学习到更有效的推理策略。具体的参数设置和网络结构细节在实验部分进行了详细描述。

🖼️ 关键图片

fig_0
fig_1

📊 实验亮点

SPRING在多个逻辑推理基准上表现出色，在ZebraLogic上相较于基线模型提高了49.71分，在AR-LSAT上提高了64.93分，在Knights and Knaves上达到了93.14的推理准确率，显示出显著的性能提升。

🎯 应用场景

该研究的潜在应用领域包括智能问答系统、自动推理工具和教育辅助软件等。通过提升逻辑推理能力，SPRING可以帮助用户更好地理解复杂问题，提供更准确的推理结果，具有重要的实际价值和广泛的应用前景。

📄 摘要（原文）

Logical reasoning remains a major challenge for large language models (LLMs), particularly on structured problems that require precise constraint tracking, consistency preservation, and multi-step deduction. This challenge is especially acute for small-scale LLMs, which are more prone to producing inconsistent, redundant, or brittle reasoning trajectories. Existing approaches for improving logical reasoning largely optimize for final-answer correctness, providing only weak supervision over the intermediate reasoning process. In this work, we propose SPRING: (Solver-guided Process Rewards for Novel LogIcal ReasoNing Step Generation). SPRING uses SMT solver as a training-time verifier of intermediate reasoning steps to provide process-level supervision. It introduces the notion of a novel reasoning step, namely, a step that is logically valid, consistent with the evolving reasoning state, and not already implied by previously accepted non-contradictory deductions. Based on this solver-based assessment, it designs process rewards that encourage novel inferential progress while penalizing contradictory and uninformative reasoning steps. Evaluation across three logical reasoning benchmarks, ZebraLogic, AR-LSAT, and Knights and Knaves, and four LLMs shows that SPRING consistently outperforms base LLMs, outcome-only reward baselines, and Logic-LM. On ZebraLogic, SPRING improves puzzle accuracy by up to 49.71 and 15.43 points over the base LLM and strongest outcome-only baseline, respectively. On AR-LSAT, it improves overall accuracy by up to 64.93 and 12.14 points, respectively. On Knights and Knaves, SPRING achieves up to 93.14 puzzle accuracy and 96.05 person accuracy.