PaperlayerView exact revision on arXiv

Source-linked AI summary

Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification

Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, Yike Guo

arXiv:2601.22642v2cs.LG

TL;DR

LLMs can produce logically inconsistent reasoning because probabilistic decoding lacks inherent consistency mechanisms and existing verifiers often overlook intermediate steps. This paper dynamically interleaves formal verification with generation and trains models in two stages, achieving average improvements of 10.4% for 7B and 14.2% for 14B over SOTA baselines across six benchmarks.

  • Problem

    LLMs lack inherent consistency mechanisms, while existing verifiers often overlook intermediate reasoning steps.

  • Method

    The framework dynamically interleaves formal verification with generation and combines verification-guided supervised fine-tuning with policy optimization.

  • Results

    10.4% and 14.2% average improvements over SOTA baselines were achieved by the 7B and 14B models, respectively, across six benchmarks.

  • Takeaways & Limitations

    The results support formal verification as a scalable mechanism for improving advanced LLM reasoning while providing interpretable step-level correctness guarantees.

  • Takeaways & Limitations

    Real-time formal verification approximately doubles reinforcement-learning training time relative to the tool-free General-Reasoner baseline.

Abstract

from arXiv · show

Large Language Models (LLMs) show remarkable capabilities, yet their stochastic next-token prediction creates logical inconsistencies and reward hacking that formal symbolic systems avoid. To bridge this gap, we introduce a formal logic verification-guided framework that dynamically interleaves formal symbolic verification with the natural language generation process, providing real-time feedback to detect and rectify errors as they occur. Distinguished from previous neuro-symbolic methods limited by passive post-hoc validation, our approach actively penalizes intermediate fallacies during the reasoning chain. We operationalize this framework via a novel two-stage training pipeline that synergizes formal logic verification-guided supervised fine-tuning and policy optimization. Extensive evaluation on six benchmarks spanning mathematical, logical, and general reasoning demonstrates that our 7B and 14B models outperform state-of-the-art baselines by average margins of 10.4% and 14.2%, respectively. These results validate that formal verification can serve as a scalable mechanism to significantly push the performance boundaries of advanced LLM reasoning.

1. Introduction

The introduction identifies a logical-consistency gap in LLM reasoning and proposes dynamically interleaving formal verification with generation to detect and correct errors in real time. A two-stage training framework and six-benchmark evaluation support the method’s effectiveness and scalability.

  • Motivation: LLMs’ probabilistic decoding lacks inherent consistency mechanisms, creating risks including hallucinations, safety vulnerabilities, and reward hacking.The introduction contrasts these risks with the consistency guarantees sought through formal verification.
  • Motivation: 39.3% of steps in chains with correct final answers were formally disproved, revealing substantial logical inconsistency despite answer correctness.The paper reports this finding from formal verification analysis of generated reasoning chains.
  • Framework: The proposed framework dynamically interleaves formal symbolic verification with natural-language generation, using satisfiability results, counterexamples, and execution outputs for real-time error detection and rectification.This extends standard chain-of-thought reasoning beyond static filtering and narrow-domain theorem proving.
  • Training: The two-stage training pipeline combines formal verification-guided supervised fine-tuning with policy optimization and execution-based validation.The data synthesis pipeline is designed to enforce logical soundness and structural integrity.

2. Related Works

Prior work has established supervised fine-tuning for LLM reasoning, expanded formal verification through machine-checkable tools, and explored interleaved versus post-hoc verification. However, supervised fine-tuning struggles with complex objectives and multi-step error correction, while post-hoc verification cannot prevent error accumulation during generation.

  • Supervised Fine-Tuning: Supervised fine-tuning on chain-of-thought examples and step-by-step solutions has been foundational for developing LLM reasoning capabilities.Recent efforts curate high-quality datasets in mathematics, code, and science.
  • Supervised Fine-Tuning: SFT alone cannot effectively optimize complex objectives beyond imitation and struggles with multi-step error correction.These limitations motivate combining supervised learning with additional optimization and verification mechanisms.
  • Formal Verification: Formal verification research integrates theorem provers, code interpreters, and symbolic solvers to provide machine-checkable validation beyond LLM-as-a-judge approaches.This direction is recognized as important for grounding generative models in verifiable systems.
  • Verification Strategies: HERMES interleaves informal reasoning with Lean-verified steps for real-time soundness, whereas Safe audits completed reasoning chains post hoc and cannot prevent error accumulation during generation.HERMES requires mature formal libraries, while Safe uses a passive verification mode.

