Saved in:
| Main Authors: | , , , , , , , , , , |
|---|---|
| Format: | Preprint |
| Published: |
2026
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2601.22642 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912862192009216 |
|---|---|
| author | Cao, Chuxue Yang, Jinluan Li, Haoran Pan, Kunhao Zhao, Zijian Chen, Zhengyu Tian, Yuchen Wu, Lijun He, Conghui Han, Sirui Guo, Yike |
| author_facet | Cao, Chuxue Yang, Jinluan Li, Haoran Pan, Kunhao Zhao, Zijian Chen, Zhengyu Tian, Yuchen Wu, Lijun He, Conghui Han, Sirui Guo, Yike |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2601_22642 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification Cao, Chuxue Yang, Jinluan Li, Haoran Pan, Kunhao Zhao, Zijian Chen, Zhengyu Tian, Yuchen Wu, Lijun He, Conghui Han, Sirui Guo, Yike Machine Learning 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. |
| title | Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification |
| topic | Machine Learning |
| url | https://arxiv.org/abs/2601.22642 |