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

TL;DR

This paper introduces a formal logic verification-guided framework that actively integrates symbolic validation into LLM reasoning, significantly improving their logical consistency and reasoning performance across multiple benchmarks.

Contribution

It presents a novel interleaved verification approach with a two-stage training pipeline, advancing neuro-symbolic methods beyond passive validation.

Findings

7B and 14B models outperform baselines by 10.4% and 14.2%.

Framework effectively detects and corrects reasoning errors in real-time.

Demonstrates scalable improvement in logical and mathematical reasoning.

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.