Expandindo os Limites do Raciocínio Natural: Benefício Intercalado da Verificação 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

Resumo

Os Grandes Modelos de Linguagem (LLMs) demonstram capacidades notáveis, mas a sua previsão estocástica do próximo token cria inconsistências lógicas e manipulação de recompensas que os sistemas simbólicos formais evitam. Para colmatar esta lacuna, introduzimos uma estrutura orientada pela verificação de lógica formal que intercala dinamicamente a verificação simbólica formal com o processo de geração de linguagem natural, fornecendo feedback em tempo real para detetar e retificar erros à medida que ocorrem. Distinguindo-se de métodos neuro-simbólicos anteriores limitados pela validação passiva a posteriori, a nossa abordagem penaliza ativamente falácias intermédias durante a cadeia de raciocínio. Operacionalizamos esta estrutura através de um pipeline de treino inovador em duas fases que sinergiza o ajuste fino supervisionado orientado por verificação de lógica formal e a otimização de políticas. A avaliação extensiva em seis benchmarks abrangendo raciocínio matemático, lógico e geral demonstra que os nossos modelos de 7B e 14B superam os melhores baselines existentes por margens médias de 10,4% e 14,2%, respetivamente. Estes resultados validam que a verificação formal pode servir como um mecanismo escalável para expandir significativamente os limites de desempenho do raciocínio avançado em LLMs.

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.