3. Preliminaries

This section motivates formal logic verification by showing that conventional language reasoning lacks guaranteed logical validity, while verification integration improves performance across domains. It defines a reasoning paradigm that interleaves natural-language steps, formal specifications, and verifier feedback.

  • Motivation: LLM reasoning lacks mechanisms to ensure global logical consistency, motivating formal verification that can reliably validate reasoning steps with formal solvers.The section contrasts probabilistic natural-language reasoning with the rigor of formal verification.
  • Motivation: Across 500 instances per domain, FLV-SFT achieved 291 vs. 219 correct answers in Logical (+32.8%) and 243 vs. 163 in Mathematical (+49.3%) compared with Natural-SFT.FLV-SFT incorporates formal logic verification, whereas Natural-SFT relies solely on natural-language reasoning.
  • Formal Logic Verification-Guided Reasoning: The proposed paradigm extends each reasoning step with a formal specification and a formal verification result, producing an interleaved chain z′ = (s1, f1, v1, …, sn, fn, vn).Formal specifications may encode symbolic constraints, SAT clauses, SMT formulas, or executable code.
  • Formal Logic Verification-Guided Reasoning: During inference, the verifier returns satisfiability results, counterexamples, proof traces, execution outputs, or error messages to guide subsequent logically sound and verifiable reasoning steps.The feedback is provided at each reasoning step.

4. Methodology

The methodology interleaves formal verification with language reasoning through a two-stage pipeline: verification-guided supervised fine-tuning followed by reinforcement learning. It synthesizes and validates aligned reasoning–proof–execution data, then optimizes structure, semantics, and computational efficiency with composite rewards.

  • Two-stage training: The framework combines supervised fine-tuning and reinforcement learning to generate interleaved natural-language reasoning and formal proofs while enforcing logical soundness and correctness.SFT teaches the structured format; RL further optimizes verification-guided reasoning.
  • Supervised fine-tuning: Because interleaved reasoning-and-proof datasets are scarce, the SFT stage uses hierarchical formal-proof data synthesis to support self-verification.The pipeline aligns the model’s output distribution with a structured reasoning format.
  • Supervised fine-tuning: K = 4 candidate reasoning chains are generated, correct chains are selected, and each is decomposed into logical modules paired with synthesized formal proofs and expected execution outputs.A judge model evaluates final-answer correctness before formalization.
  • Execution-based validation: Generated proofs are executed and accepted by exact match or semantic equivalence, while minor inconsistencies trigger proof rewriting and failed cases are discarded.Rewriting conditions the natural-language reasoning on the actual execution result to preserve coherence.
  • Execution-based validation: The resulting training examples align natural-language hypotheses, formal logic reasoning, and execution feedback, providing high-quality supervision for reliable reasoning patterns.Each structured instance is represented as (s, f, v) with validated proofs and verified execution outputs.
  • Reinforcement learning: Reinforcement learning uses a multi-dimensional reward function that provides fine-grained feedback on structure, semantics, and computational efficiency.The method additionally optimizes the policy with GRPO using group-normalized advantages to emphasize relative output quality.

5. Experiment

