adu2021 Validate LLM Reasoning Through Logical Consistency Checking
Chain-of-Thought reasoning enables LLMs to decompose complex problems into justifiable steps. However, LLMs cannot reliably verify their own logic—flawed reasoning can produce correct-looking answers, creating false confidence. VeriCoT bridges this gap by combining neural language understanding with formal symbolic verification.
VeriCoT converts each reasoning step into first-order logic, identifies supporting premises from context or prior steps, and uses automated SMT solvers to verify logical validity. This neuro-symbolic approach exposes ungrounded claims, contradictions, and reasoning errors while maintaining human interpretability through natural language premises.
Core Concept
VeriCoT operates as a post-hoc verification system for Chain-of-Thought reasoning. Rather than modifying model architecture or training procedures, it validates completed reasoning traces by:
- Formalizing reasoning - Converting natural language CoT steps into first-order logic (FOL) formulas
- Identifying premises - Extracting grounding sources (context, commonsense, prior steps) that justify each step
- Checking consistency - Using SMT solvers (Z3) to verify logical relationships between steps and premises
- Classifying errors - Categorizing verification failures as ungrounded, contradictory, or untranslatable steps
Architecture Overview
- Autoformalization Module: LLM-driven two-stage translation from natural language to SMT-LIB FOL notation, iteratively extending variable declarations
- Premise Identification: Solicits supporting premises from source context, commonsense knowledge, or preceding reasoning steps
- Symbolic Verification: Z3 SMT solver checks three relationships: entailment (step logically follows), contradiction (step conflicts with facts), consistency (neither follows nor contradicts)
- Error Classification: Categorizes failures and computes verification scores across reasoning traces
- Downstream Integration: Routes verification signals to three enhancement pathways (inference-time reflection, supervised fine-tuning, preference optimization)
Implementation Steps
Step 1: Autoformalization Pipeline
Convert natural language CoT steps to first-order logic formulas. The LLM performs two-stage translation: initial formalization using existing variable declarations, then iterative extension of vocabulary (up to three iterations) if new concepts appear.
# Simplified formalization prompt structure
def formalize_cot_step(step_text, existing_declarations, max_iterations=3):
"""
Convert a reasoning step to FOL using iterative LLM refinement.
Args:
step_text: Natural language reasoning statement
existing_declarations: Prior FOL variable definitions
max_iterations: Max attempts to extend vocabulary
Returns:
smt_lib_formula: FOL formula in SMT-LIB notation
"""
# Iteration 1: Attempt formalization with existing vocabulary
prompt = f"""Given these variable declarations:
{existing_declarations}
Formalize this reasoning step as a first-order logic formula:
"{step_text}"
Respond with SMT-LIB notation."""
formula = llm_call(prompt)
# Iteration 2-3: Extend declarations if needed
iteration = 1
while iteration < max_iterations and "undefined" in formula.lower():
prompt = f"""The formula referenced undefined variables.
Add new declarations and reformalize:
"{step_text}"
Current declarations:
{existing_declarations}"""
existing_declarations += llm_call(prompt)
iteration += 1
return formula
Step 2: Premise Generation
When a step lacks logical support, identify premises from three sources. Filter premises for consistency with established facts before conjunction.
def generate_supporting_premises(step_fol, prior_facts, context_doc):
"""
Identify and filter premises justifying a reasoning step.
Args:
step_fol: FOL formula representing the step
prior_facts: Established facts (FOL formulas)
context_doc: Source document or reasoning context
Returns:
verified_premises: Premises passing consistency filters
"""
# Prompt for candidate premises from three sources
prompt = f"""Step to justify: {step_fol}
Prior facts: {prior_facts}
Context: {context_doc}
Generate candidate premises from:
1. Source context (direct quotes)
2. Commonsense knowledge
3. Prior reasoning steps
Format as FOL formulas."""
candidates = llm_call(prompt)
# Filter candidates for consistency
verified = []
for premise in candidates:
# Check premise doesn't contradict prior facts
if not check_contradiction(premise, prior_facts):
verified.append(premise)
return verified
Step 3: Symbolic Verification
Use Z3 SMT solver to check logical relationships. For each step, verify it either logically follows from premises or is consistent with prior knowledge.
def verify_step_consistency(step_fol, premises, prior_facts):
"""
Check logical consistency between a step and its premises/facts.
Args:
step_fol: The reasoning step in FOL
premises: Supporting premises in FOL
prior_facts: Established facts in FOL
Returns:
verification_result: {entailment, contradiction, consistent, ungrounded}
"""
from z3 import Solver, And, Implies, unsat
solver = Solver()
# Add prior facts as assertions
for fact in prior_facts:
solver.add(fact)
# Add premises as assertions
premises_conj = And(premises) if premises else True
solver.add(premises_conj)
# Check if step is entailed by premises
solver.push()
solver.add(Implies(premises_conj, step_fol))
if solver.check() == unsat:
return "entailment" # Step logically follows
solver.pop()
# Check if step contradicts facts
solver.push()
solver.add(Not(step_fol))
if solver.check() == unsat:
return "contradiction" # Step conflicts with facts
solver.pop()
# Otherwise step is consistent but ungrounded
return "ungrounded"
Step 4: Downstream Integration
Route verification results to enhancement pathways. Inference-time self-reflection prompts the model to correct failed steps; supervised fine-tuning uses verified traces as training data; preference optimization uses verification as reward signal.
def apply_verification_signal(cot_trace, verification_results):
"""
Apply verification outcomes to improve reasoning.
Args:
cot_trace: Original chain-of-thought sequence
verification_results: Per-step verification outcomes
Returns:
enhanced_trace: Improved reasoning with corrections
"""
failed_steps = [i for i, v in enumerate(verification_results)
if v != "entailment"]
if failed_steps:
# Inference-time reflection: prompt model to self-correct
prompt = f"""Your reasoning had issues:
Step {failed_steps[0]}: {cot_trace[failed_steps[0]]}
Verification: {verification_results[failed_steps[0]]}
Please reconsider and provide corrected reasoning."""
corrected = llm_call(prompt)
return corrected
return cot_trace
Practical Guidance
When to Use VeriCoT:
- High-stakes domains (legal, medical, scientific reasoning) requiring verifiable logic
- Tasks with clear logical structures (mathematics, formal proofs, knowledge-base reasoning)
- Situations where source attribution matters (document-grounded reasoning, RAG systems)
When NOT to Use:
- Creative writing or subjective reasoning without formal logic requirements
- Real-time systems requiring immediate inference (verification adds latency)
- Domains where formal FOL cannot capture reasoning nuances (abstract philosophy, poetry)
Hyperparameters and Configuration:
- SMT solver timeout: 5-10 seconds per step (balance thoroughness with latency)
- Premise iteration budget: 2-3 attempts before declaring step ungrounded
- Entailment threshold: Use strict logical entailment (not heuristic similarity) for correctness
Pitfalls to Avoid:
- Over-formalization - Not all reasoning steps translate cleanly to FOL; have fallback interpretations for untranslatable cases
- Premise hallucination - Verify generated premises against actual source documents; don't accept LLM-generated commonsense without validation
- Solver timeout neglect - Set realistic timeouts; unsolved constraints are treated as inconsistent, potentially rejecting valid reasoning
- Ignoring context - FOL formalization loses pragmatic context; maintain natural language premises alongside formal verification
Reference: https://arxiv.org/abs/2511.04662