Spingendo i Confini del Ragionamento Naturale: Beneficio Intervallato dalla Verifica Logico-Formale

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

January 30, 2026

Autori: Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, Yike Guo

cs.AI

Abstract

I modelli linguistici di grandi dimensioni (LLM) mostrano capacità notevoli, ma la loro predizione stocastica token-per-token genera incoerenze logiche e fenomeni di reward hacking che i sistemi simbolici formali evitano. Per colmare questa lacuna, introduciamo un framework guidato dalla verifica logica formale che intercala dinamicamente la verifica simbolica formale con il processo di generazione del linguaggio naturale, fornendo un feedback in tempo reale per rilevare e correggere gli errori man mano che si verificano. A differenza dei precedenti metodi neuro-simbolici limitati da una validazione passiva a posteriori, il nostro approccio penalizza attivamente le fallacie intermedie durante la catena di ragionamento. Implementiamo questo framework attraverso una innovativa pipeline di addestramento in due fasi che sinergizza un fine-tuning supervisionato guidato dalla verifica logica formale e un'ottimizzazione tramite policy. Una valutazione estesa su sei benchmark che coprono il ragionamento matematico, logico e generico dimostra che i nostri modelli da 7B e 14B superano i baseline all'avanguardia con margini medi rispettivamente del 10,4% e del 14,2%. Questi risultati convalidano che la verifica formale può fungere da meccanismo scalabile per spingere significativamente i limiti prestazionali del ragionamento avanzato degli LLM.

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.