The experiments evaluate FLV across logical, mathematical, and general reasoning benchmarks, using standardized OpenCompass evaluation with greedy decoding except AIME24 avg@16 sampling. FLV outperforms natural-language and tool-integrated baselines, with ablations attributing gains to formal verification and multi-stage training despite moderate token overhead.

  • Evaluation: Evaluation spans logical reasoning with KOR and BBH, mathematical reasoning with MATH-500 and AIME 2024, and general reasoning with GPQA-Diamond and TheoremQA.These benchmarks cover knowledge-grounded logic, multi-step deduction, competition and Olympiad mathematics, graduate-level science, and theorem application.
  • Results: 49.8 average score for FLV-SFT on Qwen2.5-7B, exceeding the strongest natural-language baseline RLPR at 47.0 by 2.8 points.Even the supervised fine-tuning stage surpasses all comparative RL baselines on the 7B scale.
  • Results: 30.2% on AIME 2024 for FLV-RL-14B, nearly doubling General-Reasoner at 17.5% and far exceeding the Base model at 3.6%.FLV-RL-14B also achieves 81.4% on MATH500 and 63.5% on TheoremQA, outperforming all baselines and the nearest TheoremQA competitor by over 8 points.
  • Results: Formal verification acts as a verifier enforcing logical consistency, whereas SimpleTIR primarily uses tools as solvers for direct computation, yielding 41.0 on AIME24.FLV consequently shows dominant performance on logic-heavy benchmarks such as KOR.
  • Ablation Study: 49.8% average accuracy for FLV-SFT versus 36.5% for Natural-SFT, including gains of +16.2 points on KOR-Bench and +13.9 points on TheoremQA.The comparison uses identical training data and attributes the improvements to formal proofs and execution validation.
  • Ablation Study: 51.9% for FLV-RL after improving from 30.0% for Base to 49.8% for FLV-SFT, while natural-language RL changes only from 36.5% to 37.0%.The results indicate that formal verification provides more stable and reliable reward signals for policy optimization; FLV-RL incurs moderate computational overhead.

6. Conclusion

The work addresses the tension between probabilistic language generation and logical consistency by dynamically integrating formal logic verification into LLM reasoning. Its two-stage training methodology combines FLV-SFT with formal logic verification-guided policy optimization, using real-time symbolic feedback to mitigate logical fallacies.

  • 6. Conclusion: The framework dynamically integrates formal logic verification into the reasoning process to address logical inconsistency in probabilistic language generation.It targets the fundamental tension between probabilistic language generation and logical consistency in LLM reasoning.
  • 6. Conclusion: The two-stage training methodology combines FLV-SFT’s rigorous data synthesis pipeline with formal logic verification-guided policy optimization.These components jointly operationalize the proposed verification-guided approach.
  • 6. Conclusion: Real-time symbolic feedback can effectively mitigate logical fallacies during LLM reasoning.The conclusion attributes this effect to integrating formal verification into the reasoning process.

Limitations · A. Reward Calculation Pseudocode

The framework’s main limitation is computational overhead from real-time formal verification, while its reward-calculation pseudocode specifies hierarchical format, correctness, and verification rewards with constraint checks and penalties. Reward computation begins with linear-time screening of generated tokens before further structural and semantic evaluation.

  • Limitations: Limitations: Real-time formal verification approximately doubles reinforcement-learning training time compared with the tool-free General-Reasoner baseline.The paper characterizes this overhead as a primary limitation.
  • Limitations: Limitations: The authors deem the added cost acceptable because the framework yields 10.4%-14.2% performance improvement and superior data efficiency.They report comparable results using only a fraction of the training data required, although the passage is truncated before specifying the comparison.
  • A. Reward Calculation Pseudocode: A. Reward Calculation Pseudocode: Table 3 presents the complete algorithmic implementation of the multi-component reward function used in FLV-RL training.The table is described as a hierarchical reward function for formal logic verification-guided policy optimization.
  • A. Reward Calculation Pseudocode: A. Reward Calculation Pseudocode: The pseudocode computes format rewards, correctness rewards, and formal verification rewards.It gives step-by-step computation for these reward components.
  • A. Reward Calculation Pseudocode: A. Reward Calculation Pseudocode: The reward algorithm includes constraint checks and penalty mechanisms described in Section 4.These mechanisms are part of the complete FLV-RL implementation.
  • A. Reward Calculation Pseudocode: A. Reward Calculation Pseudocode: Initial screening for pathological states and invalid formats scans the L-token response in O(L) time.The scan detects repetition loops, counts tool invocations Ncall, and validates tags before valid responses proceed to structural reward computation.

B. Dataset Construction Details

