Search papers, labs, and topics across Lattice.
This paper introduces SymDiag, a neuro-symbolic framework that enhances the verification of large language model (LLM) reasoning by translating natural-language chains-of-thought into symbolic constraints for structured failure diagnosis. The method addresses the limitations of existing verification techniques by providing detailed diagnostic evidence, such as counterexamples and missing-premise indicators, while effectively distinguishing between translation errors and genuine reasoning defects. Experimental results demonstrate that SymDiag significantly improves the detection of unfaithful reasoning and offers more actionable feedback for multi-round reasoning repair compared to traditional verification methods.
SymDiag reveals that existing verification methods fail to diagnose reasoning errors effectively, providing a robust framework that localizes failures and generates actionable insights.
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.