Research map / Large language models / Reasoning and chain of thought

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

ICLR 2026 · Large language models › Reasoning and chain of thought · approach: Chain-of-thought training and analysis · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Introduces VeriCoT, a neuro-symbolic checker that autoformalizes each chain-of-thought step into first-order logic (SMT-LIB), grounds it in premises from context or commonsense, and checks entailment with Z3, then uses the signal for self-reflection, SFT, and DPO.

Problem

LLM chain-of-thought can reach correct answers through logically invalid or ungrounded steps, and existing verifiers do not check the logical validity and context grounding of every step in non-math/code domains.

Approach

Autoformalize each CoT step into SMT-LIB first-order logic, generate supporting premises from source context or commonsense when a step is not entailed, check entailment and contradiction with Z3, and use the resulting error types as feedback for self-reflection and as data/reward signals for SFT and DPO.

Key results

• On ProofWriter, VeriCoT reaches 45.2% pass rate and 42.5% VCAR versus 14.8% and 12.3% for Explanation-Refiner.
• Self-reflection raises VeriCoT ProofWriter pass rate from 45.2% to 60.6% (w LLMaj), with average pass-rate gain of about 46% relative.
• DPO on top of verified-CoT SFT raises Qwen2.5-7B ProofWriter pass rate from 23.2% to 27.8% and VCAR from 18.9% to 23.0%.

Surprising findings

• Verifier precision on validated CoTs exceeds raw task accuracy on ProofWriter and BioASQ, so passing verification is a stronger correctness signal than the base answer rate.
• Adding LLM-as-judge premise evaluation gives only marginal gains over verifier-only self-reflection.

Limitations

• Autoformalization and premise generation rely on LLMs, so mistranslations or ill-founded premises can occur.
• Verification proves entailment from inferred premises but cannot guarantee the CoT or premises are true.
• Some reasoning steps cannot be expressed in the supported SMT-LIB fragment and are marked untranslatable.

Experimental setup

Datasets: ProofWriter LegalBench SARA BioASQ

Benchmarks: ProofWriter LegalBench SARA BioASQ

Metrics: verification pass rate verifier precision verified correct answer rate task accuracy

Baselines: Explanation-Refiner Direct SMT Baseline VeriCoT-NoPrem

Builds on: Explanation-Refiner chain-of-thought direct preference optimization SMT-LIB Z3

Closest papers by meaning

• Verifying Chain-of-Thought Reasoning via Its Computational Graph (ICLR 2026 · similarity 0.89)
• Chain of Preference Optimization: Improving Chain-of-Thought Reasoning in LLMs (NeurIPS 2024 · similarity 0.88)
• VeriThinker: Learning to Verify Makes Reasoning Model Efficient (NeurIPS 2025 · similarity 0.88)
• Deep Hidden Cognition Facilitates Reliable Chain-of-Thought Reasoning (AAAI 2026 · similarity 0.88)
• On Learning Verifiers and Implications to Chain-of-Thought Reasoning (NeurIPS 2025 · similarity 0.88)
• Causal Sufficiency and Necessity Improves Chain-of-Thought Reasoning (NeurIPS 2025 · similarity 0.88)