SymDiag: 신경-기호 검증을 통한 LLM 추론의 설명 가능한 진단

초록

대규모 언어 모델(LLM)은 점차 데이터 기반 추론기로 활용되고 있지만, 최종 답변이 정확하더라도 이들의 사고 사슬(CoT)은 불충실할 수 있다. 기존의 대부분 '검증' 신호는 진단적이지 않다. 답안 일치는 결과만을 관찰하고, LLM-as-judge는 주관적이고 검증 불가능한 비평을 제공하며, 스칼라 보상(예: PRM/RM)은 다단계 유도가 실패하는 지점에 대한 통찰을 거의 제공하지 않는다. 우리는 추론 검증을 구조화된 실패 진단으로 재구성하는 신경-기호 프레임워크인 SymDiag를 제안한다. SymDiag는 자연어 CoT를 기호 제약 조건으로 변환하고 단계별 만족 가능성/함의 검사를 수행하여 (i) 실패 단계를 특정하고 (ii) 반례, 불일치 증인, 누락 전제 지표를 포함한 검증 가능한 진단 증거를 생성한다. 핵심 과제는 겉보기의 '논리 위반'이 실제 추론 결함 또는 신경-기호 변환 잡음으로 인해 발생할 수 있다는 것이다. 따라서 SymDiag는 이중 기호 인코딩 일관성 검사를 통해 번역 오류(TranslationError)와 추론 오류(ReasoningError)를 분리하는 자가 감사기(Self-Auditor)를 통합하여, 부분 관측 가능성 하에서도 강건한 진단을 가능하게 한다. 다양한 수학, 논리, 과학 및 일반 추론 벤치마크에서 SymDiag는 불충실한 추론 탐지를 개선하고, 결과만 사용하는 검증 및 LLM 기반 판정보다 다회차 추론 수정에 훨씬 더 효과적인 피드백을 제공함으로써, 신뢰할 수 있고 확장 가능한 추론 진단을 위한 원칙적 기반을 제시한다.

English

Large language models (LLMs) increasingly serve as data-driven reasoners, yet their chains-of-thought (CoT) can be unfaithful even when final answers are correct. Most existing ``verification'' signals are not diagnostic: answer matching observes only the outcome, LLM-as-judge provides subjective and non-verifiable critiques, and scalar rewards (e.g., PRMs/RMs) offer little insight into where a multi-step derivation fails.We propose SymDiag, a neuro-symbolic framework that reframes reasoning verification as structured failure diagnosis. SymDiag translates natural-language CoT into symbolic constraints and performs step-level satisfiability/entailment checks to (i) localize failing steps and (ii) produce verifiable diagnostic evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators. A central challenge is that apparent ``logic violations'' can be caused either by genuine reasoning defects or by neural-to-symbolic translation noise. SymDiag therefore incorporates a Self-Auditor that disentangles TranslationError from ReasoningError via dual symbolic encodings consistency checks, enabling robust diagnosis under partial observability. Across diverse mathematical, logical, scientific, and general reasoning benchmarks, SymDiag improves detection of unfaithful reasoning and provides substantially more effective feedback for multi-round reasoning repair than outcome-only verification and LLM-based judging, offering a principled foundation for trustworthy and scalable reasoning diagnosis.