Repousser les frontières du raisonnement naturel : bénéfice entrelacé de la vérification par logique formelle
Pushing the Boundaries of Natural Reasoning: Interleaved Bonus from Formal-Logic Verification
January 30, 2026
papers.authors: Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, Yike Guo
cs.AI
papers.abstract
Les grands modèles de langage (LLM) démontrent des capacités remarquables, mais leur prédiction stochastique token par token génère des incohérences logiques et du détournement de récompense que les systèmes symboliques formels évitent. Pour combler cet écart, nous introduisons un cadre guidé par la vérification logique formelle qui entrelace dynamiquement la vérification symbolique formelle avec le processus de génération en langue naturelle, fournissant un retour en temps réel pour détecter et rectifier les erreurs au fur et à mesure qu'elles se produisent. Contrairement aux méthodes neuro-symboliques antérieures limitées par une validation passive a posteriori, notre approche pénalise activement les erreurs de raisonnement intermédiaires durant l'enchaînement déductif. Nous opérationnalisons ce cadre via un nouveau pipeline d'entraînement en deux étapes qui synergise un fine-tuning supervisé guidé par vérification logique formelle et une optimisation par politique. Une évaluation approfondie sur six benchmarks couvrant les raisonnements mathématique, logique et général démontre que nos modèles de 7B et 14B paramètres surpassent les meilleures méthodes de référence par des marges moyennes de 10,4 % et 14,2 % respectivement. Ces résultats valident que la vérification formelle peut servir de mécanisme scalable pour repousser significativement les limites de performance du raisonnement avancé des 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.