The dataset construction pipeline combines generated reasoning, formal logic extraction and translation, and execution-based verification to produce training data with human-readable reasoning and mathematically sound validation. Validation retains semantically equivalent proofs while discarding fundamentally misaligned cases and filters problems to meaningful difficulty for reinforcement learning.

  • Data construction: The pipeline generates reasoning questions, extracts and formally translates logic, then verifies outputs to create supervised fine-tuning data combining readable reasoning with formal validation.This construction process is designed to teach both human-readable reasoning patterns and mathematically sound logical validation.
  • Filtering stages: 72.2% retention at Stage 3 reflects Claude’s high-quality formal translation combined with execution-based validation.Stage 2 excludes trivially easy problems with pass rate=1.0 and completely unsolvable problems with pass rate=0, retaining meaningful difficulty for reinforcement learning.
  • Validation outcomes: 59.55% of proofs in the 9,162-chain merged dataset achieve perfect alignment and pass Stage 1 without further verification.The analysis covers a subset of the full training data.
  • Validation outcomes: 26.53% of proofs have 95–100% match rates, indicating strong but imperfect alignment that requires semantic equivalence checking in Stage 2.These proofs fall into a high-confidence range rather than achieving perfect alignment.
  • Validation outcomes: 62.22% (2,306 instances) of below-100% cases preserve semantic equivalence, while 37.78% (1,400 instances) show fundamental misalignment and are discarded.The semantically equivalent cases recover through Stage 2 verification or Stage 3 proof rewriting.
  • Validation outcomes: 0.83% of proofs have critically low match rates below 60%, indicating predominantly high-quality candidates while motivating execution-based checks for subtle logical inconsistencies.The distribution supports the teacher model’s effectiveness but shows that language-only evaluation can miss logical errors.

C. Hyperparameter Specification

The reward configuration balances semantic correctness, structural validity, tag usage, verification efficiency, and concise generation. It uses hierarchical penalties and bounded tool and tag costs to discourage pathological behavior while preserving exploration.

  • Correctness vs. Format Balance: W = 3 and α = 1.0 establish a 3:1 correctness-to-structure balance, prioritizing semantic accuracy while integrating natural-language and formal-verification components.The configuration balances hybrid reasoning with correct answers under the new framework.
  • Fatal Error Prevention: γstruct = 3.0 assigns maximum penalties to fatal errors, while βstruct = 1.0 penalizes invalid but recoverable format violations.Fatal errors include repetitive tokens and malformed structures, creating a hierarchy that discourages catastrophic failures while allowing bounded exploration.
  • Tag Usage Regulation: λtag = 0.005 with cap τtag = 200 discourages alternative tags without allowing tag penalties to overwhelm correctness rewards.The regulated vocabulary includes tags such as <code> and <interpreter>.
  • Formal Verification Efficiency: Nmax = 3 and λcall = 0.5 penalize excessive formal-verification calls, while more than 2 × Nmax = 6 calls triggers a fatal error.Most problems can be solved within 4 formal verification steps, and penalties increase beyond the baseline threshold.
  • Length Control: λlen = 0.04, δmax = 10, and a 512-token hard limit constrain verbosity to encourage concise, focused reasoning without sacrificing completeness.The length penalties follow prior work on general reasoners.
  • Model-Based Verifier: CompassVerifier-7B is selected as the model-based verifier because empirical evaluation identifies its balance between accuracy and efficiency across domains beyond mathematics.Manual review found that diverse nonmathematical problems could not be verified through rule-based methods.

D. Training Dynamics and Behavior Analysis

Across 120 optimization steps, FLV-RL training steadily improves composite reward and verification efficiency while producing responses that first shorten and then stabilize in length. These dynamics indicate progress toward structurally sound, semantically correct, efficient reasoning.

  • Training Dynamics and Behavior Analysis: 120 optimization steps: Figure 8 analyzes reward, response length, and formal logic verification efficiency during FLV-RL optimization.The analysis tracks key training dynamics throughout the optimization process.
  • Reward Evolution: -0.45 to -0.1: Composite reward improves steadily across training, balancing structural integrity, semantic correctness, and efficiency.Figure 8a shows consistent progress in the composite reward function.
  • Response Length: 3100 to 2850 tokens, followed by stabilization around 3100-3200 tokens: Response length follows a U-shaped pattern.The initial decrease reflects redundancy reduction, while later stabilization indicates a balance between completeness and conciseness.
  • Formal Logic Verification Efficiency: 2.3 to 1.9 in the first 40 steps: Formal logic verification efficiency improves rapidly before gradually stabilizing.The model learns to generate proofs requiring fewer symbolic interpreter calls.

