VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks
Yu Feng, Nathaniel Weir, Kaj Bostrom, Sam Bayless, Darion Cassel, Sapana Chaudhary, Benjamin Kiesl-Reiter, Huzefa Rangwala
2025-11-10
Summary
This paper addresses a key weakness of large language models (LLMs) – while they can seem to reason through problems step-by-step, they often do so with flawed logic, even when arriving at the correct answer.
What's the problem?
LLMs, even when giving correct answers, can't reliably check *how* they got there. This is a big issue, especially when you need to trust the reasoning, like in legal or medical situations. Just getting the right answer isn't enough if the steps to get there are shaky and based on faulty assumptions.
What's the solution?
The researchers developed a method called VeriCoT that breaks down the LLM’s reasoning into formal, logical steps. It then checks if those steps actually make sense using both automated tools and by making sure each step is grounded in facts from the original text, common knowledge, or previous steps in the reasoning. Essentially, it translates the LLM’s thoughts into a language that can be rigorously checked for errors.
Why it matters?
VeriCoT is important because it helps us build more trustworthy AI systems. By identifying flawed reasoning, it allows for improvements to the LLM itself through better training, and also provides a way to assess the reliability of its answers. This is crucial for using LLMs in high-stakes fields where accuracy and sound reasoning are paramount.
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.