AI news and explainers at 7 AM weekdays, plus a Sunday weekly at 8Get it in your inbox

METAL LAB

SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification

arXiv:2608.087862026-08-08

A diagnostic system that pinpoints where and why an AI's reasoning chain goes wrong, using logic programs

SymDiag tackles the problem that an LLM's step-by-step reasoning (chain-of-thought) can be logically broken even when the final answer is correct. It translates the natural-language reasoning into two independent Prolog logic programs, checks each step for contradictions or unsupported claims, and uses a self-auditing step to tell apart genuine reasoning errors from mere translation noise. On a manually verified 240-example benchmark spanning math, logic, science, and general reasoning, it detected unfaithful reasoning better and drove more effective iterative repair than existing methods.

METAL LAB explanatory visual

SymDiag's two-stage diagnose-and-repair pipeline

Evidence statusMeasured results reported

  1. Input: LLM's reasoning traceTakes the problem and the LLM-generated step-by-step chain-of-thought plus its final answer.
  2. Dual logic translationConverts the natural-language reasoning into two independent Prolog programs: a formal translation and a stricter critical restatement.
  3. Self-Auditor checkCompares the two translated programs to determine whether an apparent error is a genuine reasoning defect or just translation noise, passing only approved states forward.
  4. Step-level symbolic verificationSWI-Prolog checks each step for contradictions (satisfiability) and whether its claimed conclusion follows from prior steps (entailment), producing pass/fail verdicts with counterexamples or inconsistency evidence.
  5. Evidence-guided repairUses the failing steps and evidence to prompt the LLM to either locally patch that step or globally rewrite the reasoning from that point, repeating over multiple rounds.
An explanatory diagram made by METAL LAB, not a figure supplied by the paper's authors.

What they did

  1. The motivation is that common checks—matching only the final answer, having an LLM 'judge' loosely critique the solution, or giving a single scalar reward score—cannot tell you which specific step in a multi-step derivation actually failed.
  2. SymDiag compiles the natural-language chain-of-thought into two independently generated Prolog logic programs (a formal translation and a stricter 'critical restatement'), then uses the SWI-Prolog solver to check, step by step, whether each step is consistent with what came before and whether its claimed conclusion actually follows (satisfiability and entailment checks).
  3. A separate 'Self-Auditor' step compares the two translated programs to determine whether a detected logic violation is a real reasoning defect or just noise introduced during the natural-language-to-logic translation process.
  4. When a step fails, the system produces concrete evidence—counterexamples, inconsistency witnesses, or missing-premise indicators—and uses this to either patch just that step or rewrite the reasoning from that point onward, repeating this diagnose-and-repair loop.
  5. Evaluation was done on a manually audited set of 240 examples sampled across math (e.g., AIME), logic (AR-LSAT), science (GPQA), and general reasoning (MMLU) benchmarks.
Figure 1. Paradigms for evaluating chain-of-thought (CoT) reasoning. Outcome- and process-level approaches treat verification as scoring, judging only final answers or subjective plausibility. SymDiag introduces a diagnosis-level paradigm, performing symbolic checks to localize reasoning failures and produce verifiable diagnostic evidence, enabling targeted repair.
Figure 1. Paradigms for evaluating chain-of-thought (CoT) reasoning. Outcome- and process-level approaches treat verification as scoring, judging only final answers or subjective plausibility. SymDiag introduces a diagnosis-level paradigm, performing symbolic checks to localize reasoning failures and produce verifiable diagnostic evidence, enabling targeted repair.
Figure 2. SymDiag overview. Stage I (Diagnosis): a neuro-symbolic generator produces (i) a formal translation and (ii) a critical restatement of the original CoT as two independent Prolog programs; a Self-Auditor checks cross-encoding consistency to distinguish TranslationError from ReasoningError, and SWI-Prolog performs step-level satisfiability/consistency checks to output a faithful/unfaithful decision with verifiable evidence (e.g., counterexamples, inconsistency witnesses, missing-premise indicators). Stage II (Repair): SymDiag uses localized failures and evidence to prompt an LLM to generate a repaired reasoning trace that is solver-consistent.
Figure 2. SymDiag overview. Stage I (Diagnosis): a neuro-symbolic generator produces (i) a formal translation and (ii) a critical restatement of the original CoT as two independent Prolog programs; a Self-Auditor checks cross-encoding consistency to distinguish TranslationError from ReasoningError, and SWI-Prolog performs step-level satisfiability/consistency checks to output a faithful/unfaithful decision with verifiable evidence (e.g., counterexamples, inconsistency witnesses, missing-premise indicators). Stage II (Repair): SymDiag uses localized failures and evidence to prompt an LLM to generate a repaired reasoning trace that is solver-consistent.

