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

TL;DR

This work tackles the mismatch between probabilistic natural-language reasoning and formal logical validity in large language models by introducing a formal-logic verification-guided framework that interleaves symbolic checks during generation. It employs a two-stage training pipeline—formal-logic guided supervised fine-tuning with a hierarchical data synthesis and execution-based validation, followed by reinforcement learning with a multi-dimensional reward (GRPO)—to enforce structural integrity and logical correctness across multiple reasoning domains. Evaluations on six benchmarks show that FLV improves state-of-the-art performance for 7B and 14B models by substantial margins, demonstrating the scalability and robustness of verifier-guided reasoning across logical, mathematical, and general tasks. The approach advances trustworthy AI by providing interpretable, step-level correctness guarantees and highlighting a practical trade-off between computation and reasoning fidelity, with potential implications for real-world problem solving and safety-critical applications.

Abstract

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.

Figures (9)

• Figure 1: Comparison between natural language reasoning and formal logic verification-guided reasoning. Formal verification detects logical errors in natural language reasoning and provides corrected reasoning paths. "NL" means Natural Language.
• Figure 2: Number of correct answers using natural language reasoning versus formal logic verification. We randomly sampled 500 instances from each domain for this comparison.
• Figure 3: Overview of the formal logic verification-guided training framework. The framework operates in two stages: (1) SFT: A teacher model synthesizes formal logic verification traces, which are validated by a verifier. A subset of verified samples is used to fine-tune the model, while challenging samples are reserved for RL training. (2) RL: The policy model generates natural language reasoning followed by formal reasoning. A formal interpreter verifies the formal reasoning and provides feedback, enabling iterative refinement until the model produces a final answer or reaches the maximum number of interpreter calls. Rewards computed from verification outcomes are used to calculate advantages and update the policy model via reinforcement learning.
• Figure 4: Python packages type distribution invoked by SimpleTIR (blue) vs. FLV-RL (red) across three domains.
• Figure 5: Token length distribution comparison across General-Reasoner, SimpleTIR, and FLV-RL. The box plots illustrate the median token usage (center line) and interquartile ranges.