通过结构化形式化中间产物学习生成可形式化验证的逐步逻辑推理

摘要

大语言模型（LLM）近来在复杂的多步推理任务上展现出令人瞩目的表现，尤其是在采用结果奖励强化学习进行后训练时（Guo et al. 2025）。然而，已有观察表明，结果奖励常常忽视有缺陷的中间步骤，导致即便最终答案正确，推理步骤也不可靠。为解决这一不可靠推理问题，我们提出 PRoSFI（Process Reward over Structured Formal Intermediates），一种在不牺牲准确性的前提下增强推理可靠性的新型奖励方法。直接生成形式化证明对中等规模（7B）模型而言几乎难以完成，因此模型并不这样做，而是输出与其自然语言推理对齐的结构化中间步骤。随后，每一步都由形式化证明器（formal prover）验证。只有完全通过验证的推理链才能获得高奖励。形式化验证的引入引导模型生成逐步可机器检查的证明，从而产生更可信的最终答案。PRoSFI 为训练可信赖的推理模型提供了一种简单而有效的方法。

通过结构化形式化中间产物学习生成可形式化验证的逐步逻辑推理：论文配图 — 图 1：相对于结构化正式中间体的过程奖励的流程以及与结果奖励的比较。该过程从一个问题陈述（左块）开始，其中包含与个人（海蒂和坎迪）相关的多个命题（h1-h4）。然后，大语言模型（LLM）首先生成自然语言推理步骤来解决问题（中间块）。然后，结果奖励方法直接将生成的答案与基本事实进行比较，如果匹配则分配奖励 1。相比之下，PRoSFI 引入了一个额外的步骤，即生成结构化的形式中间体，捕获逻辑依赖性、推断结论以及形式推理规则（例如假设三段论和 Modus Ponens）的应用。然后将这些形式表示提交给形式证明者，由形式证明者验证推理的逻辑合理性。在所示示例中，虽然生成的答案（“Hattie 没有获得社区尊重”是错误的）是正确的，但形式证明未能验证。因此，尽管结果正确，但 PROSFI 分配的奖励较低。