奖励新颖的推论：求解器引导的逻辑推理过程奖励

逻辑推理仍然是大语言模型（LLM）的主要挑战，特别是在需要精确约束跟踪、一致性保持和多步推导的结构化问题上。对于小规模的LLM来说，这一挑战尤其严峻，因为它们更容易产生不一致、冗余或脆弱的推理轨迹。现有的改进逻辑推理的方法在很大程度上优化了最终答案的正确性，仅对中间推理过程提供了较弱的监督。在这项工作中，我们提出了 SPRING：（用于新颖逻辑推理步骤生成的求解器引导过程奖励）。 SPRING 使用 SMT 求解器作为中间推理步骤的训练时验证器，以提供过程级监督。它引入了新颖推理步骤的概念，即逻辑上有效的步骤，与不断发展的推理状态一致，并且尚未被先前接受的非矛盾推论所暗示。基于这种基于求解器的评估，它设计了过程奖励，鼓励新的推理进展，同时惩罚矛盾和无信息的推理步骤。对三个逻辑推理基准（ZebraLogic、AR-LSAT、Knights and Knaves）以及四个 LLM 的评估表明，SPRING 始终优于基础 LLM、仅结果奖励基准和 Logic-LM。在 ZebraLogic 上，SPRING 比基本 LLM 和最强的仅结果基线分别将谜题准确度提高了 49.71 分和 15.43 分。在 AR-LSAT 上，其整体准确率分别提高了 64.93 分和 12.14 分。在《Knights and Knaves》中，SPRING 的谜题准确率高达 93.14，人物准确率高达 96.05。