자연적 추론의 경계 확장: 형식 논리 검증에서 얻는 상호작용적 보너스

초록

대규모 언어 모델(LLM)은 놀라운 능력을 보여주지만, 확률적 다음 토큰 예측 방식으로 인해 형식적符号 시스템이 회피하는 논리적 불일치와 보장 해킹 문제가 발생합니다. 이러한 격차를 해소하기 위해 우리는 형식 논리 검증을 자연어 생성 과정에 동적으로 연계하여 오류 발생 시 실시간으로 탐지 및 수정하는 피드백을 제공하는 형식 논리 검증 주도 프레임워크를 제안합니다. 수동적 사후 검증에 제한됐던 기존 신경-符号 접근법과 차별화되게, 우리의 방법은 추론 과정에서 발생하는 중간 오류를 능동적으로 제재합니다. 우리는 형식 논리 검증 기반 지도 미세 조정과 정책 최적화를 결합한 새로운 2단계 학습 파이프라인을 통해 이 프레임워크를 구현했습니다. 수학적, 논리적, 일반 추론 영역을 아우르는 6개 벤치마크에서 진행한 폭넓은 평가 결과, 우리의 7B 및 14B 모델이 각각 평균 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.

자연적 추론의 경계 확장: 형식 논리 검증에서 얻는 상호작용적 보너스

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

초록

Support