PaperlayerView exact revision on arXiv

Source-linked AI summary

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, Yutong Gu, Likang Xiao, Zhijun Chen, Weifeng Jiang, Haoyi Zhou, Jianxin Li

arXiv:2609.37203v1cs.AI

TL;DR

Natural-language logical reasoning needs machine-checkable validation of intermediate conclusions and the dependencies supporting an answer, which existing methods lack. PROOF-R1 uses UNSAT-based verification and answer-supporting dependency closure to train models to construct verifiable proofs. Across benchmarks and backbone models, it improves answer accuracy and reasoning-process verifiability.

  • Problem

    Existing methods lack machine-checkable verification of intermediate conclusions and answer-supporting proof dependencies, leaving these steps without explicit validation.

    Source: §1 · p. 2

  • Method

    PROOF-R1 uses UNSAT-based formal verification to admit conclusions as trusted proof facts and recovers the answer-supporting dependency closure to align outcome credit with proof dependencies.

    Source: §1 · p. 2

  • Results

    Across three logical reasoning benchmarks and four backbone models, PROOF-R1 improves answer accuracy and outperforms baselines in reasoning-process verifiability.

    Source: §1 · p. 3

  • Takeaways & Limitations

    The work integrates formal verification into proof construction and policy optimization for verifiable proof-based reasoning over natural-language logical problems.

    Source: §6 · p. 10

    Evaluation on English benchmarks with well-defined deductive structures covers only a controlled subset of natural-language reasoning, abstracting away ambiguity, implicit background knowledge, and pragmatic interpretation.

    Source: §5 · p. 9

Abstract

from arXiv · show

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.

1 INTRODUCTION

Natural-language logical reasoning requires not only a correct answer but a derivation whose intermediate conclusions follow from their premises and whose root establishes the target. PROOF-R1 uses formal verification to construct trusted proof facts and trace which actions support the answer, with experiments reporting improved accuracy and reasoning-process verifiability.

  • A verifiable solution is a finite derivation whose intermediate conclusions follow from declared premises under valid rules and whose root establishes the target.Source: §1 · p. 2
  • Existing methods lack machine-checkable checks of intermediate conclusions and answer-supporting dependencies, risking credit for invalid or answer-irrelevant steps.A verification verdict alone does not determine which conclusions become trusted facts or which verified inferences support the answer.Source: §1 · p. 2
  • PROOF-R1 uses UNSAT-based verification to admit a conclusion as a trusted dependency only when its reasoning action meets the proof obligations.It builds a candidate proof-certificate graph and recovers the answer-supporting dependency closure to identify actions supporting the final answer.Source: §1 · p. 2
  • Across three logical reasoning benchmarks and four backbone models, PROOF-R1 improves answer accuracy and outperforms baselines in reasoning-process verifiability.Source: §1 · p. 3
  • Behavioral and optimization analyses provide empirical support for MCFV, describe how policy learning suppresses invalid inferences through ASDC, and examine alignment of optimization signals with proof dependencies.Source: §1 · p. 3

2 RELATED WORK

Prior work spans logical-reasoning benchmarks and approaches that use symbolic solving, verification of generated steps, or formal feedback in learning. The paper distinguishes these methods by whether verification determines trusted proof facts and outcome credit during policy optimization.

  • Benchmarks range from multi-step deduction over textual facts and rules to more complex first-order-logic problems, while approaches include direct prediction and supervised proof generation.ProofWriter provides explicit proof targets; PrOntoQA uses synthetic problems with recoverable proof structures.Source: §2 · p. 3
  • Prior methods use verification at reasoning time, to check generated steps, or to construct learning signals, but generally do not let it select trusted proof facts and credited actions during optimization.Reasoning-time pipelines delegate deduction to symbolic solvers; other approaches verify generated steps or use formal feedback in supervised, preference, or reinforcement learning.Source: §2 · p. 3

3 METHODOLOGY

PROOF-R1 trains language models to construct structured proofs, admitting conclusions only through verification and aligning answer credit with the proof dependencies supporting the selected answer.

3.1 PROBLEM FORMULATION

  • A reasoning instance contains premises, a query, and candidate answer propositions; the task is to select one entailed by the premises and prove it.The premises are provided in natural language and as formal logical expressions.Source: §3.1 · p. 3

