论文
学习证明，而不仅仅是回答：自然语言逻辑推理的形式验证强化学习
Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
摘要
大语言模型 (LLM) 越来越多地用于自然语言逻辑推理，其中最终答案很容易检查，但其背后的证明却很难。在自然语言逻辑推理中，中间结论应该从其前提中得出，并且由此产生的推导应该支持最终答案。现有方法缺乏对中间结论和答案支持证明依赖性的机器可检查验证，因此它们可能会将功劳分配给无效或与答案无关的步骤。我们提出了 Proof-R1，这是一种来自形式验证的强化学习框架，可训练大语言模型为自然语言逻辑推理构建可验证的证明。仅当相应的推理动作通过基于 UNSAT 的机器可检查形式验证满足证明义务时，Proof-R1 才会承认生成的结论进入已验证的证明状态。 Proof-R1 还恢复支持答案的依赖闭包，以跟踪最终答案的证明结构，并将结果信用与证明依赖项对齐。实验表明，Proof-R1 提高了三个逻辑推理基准和四个骨干模型的答案准确性，并且在推理过程可验证性方面优于免训练Agent和基于训练的方法。