Language models trained to prove reasoning steps for better answers
Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
Artificial Intelligence
Summary
Some computer programs can answer tricky questions, but the way they explain their answers is not always clear or trustworthy. The authors created a new way to teach language models to provide proofs that can be checked by a computer, making sure every step in the reasoning is valid. This helps the programs give more accurate answers and clearer explanations. Their approach was tested on several challenges and improved performance compared to previous methods.
What this means in practice
- •For automated reasoning engineers: Develop AI systems that provide verifiable logical proofs to support their answers, improving trust and correctness in decision-making.
- •For ai system developers: Improve natural-language reasoning tasks by integrating machine-checkable proof generation to enhance answer accuracy and transparency.
Authors
Qili Zhang, Qianren Mao, Hanze Cai, Kaiming Zhao, Yuening He, Xihan Lei, Yashuo Luo, Hanwen Hao, Yutong Gu, Likang Xiao, Zhijun Chen, Weifeng Jiang, Haoyi Zhou, Jianxin Li
Abstract
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.