3.2 STRUCTURED PROOF GENERATION

  • PROOF-R1 represents each proof step as an action specifying dependencies, an intermediate conclusion, and a predicate-logic rule, with a terminal action matching the selected answer.The task selects an answer proposition entailed by the premises and constructs its proof.Source: §3.1 · p. 3, §3.2 · p. 4

3.3 MACHINE-CHECKABLE FORMAL VERIFICATION (MCFV)

  • MCFV checks declared dependencies against premises and previously accepted conclusions, admitting a conclusion to semantic state when an SMT solver returns UNSAT.The verifier also checks rule obligations and proof progress, retaining four Boolean verdicts that become numerical verification signals.Source: §3.3 · p. 5

3.4 ANSWER-SUPPORTING DEPENDENCY CLOSURE (ASDC)

  • ASDC traces backward from the final conclusion through the candidate proof-certificate graph to identify its premise and conclusion ancestors.The induced subgraph contains the dependencies declared to support the answer; conclusions outside the closure receive no outcome advantage, even when the answer is correct.Source: §3.4 · p. 6

3.5 VERIFICATION-ALIGNED OPTIMIZATION

  • Verification-aligned optimization combines action-verification advantages with outcome advantages masked to the answer-supporting closure, then maps action advantages to their exact token spans.The policy is optimized with a KL-regularized PPO-style clipped objective.Source: §3.5 · p. 6

4 EXPERIMENTS

Experiments evaluate PROOF-R1 on ProverQA, additional backbones, and cross-dataset benchmarks, with ablations and training analyses examining its verification components. Results show improved answer performance and proof verification across settings, while the analysis distinguishes the roles of MCFV and ASDC.

4.1 EXPERIMENTAL SETUP

  • Experiments train and evaluate on ProverQA using four backbones, then assess generalization on FOLIO and ProofWriter; the evaluated FOLIO subset requires broader quantifier rules than the training system.The backbones are Qwen2.5-7B-Instruct, Llama-3.1-8B, Qwen3-8B, and GLM-Z1-9B-0414.Source: §4.1 · p. 6

4.2 RESULTS

  • On Qwen2.5-7B-Instruct, PROOF-R1 improves Overall-split Avg@3, Pass@3, FVR, and RVR over the strongest baseline by 3.23, 2.87, 2.08, and 10.75 points, respectively, while reducing RGD from 0.80 to 0.70.On ProverQA-Hard, the respective gains are 4.86, 11.05, 1.15, and 3.66 points, with RGD falling from 1.15 to 1.05; on Qwen3-8B, Overall FVR and RVR reach 96.56 and 94.36, with lowest RGD of 0.28.Source: §4.2 · p. 7

4.3 ABLATIONS

  • The full method achieves the best result on every ProverQA-Hard metric across both tested backbones; ablations associate ASDC with closer reference-proof granularity and MCFV with higher semantic and rule validity.The w/o MCFV variant has lower RGD than w/o ASDC on both backbones, while w/o ASDC has higher FVR and RVR than w/o MCFV.Source: §4.3 · pp. 7–8

4.4 DISCUSSION

  • Across all four backbones, PROOF-R1 outperforms the backbone and SFT on all five ProverQA metrics, with additional gains reported for Llama-3.1-8B and GLM-Z1-9B-0414.For Llama-3.1-8B, Avg@3 and Pass@3 improve by 7.65 and 6.30 points; for GLM-Z1-9B-0414, FVR and RVR improve over SFT by 11.98 and 30.03 points, while RGD falls by 0.23.Source: §4.4 · p. 8
  • On FOLIO, under RFOLIO, ProverQA-trained PROOF-R1 achieves 90.85 Avg@3, 82.58 FVR, and 59.70 RVR, versus backbone scores 88.89, 64.46, and 38.87, showing transfer beyond ProverQA’s training rule ontology.The evaluated FOLIO subset requires universal and existential quantifier rule families absent from the training ontology.Source: §4.4 · p. 8
  • On Qwen3-8B, answer accuracy remains high during training as FVR and RVR rise to 96.56 and 94.36, while full verification signals become more common.Signals of 0.1 or 0.3 decline; the passage associates these with failures in semantic, rule, or proof-progress checks.Source: §4.4 · pp. 8–9
  • At training step 100, rule-conditioned centering reduces prediction error from 0.24 to 0.18 versus global-mean centering, supporting rule-conditioned verification-signal centering.The estimators are cross-validated on data unseen during fitting.Source: §4.4 · p. 9
  • MCFV and ASDC gradients are nearly orthogonal in early layers and increasingly compete with depth, yet their weighted joint direction is acute with MCFV in all 196 blocks and with ASDC in 195.The weighted MCFV gradient norm is approximately 1.14 times that of ASDC.Source: §4.4 · p. 9