E. Analysis of Verification Overhead in Mathematical Reasoning

Enforced formal verification can impose cognitive and syntactic overhead that distracts mathematical reasoning from semantic correctness. In the analyzed cube problem, this overhead contributed to an incorrect answer and failed to improve error detection.

  • Failure Case: 27 is the correct smallest perfect cube, but the model instead reaches 81 through flawed reasoning.The task requires finding the smallest perfect cube expressible as the sum of three consecutive integers, with 27 = 8+9+10.
  • Failure Case: The verification framework outputs “DISPROVED,” yet the model rationalizes this result by asserting that 81 works.This demonstrates how mandatory verification can paradoxically reduce error-detection capability.
  • Verification Overhead: Syntactic complexity from z3 constraint formulation distracts from semantic correctness, whereas direct enumeration identifies 33 = 27 = 3 × 9✓.The passage contrasts verification overhead with checking 13 = 1̸ = 3k, 23 = 8̸ = 3k, and 33 = 27 = 3 × 9✓.

F. Analysis of Package Usage Distribution … L. Prompts

Across package usage, conceptual analysis, cross-domain evaluation, economic case studies, and prompt design, FLV-RL shifts reasoning toward symbolic verification while targeting compounding errors and domain-specific failures. The paper also documents baseline errors, data-synthesis choices, and explicit rules for using Python and Z3 during training.

  • F. Analysis of Package Usage Distribution: 62.5% of FLV-RL package usage is Symbolic & Logic, compared with 42.5% for SimpleTIR, indicating a shift toward abstract reasoning.Algorithmic & Search usage falls from 20.2% to 6.5%, while Numerical & Scientific and Domain & Utils remain approximately 21% and 10%, respectively.
  • G. Conceptual Insights: Formal verification counters compounding autoregressive errors by translating each reasoning step into formal constraints and enforcing structural rigor.Verification is most effective for high-rigidity tasks, while flexible post-verification is important for direct numerical computation.
  • H. Model Comparison for Data Synthesis: 68.9% is Claude Sonnet 4.5’s perfect conversion rate on 103 reasoning traces, the highest among the compared data-synthesis models.DeepSeek-R1 generates exploratory traces cost-effectively, while Claude supplies strict formal translation and formatting.
  • I. Cross-Domain Generalization: LegalBench-SARA: FLV-RL outperforms all baselines on LegalBench-SARA, demonstrating generalization of formal verification to US tax-law statutory reasoning.The benchmark requires multi-step deductive inference over legal rules beyond mathematical and scientific domains.
  • J. GPQA Problems: 26.8% is GPQA (Diamond)’s reported inherent error-rate lower bound, motivating caution about evaluating reasoning on flawed questions and answers.Reported flaws include factual errors, missing parameters, and transcription mistakes.
  • K.1. Problem and Baseline Error Analysis: The Qwen 2.5-7B baseline selects “goes from elastic to inelastic” and exhibits semantic mis-mapping, undetected contradictions, and slope–elasticity conflation.The verified analysis instead establishes that elasticity increases when moving northwest along a linear demand curve.
  • K. Case Study: Formal Verification in Economic Reasoning: SMT-based verification corrects economic reasoning through executable semantic grounding, global consistency checks, numerical witnesses, and verified compositional substeps.The solver rejects inconsistent mappings via SAT/UNSAT, supplies satisfying assignments, and yields reusable solver-checkable components.
  • L. Prompts: The prompts assign Python to computation and Z3 to symbolic logical verification, require independently executable code blocks, and limit tool use to cases providing genuine value.The revised process permits Python or Z3 for a combined total of no more than 4 times.
Loading 2601.22642v2…