Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries

Luoxin Chen; Yichi Zhou; Huishuai Zhang

cs.AIMar 31, 2026

Learning to Generate Formally Verifiable Step-by-Step Logic Reasoning via Structured Formal Intermediaries

Authors: Luoxin Chen, Yichi Zhou, Huishuai Zhang

Organizations: Wangxuan Institue of Computer Technology, Peking University. · ByteDance.

Abstract

Large language models (LLMs) have recently demonstrated impressive performance on complex, multi-step reasoning tasks, especially when post-trained with outcome-rewarded reinforcement learning Guo et al. 2025. However, it has been observed that outcome rewards often overlook flawed intermediate steps, leading to unreliable reasoning steps even when final answers are correct. To address this unreliable reasoning, we propose PRoSFI (Process Reward over Structured Formal Intermediates), a novel reward method that enhances reasoning reliability without compromising accuracy. Instead of generating formal proofs directly, which is rarely accomplishable for a modest-sized (7B) model, the model outputs structured intermediate steps aligned with its natural language reasoning. Each step is then verified by a formal prover. Only fully validated reasoning chains receive high rewards. The integration of formal verification guides the model towards generating step-by-step machine-checkable proofs, thereby yielding more credible final answers. PRoSFI offers a simple and effective approach to training trustworthy reasoning models.

Figures & tables

Figure 1: Pipeline for Process Reward over Structured Formal Intermediates and comparison with Outcome Reward. The process begins with a problem statement (left block) containing multiple propositions (h1–h4) related to individuals (Hattie and Candy). Then, a large language model (LLM) first generates natural language reasoning steps to solve the problem (middle block). The Outcome Reward approach then directly compares the generated answer with the ground truth, assigning a reward of 1 if they match. In contrast, PRoSFI introduces an additional step by generating structured formal intermediates that capture logical dependencies, inferred conclusions, and the application of formal inference rules such as Hypothetical Syllogism and Modus Ponens . These formal representations are then submitted to a Formal Prover , which verifies the logical soundness of the reasoning. In the illustrated example, although the generated answer (“Hattie does not gain community respect” is false) is correct, the formal proof fails verification. As a result, PRoSFI assigns a low reward despite the correct outcome.

Metric	Definition
Answer Correct Rate	$\dfrac{\#\text{Final Answer Correct}}{\#\text{Total Examples}}$
Reward Hit Rate	$\dfrac{\#\text{Outputs with Max Reward}}{\#\text{Total Examples}}$
Soundness	$\dfrac{\#\text{Answer Correct \& Path Valid}}{\#\text{Total Examples}}$

Table 1: Evaluation metrics and their definitions.

Method	Metric (%)	Hard	Extra
Outcome-CoT	Answer Correct Rate	91.31	86.96
Outcome-CoT	GPT Soundness	21.97	11.87
Direct Lean Generation	Answer Correct Rate	92.29	83.15
Direct Lean Generation	GPT Soundness	33.11 $\uparrow 11.1$	10.45 $\downarrow-1.4$
ProSFI	Answer Correct Rate	92.97	91.94
ProSFI	GPT Soundness	76.07 $\uparrow 54.1$	56.10 $\uparrow 44.2$

Table 2: Results on ProverQA Hard and Extra. GPT Soundness values include the difference of each method versus the Outcome-CoT baseline.

Figure 2: Left: GPT Soundness on ProverQA-hard subset. Right: GPT Soundness on ProverQA-extra subset. As the number of sampled paths increases, PRoSFI with PRoSFI selection consistently improves, while Outcome-CoT cannot benefit due to translation limits.

Figure 3: Left: Metric correlation heatmap on ProverQA-Hard . Right: Metric correlation heatmap on ProverQA-Extra . Compared to Answer Correctness, PRoSFI Reward Hit better reflects reasoning-path soundness.

Method	Metric (%)	2ppl	3ppl	4ppl	5ppl	6ppl	7ppl	8ppl
Outcome-CoT	Answer Correct Rate	99.63	99.81	99.81	98.13	98.69	95.13	94.25
Outcome-CoT	GPT Soundness	64.81	68.56	69.13	61.75	56.06	53.88	47.94
PRoSFI	Answer Correct Rate	99.75	99.31	99.75	99.63	99.25	98.56	97.38
PRoSFI	GPT Soundness	86.56 $\uparrow 21.8$	90.31 $\uparrow 21.8$	90.50 $\uparrow 21.4$	90.44 $\uparrow 28.7$	91.00 $\uparrow 35.0$	86.31 $\uparrow 32.4$	80.94 $\uparrow 33.0$

Table 3: Results on Knights and Knaves dataset.

Appendix figures & tables1 asset

Supplementary material from the paper’s appendix.

Appendix

Figure 4: Left: Confusion matrix of answer correctness vs. reasoning soundness for Outcome-CoT on the ProverQA-hard subset. Right: Corresponding results on the ProverQA-extra subset. The lack of alignment between correct answers and sound reasoning indicates that answer accuracy alone is not a sufficient criterion for judging the quality of reasoning.

LLM Reasoning

Large language model reasoning studies how models solve multi-step problems, verify intermediate steps, and use computation or tools reliably.

See all 924 papers

Learning to Prove, Not Just to Answer: Reinforcement Learning from Formal Verification for Natural-Language Logical Reasoning
Sep 29, 2026Qili Zhang, Qianren Mao, Hanze Cai +11Logical Reasoning RL for Language Model Reasoning
Zhongguancun Laboratory · Beihang University · Nanyang Technological University +1
Step-wise Rubric Rewards for LLM Reasoning
May 17, 2026Weichu Xie, Haozhe Zhao, Wenpu Liu +15Reward Modeling Credit Assignment in RL
Peking University · JD Explore Academy · Shanghai Jiao Tong University +2
Correct Answers from Sound Reasoning: Verifiable Process Supervision for Language Models
Apr 3, 2026Kyuyoung Kim, Kevin Wang, Yunfei Xie +7Process Supervision RL for Language Model Reasoning
KAIST AI · University of Texas, Austin · Rice University +3

Sep 29, 2026J/K move · Enter open · S save

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

Qili Zhang, Qianren Mao, Hanze Cai, Kaiming Zhao+10

Zhongguancun Laboratory · Beihang University · Nanyang Technological University+1

Logical Reasoning RL for Language Model Reasoning

Open paper AskPDF 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.

Abstract

LLM Reasoning

Explore similar work

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

Step-wise Rubric Rewards for LLM Reasoning

Correct Answers from Sound Reasoning: Verifiable Process Supervision for Language Models