5 LIMITATIONS

The evaluation addresses verifiable natural-language reasoning on English benchmarks with well-defined deductive structures, a controlled subset of unrestricted natural-language reasoning.

5 LIMITATIONS

  • The evaluation covers only a controlled subset of natural-language reasoning because it uses English benchmarks with well-defined deductive structures.Unrestricted language phenomena such as ambiguity, implicit background knowledge, and pragmatic interpretation are abstracted away.Source: §5 · p. 9
  • Coverage across multiple benchmarks, model families, and proof structures does not exhaust the broader reasoning landscape.The authors identify multilingual settings and additional logical formalisms as future directions.Source: §5 · p. 9
  • The authors identify multilingual settings and additional logical formalisms as areas for future work.Source: §5 · p. 9

6 CONCLUSION

The conclusion presents PROOF-R1 as a formal-verification-driven reinforcement-learning framework for verifiable natural-language logical reasoning. It combines verified proof-state construction with answer-supporting dependency closure, and reports improved answer performance and verification pass rates across models and benchmarks.

6 CONCLUSION

  • PROOF-R1 is a formal verification-driven reinforcement-learning framework for verifiable natural-language logical reasoning.Source: §6 · p. 10
  • The framework combines UNSAT-based machine-checkable verification with answer-supporting dependency closure to construct verified proof states and align policy learning with the final derivation.Source: §6 · p. 10
  • Experiments across multiple backbones and benchmarks show improved answer performance and reasoning-step verification pass rates.Source: §6 · p. 10

AI USE STATEMENT

The statement describes limited language polishing and semantic review by GPT models, while assigning core contributions and experimental work to the authors. The accompanying implementation passage describes action-to-token advantage alignment and policy optimization.

AI USE STATEMENT

  • GPT5.6-Sol was used for linguistic polishing, and GPT-5.5 served as an independent semantic reviewer; the authors state that core intellectual contributions and experimental results were their own.Source: AI USE STATEMENT · p. 10

A POLICY OPTIMIZATION IMPLEMENTATION

  • The normalized action-to-token alignment matrix maps each structured action’s advantage to its token span before policy optimization.The implementation distributes an action’s advantage uniformly across its span and assigns zero weight elsewhere.Source: A POLICY OPTIMIZATION IMPLEMENTATION · p. 14
  • The implementation applies group-level and negative-mass controls to action credit before projecting it onto tokens, with token losses normalized by the number of mapped actions.Source: A POLICY OPTIMIZATION IMPLEMENTATION · p. 15

B EVALUATION METRIC DEFINITIONS

The metrics evaluate sampled-answer correctness, local semantic and rule validity, and the size of the answer-supporting proof relative to a reference proof.

B EVALUATION METRIC DEFINITIONS

  • Avg@K and Pass@K evaluate answer correctness over K sampled outputs per problem, with each response labeled correct or incorrect.All reported experiments use K = 3.Source: B EVALUATION METRIC DEFINITIONS · p. 15
  • FVR and RVR are micro-averaged pass rates for eligible steps checked, respectively, for semantic validity and fidelity to the declared rule.An empty eligible set has a rate of zero.Source: B EVALUATION METRIC DEFINITIONS · p. 15
  • RGD measures the deviation between generated intermediate conclusions in the answer-supporting dependency closure and the number of steps in an available reference proof.It is defined for outputs with an available reference proof.Source: B EVALUATION METRIC DEFINITIONS · p. 16

C.1 EASY AND MEDIUM DIFFICULTY SPLITS OF MAIN RESULTS

