发表机构
Zhongguancun Laboratory; Beihang University; Nanyang Technological University; Hong Kong Polytechnic University（中关村实验室; 北京航空航天大学; 南洋理工大学; 香港理工大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对自然语言逻辑推理中证明难以机器验证的问题，提出基于形式化验证的强化学习框架Proof-R1，通过UNSAT验证和依赖闭包对齐奖励，提升答案准确性与推理过程可验证性。
AI 中文摘要
大型语言模型（LLMs）正越来越多地被部署用于自然语言逻辑推理，在这种推理中，最终答案易于检查，但其背后的证明却不易验证。在自然语言逻辑推理中，中间结论应遵循其前提，且由此产生的推导应支持最终答案。现有方法缺乏对中间结论和答案支持性证明依赖的机器可检查验证，因此可能将奖励归于无效或与答案无关的步骤。我们提出Proof-R1，一种基于形式化验证的强化学习框架，用于训练LLMs为自然语言逻辑推理构建可验证的证明。Proof-R1仅当相应的推理动作通过基于UNSAT的机器可检查形式化验证满足证明义务时，才将生成的结论纳入已验证的证明状态。Proof-R1还恢复答案支持的依赖闭包，以追踪最终答案的证明结构，并将结果奖励与证明依赖对齐。实验表明，Proof-R1在三个逻辑推理基准和四个骨干模型上提高了答案准确性，并在推理过程可验证性方面优于无训练代理和基于训练的方法。
英文摘要
Large language models (LLMs) are increasingly deployed for natural-language logical reasoning, where the final answer is easy to check but the proof behind it is not. In natural-language logical reasoning, an intermediate conclusion should follow from its premises, and the resulting derivation should support the final answer. Existing methods lack machine-checkable verification of intermediate conclusions and answer-supporting proof dependencies, so they may assign credit to invalid or answer-irrelevant steps. We propose Proof-R1, an RL framework from formal verification that trains LLMs to construct verifiable proofs for natural-language logical reasoning. Proof-R1 admits a generated conclusion into the verified proof state only when the corresponding reasoning action satisfies the proof obligations through UNSAT-based machine-checkable formal verification. Proof-R1 also recovers the answer-supporting dependency closure to trace the proof structure of the final answer and align outcome credit with the proof dependencies. Experiments demonstrate that Proof-R1 improves answer accuracy across three logical reasoning benchmarks and four backbone models and outperforms training-free agents and training-based methods in terms of reasoning-process verifiability.
