Расширяя границы естественных рассуждений: преимущества чередующейся верификации средствами формальной логики

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

January 30, 2026

Авторы: Chuxue Cao, Jinluan Yang, Haoran Li, Kunhao Pan, Zijian Zhao, Zhengyu Chen, Yuchen Tian, Lijun Wu, Conghui He, Sirui Han, Yike Guo

cs.AI

Аннотация

Крупные языковые модели (LLM) демонстрируют впечатляющие возможности, однако их стохастическое предсказание следующей лексемы порождает логические противоречия и взлом системы вознаграждений, которых избегают формальные символьные системы. Для преодоления этого разрыва мы представляем фреймворк, управляемый верификацией формальной логики, который динамически чередует формальную символьную верификацию с процессом генерации естественного языка, обеспечивая обратную связь в реальном времени для обнаружения и исправления ошибок по мере их возникновения. В отличие от предыдущих нейро-символьных методов, ограниченных пассивной апостериорной валидацией, наш подход активно штрафует промежуточные заблуждения в цепи рассуждений. Мы реализуем этот фреймворк с помощью нового двухэтапного конвейера обучения, который объединяет контролируемую тонкую настройку под руководством верификации формальной логики и оптимизацию политики. Обширная оценка на шести тестовых наборах, охватывающих математические, логические и общерассудительные задачи, показывает, что наши модели с 7 и 14 миллиардами параметров превосходят современные базовые уровни в среднем на 10,4% и 14,2% соответственно. Эти результаты подтверждают, что формальная верификация может служить масштабируемым механизмом для значительного расширения границ производительности передовых систем логического вывода 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.