PROOF-R1 improves answer and proof-verification results across ProverQA difficulty splits and additional benchmarks and backbones. The paper also gives a conditional soundness guarantee for its verified proof certificate.

C.1 EASY AND MEDIUM DIFFICULTY SPLITS OF MAIN RESULTS

  • On ProverQA Easy and Medium, PROOF-R1 leads on key Qwen2.5-7B-Instruct verification metrics; on Qwen3-8B it has the strongest proof-verification quality despite near-saturated answer accuracy.Its RVR gains over the strongest baseline are 22.50 points on Easy and 8.56 on Medium for Qwen2.5-7B-Instruct, and 3.97 and 8.37 points, respectively, for Qwen3-8B.Source: Table 5 · p. 16, §C.1 · p. 16

C.2 CROSS-DATASET RESULTS WITH QWEN2.5-7B-INSTRUCT

  • On FOLIO, PROOF-R1 improves Avg@3 and RVR over the backbone by 13.08 and 13.43 points; on ProofWriter, it improves Avg@3, Pass@3, FVR, and RVR by 18.66, 21.34, 6.54, and 15.72 points.On FOLIO, Pass@3 is joint-best at 84.31.Source: §C.2 · pp. 16–17, Table 6 · p. 17

C.3 HARD-SPLIT RESULTS ACROSS ADDITIONAL BACKBONE MODELS

  • On ProverQA-Hard, PROOF-R1 leads in Avg@3, Pass@3, FVR, and RVR across Llama-3.1-8B and GLM-Z1-9B-0414, with RVR gains of 4.40 and 38.03 points.It also has the lowest RGD on GLM-Z1-9B-0414.Source: Table 7 · p. 17, §C.3 · p. 17

D CONDITIONAL SOUNDNESS OF THE VERIFIED PROOF CERTIFICATE

  • Under the stated assumptions, if every conclusion in the answer-supporting certificate discharges its semantic obligation, the premises entail the goal; valid goal binding then entails the selected proposition.If every action also discharges its rule obligation, its inference conforms to its declared rule schema.Source: D CONDITIONAL SOUNDNESS OF THE… · pp. 17–18

E CROSS-BACKEND VERIFICATION AND INDEPENDENT SEMANTIC REVIEW

PROOF-R1’s verification gains persist across alternative formal backends and independent semantic review. The section also describes the rule checks and goal binding used to assess proof actions.

E CROSS-BACKEND VERIFICATION AND INDEPENDENT SEMANTIC REVIEW

F RULE ONTOLOGY

  • RULECHECK tests whether resolved dependencies establish an instantiated schema for the declared rule; unrecognized rules, untrusted dependencies, or no matching schema yield a negative verdict.GOAL BINDING requires the terminal action identifier and conclusion to match the selected proposition.Source: F RULE ONTOLOGY · pp. 20–21

G EVALUATION OF PROOF-R1 ON OUT-OF-DISTRIBUTION DATASETS

On FOLIO, PROOF-R1 retains strong proof-verification results when evaluated with an expanded inference system that includes rule families absent from training. The appendices detail the verification specification, structured output, and implementation.

G EVALUATION OF PROOF-R1 ON OUT-OF-DISTRIBUTION DATASETS

H FORMAL SPECIFICATION AND PROOFCHECK

  • A proof action is admitted only when it is well formed, uses trusted dependencies, is semantically valid and rule-faithful, and satisfies the relevant admissibility check.Ordinary actions use ProofCheck; the terminal action must match the selected candidate. ProofCheck rejects repeated conclusions, dependency restatements, and tautologies, which may be entailed without advancing proof progress.Source: H FORMAL SPECIFICATION AND PROOFCHECK · p. 22

I STRUCTURED OUTPUT CONTRACT

  • The structured summary serializes proof actions as a JSON list, with each action specifying a unique identifier, dependencies, a formal conclusion, and a declared rule.The terminal action binds its identifier and proposition to the selected answer option.Source: I STRUCTURED OUTPUT CONTRACT · p. 22, Figure 10 · p. 23

J IMPLEMENTATION DETAILS

  • Semantic verification uses Z3, while RULECHECK and PROOFCHECK evaluate rule and proof-admissibility conditions; policy optimization uses LoRA within VERL/HybridFlow.The implementation also reports paired checks with cvc5, veriT, and Isabelle on frozen evaluation outputs.Source: J IMPLEMENTATION DETAILS · p. 23

