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; Yuening He; Xihan Lei; Yashuo Luo; Hanwen Hao

cs.AISep 29, 2026

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

Authors: Qili Zhang, Qianren Mao, Hanze Cai, Kaiming Zhao, Yuening He, Xihan Lei, Yashuo Luo, Hanwen Hao, +6 more

Organizations: Zhongguancun Laboratory · Beihang University · Nanyang Technological University · Hong Kong Polytechnic University

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.

Figures & tables

Figure 1: Performance of Proof-R1 on ProverQA. Left : Accuracy and step verification. The x-axis shows answer accuracy, while the y-axis shows RVR reflecting the logical correctness of generated reasoning under schema, semantic, and rule checks. Middle : Performance of different methods. The total height of each bar represents the proportion of correct answers, while the blue segment indicates the portion whose proof traces pass formal verification. Right : Generated-to-reference proof-length ratios across methods on hard subset of ProverQA.

Figure 2: Illustrative contrast between normal LLM reasoning and verifiable logical reasoning. The normal LLM reasoning incorrectly infers that “Alex lacks access from not being a manager,” committing the fallacy of denying the antecedent. The verifiable logical reasoning derives access from “Alex’s engineer status” and exposes semantic proof obligation checked through formal verification.

Figure 3: Framework of Proof-R1 . MCFV formally verifies structured reasoning actions and maintains verified proof states. ASDC maintains the candidate proof-certificate graph and constructs the answer-supporting dependency closure. Verification-aligned optimization integrates the supervision signals from MCFV and ASDC into the policy update.

Panel of Table 1 — Table 1: Results on ProverQA, reported as means followed by standard deviations in gray. and denote training-free and training-based methods, respectively. Bold and underline denote the best and second-best means within each backbone model. ProverQA-Hard denotes the hard split of ProverQA, whereas ProverQA-Overall denotes the evaluation set across all difficulty levels.

Model	Variant	Avg@3 $\uparrow$	Pass@3 $\uparrow$	FVR $\uparrow$	RVR $\uparrow$	RGD $\downarrow$
Qwen2.5 7B-Instruct	w/o MCFV	37.86	68.34	40.16	11.65	1.08
	w/o ASDC	41.37	71.86	44.18	16.69	1.34
	Proof-R1	44.89	76.88	58.74	19.38	1.05
Qwen3-8B	w/o MCFV	90.28	98.49	82.52	57.73	0.37
	w/o ASDC	89.61	97.99	93.55	85.71	0.40
	Proof-R1	92.63	99.00	93.55	90.22	0.36

Table 2: Ablation results on ProverQA-Hard.

Table 6

Panel of Figure 4 — Figure 4: Training diagnostics of Proof-R1 . Shaded regions indicate 95% confidence intervals. (a) Performance during training, measured by Pass@3, FVR and RVR of Qwen3-8B on ProverQA. (b) Proportions of each verification signal of Qwen3-8B. (c) Prediction error of the global and rule-conditioned centering values during training.

Figure 5: Layer-wise and module-wise gradient at training on Qwen2.5-7B-Instruct. Figures show angles between (a) MCFV and ASDC, (b) MCFV and the joint direction, and (c) ASDC and the joint direction.

Appendix figures & tables15 assets

Supplementary material from the paper’s appendix.

Appendix

Panel of Table 5 — Table 5: Additional results of Qwen2.5-7B-Instruct and Qwen3-8B on the ProverQA Easy and Medium splits, reported as means followed by standard deviations in gray. and denote training-free and training-based methods, respectively. Bold and underline denote the best and second-best means within each backbone model and split.

Panel of Table 6 — Table 6: Additional cross-dataset results of ProverQA-trained Qwen2.5-7B-Instruct models on FOLIO and ProofWriter. and denote training-free and training-based methods, respectively. Bold and underline denote the best and second-best results within each dataset.

Panel of Table 7 — Table 7: Additional ProverQA-Hard results across backbone models. and denote training-free and training-based methods, respectively. Bold and underline denote the best and second-best results within each backbone model.

Figure 6: Z3–cvc5 paired local-check outcomes for Qwen2.5-7B-Instruct outputs from Backbone, SFT, and Proof-R1 . Rows denote Z3 and columns denote cvc5, using SAT / UNSAT / Other . Each cell shows its count and percentage of that method’s local check attempts.

