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

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.

Large language models can tackle complex problems, but they produce outputs through statistical prediction rather than rigorous logical reasoning, often introducing subtle errors even when the final answer seems correct. We found that nearly 40% of reasoning steps in apparently correct solutions are formally invalid, meaning these models can reach the right answer for entirely the wrong reasons. To address this, we built a framework that pairs natural language reasoning with formal logic solvers, programs capable of mathematically verifying each claim with certainty. Rather than checking for errors only after a solution is complete, our system validates each reasoning step as it is generated and provides immediate feedback, enabling real-time self-correction. We train models in two stages: supervised learning on verified examples, followed by reinforcement learning that rewards logically sound reasoning. Our 7B and 14B models outperform the best existing systems by over 10% across six benchmarks in mathematics, logic, and scientific reasoning, showing that grounding AI in formal verification is a scalable and practical path toward more trustworthy AI.