Findings

  • On the manually verified 240-example benchmark, SymDiag achieved the best overall F1 score (70.7) for detecting unfaithful reasoning across all datasets, outperforming answer matching, LLM-as-judge, and reward-model-based baselines.
  • The performance gap was especially large on logical and general reasoning benchmarks (AR-LSAT, LogiDed, MMLU), where correct final answers were often reached through invalid intermediate steps that the baseline methods failed to catch.
  • In iterative repair experiments, SymDiag produced faster and larger accuracy gains across repair rounds than all baselines; Answer Matching showed minimal improvement, Reward Model and LogicReward gave noisy unlocalized signals, and LLM-as-Judge plateaued quickly after early gains.
  • In an ablation study, removing step-level symbolic verification caused the largest drop in F1, and removing the Self-Auditor also caused a substantial decline because translation artifacts were then misclassified as reasoning errors.
  • With iterative Self-Auditor feedback, the overall error rate dropped from 46.6% and the pass rate rose from 53.4% to 81.4%; translation errors fell from 20.1% to near zero and execution failures fell from 5.5% to below 1% within three rounds.
Figure 3. Core experimental dataset composition. We manually audit 240 instances in total, sampling 30 examples from each dataset across four reasoning domains.
Figure 3. Core experimental dataset composition. We manually audit 240 instances in total, sampling 30 examples from each dataset across four reasoning domains.
Figure 4. Diagnosis-guided reasoning repair curves across datasets. Each subplot reports task accuracy after each repair round (Round 0 is the original answer). SymDiag yields faster and more sustained gains, reflecting the benefit of localized, verifiable error evidence for targeted correction.
Figure 4. Diagnosis-guided reasoning repair curves across datasets. Each subplot reports task accuracy after each repair round (Round 0 is the original answer). SymDiag yields faster and more sustained gains, reflecting the benefit of localized, verifiable error evidence for targeted correction.

Where it can be used

  • Auditing LLM-generated solutions to math, logic, science, or general knowledge questions to catch cases where the answer is right but the reasoning is logically flawed.
  • Building an automated repair loop that decides whether to patch a single step or rewrite an entire reasoning chain when an LLM's answer or reasoning looks suspicious.
  • Analyzing how error types differ across model sizes (e.g., small models making arithmetic mistakes vs. larger models hallucinating rules) to design scale-aware training signals.
Figure 5. Ablation results on overall faithfulness detection (F1).
Figure 5. Ablation results on overall faithfulness detection (F1).
Figure 6. Normalized distribution of reasoning error types identified by SymDiag.
Figure 6. Normalized distribution of reasoning error types identified by SymDiag.

Limits and open work

  • Evaluation is limited to a manually verified set of 240 examples; performance on the full automatically constructed corpus (over 437,000 instances) or in broader real-world deployment settings was not separately reported.
  • The Self-Auditor may not fully handle extremely vague or unstructured natural-language reasoning that is hard to translate into logical form.
  • Diagnosis, error labeling, and feedback generation relied on a strong judge model (GPTOSS-120B); using a smaller judge model (GPTOSS-20B) reduced overall F1 for all methods, indicating dependence on the capability of the underlying judge model.
  • The authors list extending the symbolic backend to stronger or hybrid provers, improving robustness to underspecified language, and training diagnosis-aware reward models as future work that has not yet been carried out.
Figure 7. Progressive reduction of error types in the SymDiag pipeline through iterative Self-Auditor feedback. Translation Errors and Execution Failures are rapidly eliminated, leading to a steady increase in the overall pass rate.
Figure 7. Progressive reduction of error types in the SymDiag pipeline through iterative Self-Auditor feedback. Translation Errors and Execution Failures are rapidly eliminated, leading to a steady increase in the overall pass rate.
Figure 8. Effect of base model scale on overall faithfulness detection F1. Solid bars compare GPTOSS-120B and GPTOSS-20B across three methods; dashed lines indicate Answer Matching and Reward Model baselines. Larger base models consistently improve all methods, and SymDiag maintains the highest F1 under both model scales.
Figure 8. Effect of base model scale on overall faithfulness detection F1. Solid bars compare GPTOSS-120B and GPTOSS-20B across three methods; dashed lines indicate Answer Matching and Reward Model baselines. Larger base models consistently improve all methods, and SymDiag maintains the highest F1 under both model scales.

Why it matters

If a model can be right for the wrong reasons and no one can catch it, that's a serious problem for deploying LLMs in high-stakes settings. This work shows that giving verifiable, localized evidence about failures—rather than just a score or a vague critique—makes iterative correction of reasoning substantially more effective.

Terms in this paper

  • Chain-of-thought (CoT) · the step-by-step reasoning text an LLM writes out before giving a final answer
  • Neuro-symbolic method · an approach combining neural networks (LLMs) with symbolic logic programs (like Prolog) to make reasoning checkable
  • Satisfiability / entailment check · logically verifying whether a set of conditions can all be true together, and whether a claimed conclusion actually follows from the premises
  • Self-Auditor · an internal check that distinguishes whether a detected logic problem is a real reasoning mistake or just an artifact of translating natural language into logic
  • Process reward model (PRM) · a model that scores each intermediate reasoning step, giving only a number rather than an explanation of what went wrong

Original abstract (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.

Authors · Wenyao Cui

Read on arXiv

Latest papers

All papers →

Latest from METAL LAB

Figures: Wenyao Cui et al., arXiv:2608.08786, CC BY 4.0