SymDiag: ニューロシンボリック検証によるLLM推論の説明可能な診断

要旨

大規模言語モデル（LLM）は、ますますデータ駆動型の推論器として機能しているが、その思考連鎖（Chain-of-Thought, 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.