J.1 METHOD-SPECIFIC IMPLEMENTATIONS

  • The comparison standardizes data splits, formal inputs, output format, training configuration, and LoRA setup, while methods differ mainly in inference procedures, objectives, and credit assignment.The baselines include untrained Backbone, supervised SFT, GRPO, and training-free LogicAgent and GoV; PRoSFI is reimplemented from its paper description.Source: §J.1 · pp. 23–24

J.2 TRAINING CONFIGURATION

  • Table 13 summarizes training and rollout parameters shared by SFT, GRPO, PRoSFI, and PROOF-R1 unless otherwise stated.Source: Table 13 · p. 24, §J.2 · p. 24

K ADDITIONAL TRAINING DIAGNOSTICS

This section reports training and inference diagnostics and implementation details for Proof-R1, alongside case studies of how verified dependencies support answers and reveal unsupported or disconnected reasoning. One case illustrates the integration of results across reasoning branches into a coherent proof supporting the correct answer.

K ADDITIONAL TRAINING DIAGNOSTICS

  • Compared with response growth under GRPO and PRoSFI, PROOF-R1 maintains an overall stable response length as its policy gradually diverges from the reference.The figure shows training trajectories for response length on Qwen2.5-7B-Instruct and sequence-level KL divergence on Qwen3-8B.Source: Figure 11 · p. 25, K ADDITIONAL TRAINING DIAGNOSTICS · p. 25

L COMPUTATIONAL COST

  • Across two backbones, PROOF-R1, GRPO, and PRoSFI have comparable training speeds, while PROOF-R1 uses substantially fewer inference-time tokens than LogicAgent and GoV.Table 14 reports hours per 100 optimization steps and mean generated tokens per response on ProverQA.Source: Table 14 · p. 25, L COMPUTATIONAL COST · p. 25

M PROMPT TEMPLATE USED BY PROOF-R1

  • Proof-R1 uses a shared structured-action prompt across warm-up, rollouts, and evaluation, with model-specific thinking instructions and a FOLIO-specific inference-system extension.The prompt requires JSON steps with identifiers, dependencies, conclusions, and canonical rules; the final answer must bind to an option.Source: M PROMPT TEMPLATE USED BY PROOF-R1 · p. 26

N.1 CASE 1: A NEGATIVE CONCLUSION ABOUT ANIMAL CARE

  • PROOF-R1 derives that Alonzo does not harm animals through explicit, verified dependencies, with all five actions passing schema, semantic, and rule checks.A verified care conclusion supports the helping conclusion, which combines with the input’s “but not both” constraint to establish the negative answer.Source: §N.1 · p. 28

N.2 CASE 2: VERIFIED DEPENDENCIES FOR A CORRECT ANSWER

  • PROOF-R1 derives the correct answer through three verified actions, while the Backbone’s wrong intermediate conclusion is rejected and cannot be reused as a trusted dependency.The Backbone’s first action passes schema validation but fails semantic and rule checks; PROOF-R1’s verified dedication conclusion is reused to derive the answer.Source: §N.2 · p. 29

N.3 CASE 3: GENERATING THE DEPENDENCIES THAT SUPPORT THE ANSWER

  • PROOF-R1 links Clay’s facts through four verified actions to the correct answer, and backward traversal selects their answer-supporting dependencies while excluding irrelevant premises.The selected closure contains premises p1, p2, p3, and p5; p4 and p6 fall outside it, illustrating the structure targeted by ASDC training.Source: §N.3 · p. 30

N.4 CASE 4: LINKING VERIFIED BRANCHES TO THE ANSWER

  • On the same problem, the Backbone leaves a verified fact disconnected from its answer, whereas PROOF-R1 joins two verified branches to establish the correct conclusion.The available passage introduces this contrast but does not provide further case details in this part.Source: §N.4 · p. 31
  • PROOF-R1 joins two verified branches to derive the correct negative answer; backward traversal includes both branches and premises p1, p3, p4, and p5, but excludes Ivan’s p2.All four actions pass schema, semantic, and rule verification.Source: §N.4 · p. 31

Related papers

Loading 2609.37203v1…