VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks

TL;DR

VeriCoT tackles the unreliability of chain-of-thought reasoning by constructing a neuro-symbolic verifier that autoformalizes each CoT step into first-order logic and grounds it in NL context and commonsense premises. Using an SMT-based checker, it assesses entailment, consistency, and grounding, outputting verifiable Premises $\mathcal{P}$ and steps $F_i$, or error signals for ungrounded, contradictory, or untranslatable steps. Empirical results on ProofWriter, LegalBench (SARA), and BioASQ show VeriCoT enhances detection of flawed reasoning and provides a strong prediction of final answer correctness; its verification signals also drive inference-time self-reflection and improve downstream task performance via supervised fine-tuning (SFT) and preference fine-tuning (PFT with DPO). The approach yields higher verification coverage and reliability than baselines, enabling more transparent, verifiable reasoning in high-stakes domains. Overall, VeriCoT offers a principled path to trustworthy CoT by marrying symbolic validation with learned grounding from context and commonsense.

Abstract

LLMs can perform multi-step reasoning through Chain-of-Thought (CoT), but they cannot reliably verify their own logic. Even when they reach correct answers, the underlying reasoning may be flawed, undermining trust in high-stakes scenarios. To mitigate this issue, we introduce VeriCoT, a neuro-symbolic method that extracts and verifies formal logical arguments from CoT reasoning. VeriCoT formalizes each CoT reasoning step into first-order logic and identifies premises that ground the argument in source context, commonsense knowledge, or prior reasoning steps. The symbolic representation enables automated solvers to verify logical validity while the NL premises allow humans and systems to identify ungrounded or fallacious reasoning steps. Experiments on the ProofWriter, LegalBench, and BioASQ datasets show VeriCoT effectively identifies flawed reasoning, and serves as a strong predictor of final answer correctness. We also leverage VeriCoT's verification signal for (1) inference-time self-reflection, (2) supervised fine-tuning (SFT) on VeriCoT-distilled datasets and (3) preference fine-tuning (PFT) with direct preference optimization (DPO) using verification-based pairwise rewards, further improving reasoning validity and accuracy.

Figures (5)

• Figure 1: VeriCoT verification of a Chain-of-Thought for the SARA dataset holzenberger2020datasetstatutoryreasoningtax. Even if the final answer is correct, a CoT that contains an invalid step hurts user trust and raises questions of LLM faithfulness. As shown in §\ref{['sec:example-verification']}, VeriCoT autoformalizes each step of the CoT into symbolic logic, producing a formula that ensures each one follows logically from a distilled list of NL premises, each of which it annotates with their source type (e.g. Commonsense or Context) If the CoT cannot be represented this way, it is unverifiable.
• Figure 2: Proportional distribution of outcome scenarios before and after self-reflection (§\ref{['exp:inference']}) under VeriCoT. Categories include successful verification (Valid) and failure cases: Contradiction, Ungrounded, Untranslatable as described in §\ref{['Failure_reasons']}. Self-reflection significantly reduce errors.
• Figure 3: Highlights of an ungrounded example from Proofwriter before self-reflection.
• Figure 4: Highlights of a contradiction example from BioASQ before self-reflection.
• Figure 5: Highlights of an untranslatable example from LegalBench-SARA before self-reflection.