SymDiag：以神經符號驗證實現可解釋的大型語言模型推理診斷

摘要

大型語言模型（LLM）日益成為資料驅動的推理器，但其思維鏈（CoT）即使最終答案正確，也可能不忠實。現有的大多數「驗證」訊號不具診斷性：答案比對僅觀察結果；以LLM作為評判提供主觀且不可驗證的評論；標量獎勵（如PRM/RM）對多步驟推導的失敗位置提供的洞察有限。我們提出SymDiag，一個神經符號框架，將推理驗證重新建構為結構化失敗診斷。SymDiag將自然語言CoT轉換為符號約束，並執行步驟層級的滿足性/蘊涵檢查，以（i）定位失敗步驟，並（ii）產生可驗證的診斷證據，包括反例、不一致性見證和缺失前提指標。一個核心挑戰是：明顯的「邏輯違反」可能源自真正的推理缺陷，也可能源於神經到符號的翻譯噪聲。因此，SymDiag納入一個自審查器，透過雙重符號編碼一致性檢查，區分翻譯錯誤與推理錯誤，從而在部分可觀測性下實現穩健的診斷。在涵蓋數學、邏輯、科學及一般推理的多樣化基準上，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.