Empujando los Límites del Razonamiento Natural: Beneficio Intercalado de la Verificación Lógico-Formal

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

January 30, 2026

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

cs.AI

Resumen

Los Modelos de Lenguaje a Gran Escala (LLM) muestran capacidades notables, pero su predicción estocástica del siguiente token genera inconsistencias lógicas y hackeo de recompensas que los sistemas simbólicos formales evitan. Para cerrar esta brecha, presentamos un marco guiado por verificación lógica formal que intercala dinámicamente la verificación simbólica formal con el proceso de generación de lenguaje natural, proporcionando retroalimentación en tiempo real para detectar y rectificar errores conforme ocurren. A diferencia de métodos neuro-simbólicos previos limitados por validación pasiva a posteriori, nuestro enfoque penaliza activamente las falacias intermedias durante la cadena de razonamiento. Operacionalizamos este marco mediante una novedosa canalización de entrenamiento en dos etapas que sinergiza el ajuste fino supervisado guiado por verificación lógica formal y la optimización de políticas. La evaluación exhaustiva en seis benchmarks que abarcan razonamiento matemático, lógico y general demuestra que nuestros modelos de 7B y 14B superan a los mejores baselines actuales por márgenes promedio de 10.4% y 14.2%, respectivamente. Estos resultados validan que la verificación formal puede servir como mecanismo escalable para ampliar significativamente los límites de rendimiento del razonamiento avanzado en 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.