# Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning

arXiv: https://arxiv.org/abs/2609.37203 · HTML: https://mlsanity.com/paper/2609.37203/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Test-time compute and efficient thinking, one of 17 directions in LLM reasoning.
- Builds on 30 of its 39 references that are in the map.
- First posted on arXiv 29 Sep 2026.

## Placed in

- LLM reasoning / [Test-time compute and efficient thinking](https://mlsanity.com/lr/test-time-compute-and-efficient-thinking/)

## Builds on (most cited first, 30 of 30)

- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [The Llama 3 Herd of Models](https://mlsanity.com/paper/2407.21783/) (2024)
- [LoRA: Low-Rank Adaptation of Large Language Models](https://mlsanity.com/paper/2106.09685/) (2021)
- [Chain-of-Thought Prompting Elicits Reasoning in Large Language Models](https://mlsanity.com/paper/2201.11903/) (2022)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Qwen3 Technical Report](https://mlsanity.com/paper/2505.09388/) (2025)
- [Qwen2.5 Technical Report](https://mlsanity.com/paper/2412.15115/) (2024)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [HybridFlow: A Flexible and Efficient RLHF Framework](https://mlsanity.com/paper/2409.19256/) (2024)
- [Gradient Surgery for Multi-Task Learning](https://mlsanity.com/paper/2001.06782/) (2020)
- [Math-Shepherd: Verify and Reinforce LLMs Step-by-step without Human Annotations](https://mlsanity.com/paper/2312.08935/) (2023)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thought](https://mlsanity.com/paper/2210.01240/) (2022)
- [ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Language](https://mlsanity.com/paper/2012.13048/) (2020)
- [Transformers as Soft Reasoners over Language](https://mlsanity.com/paper/2002.05867/) (2020)
- [Logic-RL: Unleashing LLM Reasoning with Rule-Based Reinforcement Learning](https://mlsanity.com/paper/2502.14768/) (2025)
- [FOLIO: Natural Language Reasoning with First-Order Logic](https://mlsanity.com/paper/2209.00840/) (2022)
- [LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Provers](https://mlsanity.com/paper/2310.15164/) (2023)
- [Testing the General Deductive Reasoning Capacity of Large Language Models Using OOD Examples](https://mlsanity.com/paper/2305.15269/) (2023)
- [Semantic-Aware Logical Reasoning via a Semiotic Framework](https://mlsanity.com/paper/2509.24765/) (2025)
- [Large Language Models Meet Symbolic Provers for Logical Reasoning Evaluation](https://mlsanity.com/paper/2502.06563/) (2025)
- [From Complex to Simple: Enhancing Multi-Constraint Complex Instruction Following Ability of Large Language Models](https://mlsanity.com/paper/2404.15846/) (2024)
- [RuleArena: A Benchmark for Rule-Guided Reasoning with LLMs in Real-World Scenarios](https://mlsanity.com/paper/2412.08972/) (2024)
- [From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofs](https://mlsanity.com/paper/2501.16207/) (2025)
- [Safe: Enhancing Mathematical Reasoning in Large Language Models via Retrospective Step-aware Formal Verification](https://mlsanity.com/paper/2506.04592/) (2025)
- [ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrations](https://mlsanity.com/paper/2510.15700/) (2025)
- [VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks](https://mlsanity.com/paper/2511.04662/) (2025)
- [Graph of Verification: Structured Verification of LLM Reasoning with Directed Acyclic Graphs](https://mlsanity.com/paper/2506.12509/) (2025)
- [LogicReward: Incentivizing LLM Reasoning via Step-Wise Logical Supervision](https://mlsanity.com/paper/2512.18196/) (2025)
- [Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries](https://mlsanity.com/paper/2603.29500/) (2026)

## Abstract (arXiv)

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.