Position: Logical Soundness is not a Reliable Criterion for Neurosymbolic Fact-Checking with LLMs
Organizations: School of Computer Science, University of Sheffield, United Kingdom
Abstract
As large language models (LLMs) are increasing integrated into fact-checking pipelines, formal logic is often proposed as a rigorous means by which to mitigate bias, errors and hallucinations in these models' outputs. For example, some neurosymbolic systems verify claims by using LLMs to translate natural language into logical formulae and then checking whether the proposed claims are logically sound, i.e. whether they can be validly derived from premises that are verified to be true. We argue that such approaches structurally fail to detect misleading claims due to systematic divergences between conclusions that are logically sound and inferences that humans typically make and accept. Drawing on studies in cognitive science and pragmatics, we present a typology of cases in which logically sound conclusions systematically elicit human inferences that are unsupported by the underlying premises. Consequently, we advocate for a complementary approach: leveraging human-like reasoning tendencies of LLMs as a feature rather than a bug, and using these models to validate the outputs of formal components in neurosymbolic systems against potentially misleading conclusions.
Figures & tables
| Logically Valid Operation Applied to S1 | Conclusion Derived by Applying Operation (Misleading) | What Humans Infer from Conclusion | Cognitive/Pragmatic Basis of Human Inference |
|---|---|---|---|
| Disjunction Introduction ( ) | S2 : “Tariffs for either France or some other European countries will go up 10%.” | S2-I : “It is possible that tariffs for some other European countries will go up 10%.” | Humans interpret disjunctions as a conjunction of default possibilities: i.e. given “A or B”, inferring the possibility that “B” ( Johnson-Laird and Ragni, 2025 ) . |
| Conjunction Introduction ( ) | S3 : “Tariffs for France will go up 10%, and tariffs for France will go up 10%.” | S3-I : “Tariffs will go up 10% twice in a row.” | Humans infer that the repetition refers to two separate events (by the Gricean Maxim of Quantity ( Grice, 1975 ) ), happening sequentially in time (by conjunction buttressing ( Levinson, 2000 ) ). |
| Material Implication (Positive Paradox) ( ) | S4 : “If interest rates do not decrease, tariffs for France will go up 10%.” | S4-I : “If interest rates do decrease, tariffs will not go up 10%.” | Conditional perfection. Humans routinely interpret natural-language conditionals as biconditionals ( Geis and Zwicky, 1971 ; Horn, 2000 ) . |
| Material Implication (Vacuous Truth) ( ) | S5 : “If tariffs for France will not go up 10%, our domestic market will be flooded with French goods.” | S5-I : “If tariffs for France do go up 10%, our domestic market will not be flooded” | As above |
| By Axioms B and T in Modal Logic ( ) | S6 : “It is possible that tariffs for France will go up 10%.” | S6-I : “It is possible that tariffs for France will not go up 10%.” | Humans infer uncertainty from a statement about possibility, by Gricean Maxim of Quality ( Grice, 1975 ; Johnson-Laird and Ragni, 2019 ) |
Automated Fact-Checking
Automated fact-checking detects checkable claims, retrieves evidence, and assesses whether that evidence supports or refutes them.
See all 139 papersWhether LLMs Can Navigate Beliefs and Facts Depends on How You Phrase It
SymDiag: Explainable Diagnosis for LLM Reasoning via Neuro-Symbolic Verification
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.