Source-linked AI summary
SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification
Wenyao Cui, Huaping Zhang, Yongyi Huang, Qiuchi Li, Jian Xu, Cheng-Lin Liu, Chunxiao Gao, Juan Wang, Baohua Zhang
TL;DR
LLM chains-of-thought can contain invalid reasoning despite correct answers, while common verification signals often do not localize failures. SymDiag diagnoses reasoning step by step with symbolic checks and verifiable evidence, and achieves the best faithfulness-detection performance across datasets.
Problem
Existing verification signals often fail to localize or explain invalid intermediate reasoning, including cases where the final answer is correct.
Source: §1 · p. 2Method
Results
SymDiag achieves the best faithfulness-detection performance across all datasets, with an overall F1 score of 70.7, outperforming answer matching, LLM-as-Judge, and reward-based baselines.
Source: §5.1 · p. 6Takeaways & Limitations
Checkable, attributed diagnoses support targeted repair of reasoning failures across domains.
Source: §1 · p. 2, §7 · p. 9Symbolic verification can mistake neural-to-symbolic translation artifacts for genuine reasoning defects unless it separates these sources.
Source: §1 · p. 2, §2.4 · p. 3
Abstract
from arXiv · showhide
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 \textbf{SymDiag}, a neuro-symbolic framework that \textbf{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.
1 Introduction
SymDiag reframes LLM reasoning verification as structured failure diagnosis, combining step-level symbolic checks with self-auditing to localize, attribute, and support repair of reasoning failures.
Introduction
- CoT can contain inconsistent steps, hidden assumptions, or non-entailing transformations even when the final answer is correct, complicating high-stakes deployment.The gap between outcome correctness and process validity is identified as a key deployment barrier.Source: §1 · pp. 1–2
- Answer matching cannot localize derivation failures, LLM judges give subjective critiques, and scalar rewards provide little guidance for targeted repair.These approaches treat verification as scoring rather than explaining where and why reasoning fails.Source: §1 · p. 2, Figure 1 · p. 2
- SymDiag performs step-level symbolic checks to localize failing CoT steps and provide verifiable evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators.Its evidence-grounded diagnosis-and-repair pipeline guides targeted repair and improves multi-round reasoning correction.Source: §1 · p. 2
- Unlike systems that return only a score or corrected trace, SymDiag localizes and attributes failures with checkable evidence to support targeted repair across domains.The paper characterizes SymDiag as a diagnostic system, not simply a better verifier or reasoning reward.Source: §1 · p. 2
- The Self-Auditor uses dual symbolic encodings, cross-branch consistency, and sanity checks to distinguish TranslationError from ReasoningError under partial observability.If an apparent violation disappears under minimal text-consistent reformulations, SymDiag attributes it to translation rather than reasoning.Source: §1 · p. 2
- SymDiag's diagnostic dataset spans mathematics, logical, scientific, and general reasoning, enabling diverse errors to be analyzed within a shared symbolic framework.Examples include AIME, AR-LSAT, GPQA, and MMLU.Source: §1 · p. 2
2 Related Work
The section organizes prior verification by the feedback it produces and argues that existing approaches often lack auditable, step-local failure diagnosis. SymDiag addresses that gap with localized, evidence-backed, self-audited diagnosis.
2.1 Outcome-Only Verification and LLM-as-Judge
2.2 Scalar Rewards and Process Supervision
2.3 Neuro-Symbolic Reasoning and Symbolic Interfaces
- Symbolic systems including Logic-LM [32], LogicReward [53], LINC [31], SymbCoT [52], Aristotle [51], Symbol-LLM [50], and proof-oriented or specialized systems [25] [46] strengthen explicit reasoning but focus on solving or proofs, not diagnosis.The work situates these approaches alongside analyses of LLM inference [3].Source: §2.3 · p. 3
2.4 Formal Verification and Neuro-Symbolic Verification
- SymDiag reframes verification as failure diagnosis, localizing steps, distinguishing translation from reasoning errors, and returning checkable evidence for targeted repair.Prior work includes prover-generated rewards [53], FoVer labels, and Explanation-Refiner feedback [37]; Lean [57] and hybrid provers [17] often need domain libraries, while calculators [9] do not address general logical entailment.Source: §2.4 · p. 3
3 Methodology · 3.1 Problem Setup and Outputs
SymDiag diagnoses LLM reasoning by translating CoT into symbolic constraints, checking steps, localizing failures, and using verifiable evidence to guide repair. It assesses faithfulness of a trace, including cases where the final answer is correct but intermediate reasoning is invalid.
3 Methodology
- SymDiag combines symbolic constraint checking, step-level validation, failure localization, and diagnosis-guided repair, unlike outcome-only checks or natural-language critiques.It is a two-stage neuro-symbolic framework for explainable failure diagnosis and repair.Source: §3 · p. 3
3.1 Problem Setup and Outputs
- Its input is a problem with optional context and an LLM-produced chain of thought consisting of steps and a final answer.SymDiag assesses the faithfulness of the reasoning trace, not only its final answer.Source: §3.1 · p. 3
- For each reasoning step, SymDiag returns a pass-or-fail verdict, identifies failing indices, and assigns error labels from a predefined taxonomy.Source: §3.1 · p. 3
- SymDiag supplies verifiable symbolic evidence, including counterexamples, inconsistency witnesses, and missing-premise indicators.Source: §3.1 · p. 3, Figure 2 · p. 4
- SymDiag can flag a trace with a correct final answer when its intermediate entailments are invalid, a failure answer-based evaluation cannot detect.Source: §3.1 · p. 3
- In diagnosis, two independent Prolog encodings are cross-checked to distinguish TranslationError from ReasoningError, while SWI-Prolog checks steps and returns verifiable evidence.The Self-Auditor checks consistency between the formal translation and a critical restatement of the CoT.Source: Figure 2 · p. 4
- In repair, SymDiag uses localized failures and evidence to prompt an LLM for a repaired reasoning trace that is solver-consistent.Source: Figure 2 · p. 4
3.2 Stage I: Neuro-Symbolic Compilation and Verification
Stage I compiles natural-language chains of thought into symbolic states and verifies them step by step. It uses dual encodings and a Self-Auditor to distinguish translation artifacts from reasoning failures before producing localized, evidence-backed diagnoses.
3.2 Stage I: Neuro-Symbolic Compilation and Verification
- Stage I transforms natural-language chains of thought into symbolic representations and verifies each reasoning step.The stage aims to localize failing steps and generate verifiable evidence for diagnosis.Source: §3.2 · p. 4
3.2.1 Step State Representation.
- Each step state encodes accumulated premises and facts, its intended inference, and relevant constraints, then becomes a solver-executable program fragment.Constraints can include domain restrictions, type constraints, boundary conditions, and task-specific axioms; Prolog is the backend.Source: §3.2.1 · p. 4
3.2.2 Neuro-Symbolic Generator.
- The generator creates independent formal-translation and critical-restatement encodings, then runs deterministic checks for signature consistency, groundability, normalized constraints, and solver compatibility.Formal translation normalizes quantities, units, and equalities or inequalities for math and science, and models quantifiers and scope for logic; critical restatement makes implicit assumptions explicit. Dual encodings reduce single-path translation bias and improve robustness to paraphrase variability.Source: §3.2.2 · p. 4, §3.2.3 · p. 4
3.2.4 Self-Auditor: Translation vs. Reasoning Error Disentanglement.
- The Self-Auditor compares branch facts, constraints, and entailment targets, and uses symbolic sanity tests and minimal canonical rewrites to distinguish translation artifacts from reasoning failures.It flags incompatible branch targets or substantial divergence, and attributes a failure to translation when it disappears under rewrites consistent with the text; only approved states proceed to verification.Source: §3.2.4 · pp. 4–5
3.2.5 Step-Level Symbolic Verification.
- Step verification tests whether premises and constraints are satisfiable and whether prior information entails the step claim; inconsistency or failed entailment marks a step as failed.A satisfiable negation of the step claim yields a counterexample assignment respecting prior premises; the chain is faithful only if every step passes in at least one approved branch, with ties resolved conservatively.Source: §3.2.5 · p. 5
3.2.6 Symbolic Diagnosis: Failure Localization and Evidence.
- For each failing step, symbolic diagnosis provides an error label, evidence, and a scope indicating whether repair should patch that step or rewrite a reasoning prefix or suffix.The diagnosis tuple is generated for each failing step.Source: §3.2.6 · p. 5
3.3 Stage II: Diagnosis-Guided Repair
Stage II turns symbolic diagnoses into actionable feedback and uses that feedback to repair the original reasoning trace. The repair strategy depends on whether the defect is localized or propagates.
3.3 Stage II: Diagnosis-Guided Repair
- For each failing step, SymDiag combines a verbalized error label with checkable evidence in a structured feedback message.Evidence can include counterexample assignments, inconsistency witnesses, or missing-premise indicators.Source: §3.3 · p. 5
- For a localized defect, the model minimally edits the offending step while preserving the surrounding context.Examples include arithmetic or algebra errors and invalid equivalences in one step.Source: §3.3 · p. 5
- When a failure propagates, the model rewrites the reasoning from the earliest failing step onward.Examples include an early missing premise or a type mismatch affecting later steps.Source: §3.3 · p. 5
3.4 Dataset Construction
SymDiag’s diagnostic dataset labels reasoning traces as Faithful or Unfaithful and uses a two-stage pipeline to build a large corpus. Main experiments evaluate on a manually verified, human-audited 240-instance gold set sampled from that corpus.
3.4 Dataset Construction
- Traces are Faithful when the answer is correct and the CoT has no verifiable defect; they are Unfaithful when a clear, locatable defect is present.Examples of defects include missing premises, invalid equivalences, ignored boundary conditions, or flaws leading to an incorrect answer.Source: §3.4 · p. 5
- A two-stage pipeline samples CoTs and answers from base LLMs, directly labels incorrect-answer instances Unfaithful, then uses conservative multi-judge voting to retain high-precision Faithful traces among correct-answer instances.The sampling step is described in Section 4.1.3.Source: §3.4 · p. 5
- The automatically constructed corpus contains 437,792 instances, while the main experiments use a manually verified gold set of 240 instances sampled from it for reliable, human-audited evaluation.The composition figure specifies that 30 examples per dataset were sampled across four reasoning domains.Source: §3.4 · p. 5, Figure 3 · p. 5
4 Experiments
Experiments use a manually audited, four-domain dataset to evaluate faithfulness diagnosis and diagnosis-guided reasoning repair. The setup compares SymDiag with answer-, judge-, reward-, and prover-based signals across several base-model capacities.
4.1 Experiments Setup
- The manually audited diagnostic dataset contains 240 instances across mathematics, logic, science, and general reasoning, each labeled Faithful or Unfaithful.Source: §4.1.1 · p. 5
4.1.1 Datasets.
- Evaluation covers faithfulness detection and feedback effectiveness for iterative reasoning repair, comparing SymDiag with methods using weaker or non-verifiable supervision signals.Source: §4.1.2 · p. 5, §4.1.5 · p. 6
4.1.2 Baselines.
- Baselines include final-answer matching with 1-bit feedback, LLM-as-Judge feedback, a scalar NVIDIA reward model [49], and LogicReward’s scalar signal and Isabelle prover outputs [53].LLM-as-Judge and SymDiag use GPTOSS-120B for fair comparison; LogicReward also uses GPTOSS-120B, while the Reward Model uses Qwen-3-Nemotron-32B-Reward.Source: §4.1.2 · p. 6
- Base reasoners are Llama-3.2-1B [11], Qwen3-1.7B [56], Qwen3-8B [56], and GPTOSS-20B [1]; SymDiag’s diagnosis, attribution, and feedback use GPTOSS-120B [1] unless stated otherwise.Source: §4.1.3 · p. 6
4.1.4 SymDiag Configuration.
- SymDiag translates and critiques each chain of thought into symbolic step records, verifies them step by step, and diagnoses TranslationError versus ReasoningError to localize failures and guide repair.Feedback supports local patching or full-chain rewriting; experiments report single-round and multi-round outcomes, with up to 4 repair rounds by default.Source: §4.1.4 · p. 6
4.1.5 Metrics.
- Faithfulness detection is measured by per-dataset F1, while repair effectiveness is measured after each round with benchmark scores and learning curves for effectiveness and sample efficiency.The detection results are summarized in Table 1 and repair curves in Figure 4; no table or figure passages with result values are supplied here.Source: §4.1.5 · p. 6
5 Results
On a manually audited 240-instance diagnostic dataset, SymDiag detects unfaithful reasoning more effectively than the baselines and provides more effective feedback for iterative reasoning repair.
5.1 Faithfulness Detection Performance
- 70.7 overall F1: SymDiag achieves the best faithfulness-detection performance across datasets, outperforming answer matching, LLM-as-Judge, and reward-based baselines.Gains are especially large on logical and general reasoning benchmarks, where correct answers can conceal invalid intermediate steps.Source: §5.1 · p. 6, Table 1 · p. 7
5.2 Diagnosis-Guided Reasoning Repair
- SymDiag achieves faster, larger repair gains across rounds and the strongest final performance across datasets through localized, verifiable diagnoses.Its feedback targets invalid inferences, missing premises, and constraint violations; answer matching offers minimal improvement, reward signals are scalar and sometimes noisy, and LLM-as-Judge feedback quickly saturates.Source: §5.2 · pp. 6–7, Figure 4 · p. 7
6 Analysis
The analysis finds that SymDiag’s diagnosis gains depend on interacting neuro-symbolic components and that Self-Auditor feedback reduces pipeline errors. It also identifies model-scale-dependent failure profiles and finds that SymDiag retains an advantage when the generator model is scaled down.
6.1 Ablation Study
- Removing any SymDiag component reduces faithfulness-detection F1, with the largest drop when step-level symbolic verification is removed.Removing the Self-Auditor also substantially lowers performance because translation artifacts are more often mistaken for reasoning errors; ablating either translation branch weakens exposure of hidden assumptions and underspecified inferences.Source: Figure 5 · p. 8, §6.1 · p. 8
6.2 Error Attribution Analysis
- SymDiag finds scale-dependent error profiles: small models often make arithmetic errors and omit premises, while GPTOSS-20B shows fewer arithmetic errors but more hallucinated rules and type or entity mismatches.The findings suggest smaller models need constraint enforcement and premise completion, while larger models need safeguards against rule hallucination and overgeneralization.Source: Figure 6 · p. 8, §6.2 · p. 8
6.3 Effectiveness of the Self-Auditor
- By Round 3, Self-Auditor cuts translation errors from 20.1% to near zero and execution failures from 5.5% to below 1%, raising the pass rate from 53.4% to 81.4%.The remaining errors are dominated by logic-level critique failures rather than translation noise.Source: Figure 7 · p. 8, §6.3 · pp. 8–9
6.4 Generator Model Sensitivity
- Scaling the generator from GPTOSS-120B to GPTOSS-20B lowers overall F1 across methods, but SymDiag preserves most of its advantage over purely neural baselines.The figure reports that SymDiag has the highest F1 under both model scales.Source: Figure 8 · p. 9, §6.4 · p. 9
7 Conclusion
SymDiag reframes LLM reasoning verification as explainable failure diagnosis, using step-level symbolic checks and self-auditing to localize and attribute errors; experiments report stronger unfaithful-reasoning detection and repair feedback than outcome- and judge-based baselines.
- SymDiag outperforms outcome-based and judge-based baselines in detecting unfaithful reasoning and gives more effective multi-round repair feedback, especially for smaller models.Source: §7 · p. 9
- SymDiag translates chains-of-thought into symbolic constraints, verifies steps, and uses self-auditing to distinguish translation artifacts from genuine reasoning errors.Source: §7 · p. 9
- Future work targets stronger or hybrid symbolic verifiers, robustness to underspecified language, and diagnosis-aware reward models and supervisors [13] [14] [15].The proposed training direction uses efficient and meta-learning paradigms.Source: §7 · p. 9
A Error Taxonomy
The section defines a domain-agnostic taxonomy of common LLM failure modes across math, logic, science, and general reasoning, including failures caused by translation rather than reasoning.
A Error Taxonomy
- The taxonomy covers premise omission, invalid inference, constraint or boundary neglect, rule misuse, arithmetic or algebra errors, and type or entity mismatches.Source: A Error Taxonomy · p. 11
- TranslationError identifies solver failures attributable to compilation rather than reasoning.Source: A Error Taxonomy · p. 11