VERICOT: Formal Verification of LLM Reasoning Chains

Large language models can reach correct answers through flawed reasoning. This article discusses VERICOT (Neuro-Symbolic Chain-of-Thought Validation via Logical Consistency Checks), a framework that verifies each step of a chain-of-thought (CoT) reasoning process using formal logic, making hidden assumptions explicit and checkable by automated solvers.

Key points

• The problem: LLMs are next-token predictors without explicit mechanisms for checking logical validity. A model may derive a correct conclusion (e.g., a welfare eligibility ruling) via an intermediate step containing a factual error (e.g., "Charlie is at most 15" when the premises imply at most 18). In law, medicine, and science, such silent flaws undermine trust.
• Core idea: Convert each natural-language reasoning step into a first-order logic fragment of SMT-LIB (linear arithmetic, uninterpreted functions, quantifiers) and verify it objectively with an SMT solver such as Z3.

The four-stage verification pipeline

For each CoT step, VERICOT applies layered checks:

1. Translation: Can the step be converted into a logical formula? If not → labeled *untranslatable*. 2. Contradiction check: Does the formula conflict with the knowledge base? If yes → *contradiction*. 3. Entailment check: Is the formula implied by existing knowledge? If yes → step passes. 4. Premise generation: Otherwise, the LLM proposes candidate supporting premises from context, documents, or commonsense; candidates are checked for consistency and sufficiency (their conjunction must entail the step), and optionally audited by an LLM-as-Judge against source text. If no valid premise is found → *ungrounded*.

Auto-formalization is iterative: when the existing vocabulary lacks a predicate (e.g., age), the LLM dynamically extends it via declare-fun/declare-const statements, then re-translates.

The LLM-as-Judge audit achieved reported acceptance rates of 93.5% for document-based premises and 83.9% for commonsense premises, filtering unreliable assumptions.

Experimental results

Evaluated across three domains:

| Dataset | Verification pass rate | Verification precision | VCAR | Task accuracy | |---|---|---|---|---| | ProofWriter | 45.2% | 94.1% | 42.5% | 75.8% | | BioASQ | 25.3% | 84.3% | 21.3% | 81.4% | | LegalBench-SARA | 15.2% | 87.0% | 13.2% | 80.0% |

Key insights:

• Verification precision systematically exceeds raw task accuracy — CoTs that pass VERICOT are more trustworthy than the model's unfiltered answers.
• Ungrounded errors dominate failure cases, confirming LLMs' tendency to over-generalize and assert unstated assumptions. Contradiction and untranslatable errors are less common.
• Self-reflection: feeding error types, formulas, and premises back to the model improved pass rates by +12.3% absolute (+46.4% relative) and VCAR by +9.5% absolute, while precision stayed near 90%.
• Data distillation: using VERICOT-verified CoTs for SFT improved task accuracy, and adding DPO with verification signals as rewards raised Qwen2.5-7B's pass rate from 22.8% to 26.8% — valuable where gold labels are unavailable.

Limitations

• Expressiveness: cannot formalize probabilistic statements, vagueness ("approximately"), or complex temporal logic.
• Translation risk: the LLM may mistranslate a statement into a non-equivalent formula; VERICOT validates logical form, not the truth of premises themselves.
• Knowledge dependence: fails when required facts or commonsense rules are absent from context or knowledge bases.

Broader implications

VERICOT embodies a neuro-symbolic design philosophy: the LLM handles generation, translation, and hypothesis extraction, while the symbolic solver provides objective consistency and entailment checks. For high-stakes applications, the recommendation is to treat verification pass rate as a first-class metric alongside answer accuracy, design explicit self-reflection loops with fine-grained logical feedback, and target each error type (ungrounded → better premise extraction; contradiction → better context understanding; untranslatable → broader logic support). Open questions include probabilistic reasoning, dynamic commonsense knowledge bases, multilingual formalization, and integration with reasoning models like OpenAI o1.

References

1. Wei, J., et al. (2022). Chain-of-Thought Prompting Elicits Reasoning in Large Language Models. *arXiv preprint*. 2. Quan, T. M., Petersen, B. B., & Desai, M. (2024b). Explanation-Refiner: Iterative Refinement of LLM Explanations via Theorem Prover Guidance. *NeurIPS*. 3. de Moura, L., & Bjørner, N. (2008). Z3: An Efficient SMT Solver. *TACAS 2008*. 4. Tafjord, O., Herzig, J., & Thawani, A. (2021). ProofWriter: Generating Proofs from Reasoning over Paragraphs. *EMNLP*. 5. Holzenberger, N., Tenney, I., & Pavlick, E. (2020). An Evaluation Dataset for Recognizing Entailed Clauses in Insurance Contracts. *ACL 2020 Workshop*.