Figure 7: Z3–veriT paired local-check outcomes for the same frozen Qwen2.5-7B-Instruct outputs. Rows denote Z3 and columns denote veriT, using SAT / UNSAT / Other . Each cell shows its count and percentage of that method’s local check attempts.

Figure 8: Z3–Isabelle paired local-check outcomes for the same frozen Qwen2.5-7B-Instruct outputs. Rows denote Z3 and columns denote Isabelle, using SAT / UNSAT / Other . Each cell shows its count and percentage of that method’s local check attempts. Isabelle requires a genuine Nitpick countermodel for SAT and an oracle-free kernel proof for UNSAT . Other retains input-processing failures and unresolved searches.

	FVR $\uparrow$				RVR $\uparrow$
Method	Z3	cvc5	veriT	Isabelle	Z3	cvc5	veriT	Isabelle
Backbone	67.64	67.64	67.64	67.64	18.91	18.91	18.91	18.91
SFT	66.39	66.39	66.39	66.39	19.94	19.94	19.94	19.94
Proof-R1	70.17	70.17	70.17	70.17	41.19	41.19	41.19	41.19

Appendix

Table 8: Cross-backend verification of the same frozen Qwen2.5-7B-Instruct outputs on ProverQA Overall. Values are percentages; every semantic check uses the indicated backend.

Figure 9: Z3–GPT-5.5 local semantic review of 2,000 sampled steps from frozen Qwen2.5-7B-Instruct outputs. Rows denote Z3 outcomes; columns denote GPT-5.5 judgments. SAT corresponds to invalid and UNSAT to valid . Each cell shows its count and percentage of reviewed steps.

Reviewer	Number	Valid	Invalid	Uncertain	Agreed / reference	Weighted (%)
GPT-5.5	2,000	1,199	778	23	1,952 / 1,957	99.73

Appendix

Table 9: Agreement is measured on determinate Z3/cvc5 outcomes. The weighted percentage uses the sampling weights of the 2,000-step cohort.

Rule	Symbolic form
IE : IMPLICATION_ELIMINATION	$A\!\to\!B,\ A\vdash B$
MT : MODUS_TOLLENS	$A\!\to\!B,\ \neg B\vdash\neg A$
XOI : EXCLUSIVE_DISJUNCTION_INTRODUCTION	$A,\ \neg B\vdash A\oplus B;\;\neg A,\ B\vdash A\oplus B$
XOE : EXCLUSIVE_DISJUNCTION_ELIMINATION	$A\oplus B,\ A\vdash\neg B;\;A\oplus B,\ \neg A\vdash B$
DS : DISJUNCTIVE_SYLLOGISM	$A\lor B,\ \neg A\vdash B$
CI : CONJUNCTION_INTRODUCTION	$A,\ B\vdash A\land B$

Appendix

Table 10: Predicate-logic rules covered by the ProverQA training data.

Rule	Symbolic form
UIC : UNIVERSAL_IMPLICATION_CHAINING	$\forall x(A\!\to\!B),\ \forall x(B\!\to\!C)\vdash\forall x(A\!\to\!C)$
UPI : UNIVERSAL_PROPOSITIONAL_INFERENCE	$\forall x(A\!\to\!B),\ \forall x(A\!\to\!C)\vdash\forall x(A\!\to\!(B\land C))$
EI : EXISTENTIAL_INTRODUCTION	$A(a)\vdash\exists x\,A(x);\;A(a),B(a)\vdash\exists x(A(x)\land B(x))$
ECE : EXISTENTIAL_CONJUNCTION_ELIMINATION	$\exists x(A\land B)\vdash\exists x\,A;\;\exists x(A\land G)\vdash G\ (x\notin\mathrm{FV}(G))$
EIE : EXISTENTIAL_IMPLICATION_ELIMINATION	$\exists xA,\ \forall x(A\!\to\!B)\vdash\exists xB$
ECI : EXISTENTIAL_CONJUNCTION_INTRODUCTION	$\exists xA,G\vdash\exists x(A\land G)\ (x\notin\mathrm{FV}(G))$

Appendix

Table 11: Training-time-unseen rule families and their representative symbolic forms.

Model	Rule group	FVR	RVR
Backbone	$\mathcal{R}_{\mathrm{train}}$	64.71	39.73
	$\mathcal{R}_{\mathrm{unseen}}$	63.24	34.92
SFT	$\mathcal{R}_{\mathrm{train}}$	62.02	39.77
	$\mathcal{R}_{\mathrm{unseen}}$	67.50	45.71
