Het Verleggen van de Grenzen van Natuurlijk Redeneren: Geïnterlinieerd Voordeel uit Formeel-Logische Verificatie
Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification
January 30, 2026
Auteurs: Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, Yike Guo
cs.AI
Samenvatting
Grote Taalmodellen (LLM's) vertonen opmerkelijke capaciteiten, maar hun stochastische voorspelling van volgende tokens veroorzaakt logische inconsistenties en 'reward hacking' die formele symbolische systemen vermijden. Om deze kloof te overbruggen, introduceren we een raamwerk geleid door formele logische verificatie dat dynamisch formele symbolische verificatie verweeft met het natuurlijke-taalgeneratieproces, waarbij het realtime feedback verschaft om fouten te detecteren en te herstellen zodra deze optreden. In tegenstelling tot eerdere neuro-symbolische methoden die beperkt worden door passieve achteraf-validatie, bestraft onze aanpak actief tussenliggende denkfouten tijdens de redeneerketen. We operationaliseren dit raamwerk via een nieuwe tweefasige trainingspijplijn die supervised fine-tuning en policy-optimalisatie synergistisch combineert onder begeleiding van formele logische verificatie. Uitgebreide evaluatie op zes benchmarks voor wiskundig, logisch en algemeen redeneren toont aan dat onze 7B- en 14B-modellen state-of-the-art-baselines gemiddeld verslaan met respectievelijk 10,4% en 14,2%. Deze resultaten valideren dat formele verificatie kan dienen als een schaalbaar mechanisme om de prestatiegrenzen van geavanceerd LLM-redeneren aanzienlijk te verleggen.
English
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.