Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification
Authors: name: Chuxue Cao, name: Jinluan Yang, name: Haoran Li, name: Kunhao Pan, name: Zijian Zhao, name: Zhengyu Chen, name: Yuchen Tian, name: Lijun Wu, name: Conghui He, name: Sirui Han, name: Yike Guo
Organization: The Hong Kong University of Science and Technology

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.