Proof-R1	$\mathcal{R}_{\mathrm{train}}$	81.55	58.87
	$\mathcal{R}_{\mathrm{unseen}}$	86.21	63.08

Appendix

Table 12: FVR/RVR (%) under

\mathcal{R}_{\mathrm{FOLIO}}

on frozen Qwen3-8B FOLIO outputs, grouped by whether the current rule belongs to

\mathcal{R}_{\mathrm{train}}

\mathcal{R}_{\mathrm{unseen}}

Category	Parameter	Value
LoRA	Rank	8
	Alpha	16
	Target modules	[Q, K, V, O, GATE, UP, DOWN]
Rollout	Group size ( $K$ )	8
	Sampling temperature	0.8
	Top- $p$	0.95

Appendix

Table 13: Training and rollout parameters. Unless stated otherwise, these settings are shared by SFT, GRPO, PRoSFI, and Proof-R1 .

Figure 11: Training trajectories of response length and policy divergence during reinforcement learning. Left: Mean response length of different methods on Qwen2.5-7B-Instruct during training. Right: Sequence-level KL divergence of the Qwen3-8B policy from the frozen reference policy during training. Solid lines denote EMA-smoothed trajectories, and shaded regions indicate one exponentially weighted local standard deviation.

	Qwen2.5-7B-Instruct		Qwen3-8B
Method	h/100 steps	tokens/response	h/100 steps	tokens/response
Backbone	0.00	354.2	0.00	1,213.8
LogicAgent	0.00	2,054.5	0.00	12,572.6
GoV	0.00	2,004.7	0.00	9,127.9
SFT	0.11	373.6	0.19	1,229.9
GRPO	2.64	836.4	4.70	1,176.3

Appendix

Table 14: Computational cost on ProverQA. Time is measured in hours per 100 optimization steps. Inference-time token consumption is the mean number of generated tokens per response.

Explore similar work

Logic-Regularized Verifier Elicits Reasoning from LLMs
May 7, 2026Xinyu Wang, Changzhi Sun, Lian Cheng +4LLM Reasoning Strategies Reasoning Paths
Department of Computer Science and Technology, East China Normal University · Institute of Artificial Intelligence (TeleAI), China Telecom
ProofVerifier: A Scalable, Diversity-Driven Framework for Natural-Language Proof Verification
Feb 2, 2026Haotong Yang, Zitong Wang, Shijia Kang +7Proof Large Language Model Reliability
Peking University, Beijing, China · Tencent
Answer-Conditioned Chains of Thought Degrade Verifiable-Reasoning Distillation in Large Language Models
Jul 16, 2026Jungseob Lee, Seungyoon Lee, Suhyune Son +4LLM Reasoning Strategies Reasoning Skills
1Korea University · 2Zoom Communications · 3Yonsei University

May 7, 2026, cs.CLJ/K move · Enter open · S save

Logic-Regularized Verifier Elicits Reasoning from LLMs

Xinyu Wang, Changzhi Sun, Lian Cheng, Yuanbin Wu+3

Department of Computer Science and Technology, East China Normal University · Institute of Artificial Intelligence (TeleAI), China Telecom

LLM Reasoning Strategies Reasoning Paths

Open paper AskPDF arXiv

Verifiers are crucial components for enhancing modern LLMs' reasoning capability. Typicalverifiers require resource-intensive superviseddataset construction, which is costly and faceslimitations in data diversity. In this paper, wepropose LOVER, an unsupervised verifier regularized by logical rules. LOVER treats theverifier as a binary latent variable, utilizinginternal activations and enforcing three logical constraints on multiple reasoning paths:negation consistency, intra-group consistency,and inter-group consistency (grouped by thefinal answer). By incorporating logical rulesas priors, LOVER can leverage unlabeled examples and is directly compatible with any offthe-shelf LLMs. Experiments on 10 datasetsdemonstrate that LOVER significantly outperforms unsupervised baselines, achieving performance comparable to the supervised verifier(reaching its 95% level on average). The sourcecode is publicly available at https://github.com/wangxinyufighting/llm-lover.

Abstract

Explore similar work

Logic-Regularized Verifier Elicits Reasoning from LLMs

ProofVerifier: A Scalable, Diversity-Driven Framework for Natural-Language Proof Verification

Answer-Conditioned Chains of Thought Degrade Verifiable-Reasoning Distillation in Large Language Models