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
cs.AI
2026-08-10
SymDiag turns LLM reasoning chains into Prolog and runs step-level checks to localize which step fails, separating translation from reasoning errors. It reaches 70.7 overall F1, above answer matching and reward models.
LLMs are increasingly used as data-driven reasoners, but their chains-of-thought can be unfaithful: the final answer is right while the intermediate steps are invalid. Existing verification does not diagnose where it breaks. Answer matching looks only at the outcome. LLM-as-judge gives subjective, non-verifiable critiques. Scalar reward models (PRM/RM) return a single score with no pointer to the failing step. Even when a problem is detected, nothing tells you which step to fix.
SymDiag reframes this as structured failure diagnosis.
SymDiag has two stages.
Stage I compiles the natural-language chain into an executable symbolic program. Each step Si is split into three parts: accumulated premises and derived facts Pi, the intended inference Ii, and constraints Ci (domain restrictions, type constraints, axioms). The program runs in SWI-Prolog.
A key design choice is a dual-branch symbolic generator. The formal translation branch compiles natural language into formal representation, normalizing quantities, units, and equalities. The critical restatement branch re-expresses the chain as stricter, explicitly scoped statements to surface hidden assumptions. Each branch produces an independent Prolog program. Why two? An apparent logic violation can come from a genuine reasoning defect or from neural-to-symbolic translation noise. A single encoding conflates the two.
The Self-Auditor resolves this. It runs a translation consistency check (comparing the fact sets and constraints of the two programs) and a lightweight logical critique check (immediate contradictions, type mismatches), then outputs a binary attribution: translation error or reasoning error.
After attribution, step-level symbolic verification runs two tests: a satisfiability check for whether the step introduces inconsistency (SAT of Pi and Ci), and a local entailment check for whether prior premises support the current claim, operationalized as the unsatisfiability of premises plus the negated claim. If either fails, the step is flagged unfaithful. The diagnosis is a tuple of error label, verifiable evidence (counterexamples, unsat cores, missing-premise indicators), and repair scope.
Stage II turns the diagnosis into repair feedback: a local patch for isolated defects, a global rewrite for propagating failures such as a missing premise that breaks several steps.
| Verifier | Overall F1 |
| Answer Matching | 57.7 |
| Reward Model | 57.0 |
| LLM-as-Judge (large-model tier) | 62.8 |
| SymDiag | 70.7 |
SymDiag posts the highest overall F1 across eight datasets (AIME24/25, MATH, AR-LSAT, LogiDed, GPQA, MMLU, MMLU-Pro), with the largest gains on logical and general reasoning (AR-LSAT, LogiDed, MMLU), where correct answers most often come through invalid steps. This is measured on a 240-instance manually audited set, drawn from an automatically constructed corpus of 437,792.
For multi-round repair, SymDiag shows the steepest and most sustained gains. Answer matching barely moves (no localization signal). Reward models give scalar scores that cannot be pinpointed. LLM-as-judge helps early then saturates because its feedback is coarse and non-verifiable.
The Self-Auditor itself works: before auditing, total error rate is 46.6% with translation errors at 20.1%. After three rounds, translation errors drop to near zero, execution failures fall from 5.5% to below 1%, and the pass rate rises from 53.4% to 81.4%. Remaining errors are dominated by irreducible logic-level critique failures, not translation noise.
For anyone working on reasoning reliability, this is a move from scoring to localization with evidence. The output is not "this reasoning is bad" but "step 3 fails, here is a counterexample proving it." That verifiable evidence is directly actionable for automated repair and multi-round self-correction, which scalar rewards cannot supply.
The fit is domain-bound: it depends on compiling reasoning into Prolog-executable symbolic form, so it suits math, logic, and constraint-heavy domains. Open-domain commonsense reasoning is hard to symbolize.
The authors note that the symbolic backend is Prolog, not heavier proof assistants like Lean or Coq that require domain-specific formal libraries, so the range of reasoning types is bounded by Prolog's expressiveness. The 240-instance audited set is small even though sampled from a 437,792-instance corpus. The dual-encoding consistency approach handles natural-language ambiguity but is not perfect.
A concern the text leaves open: the headline F1 is on the 240-instance audited subset, chosen for trustworthy evaluation, but a small-sample F1 carries real variance, and the full-corpus automated numbers are not given in the main text as a comparison. The reasoning backbones are GPTOSS-120B and GPTOSS-20B, whose generality warrants independent confirmation.