PaperlayerView exact revision on arXiv

Source-linked AI summary

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless

arXiv:2601.20055v2cs.CLcs.AI

TL;DR

LLMs lack reliable logical correctness guarantees for high-stakes reasoning. VERGE combines claim-level formalization, SMT verification, semantic routing, consensus checking, and MCS-guided iterative refinement; it reports broad benchmark gains and convergence, while remaining constrained by latency, model scale, and decidable-logic coverage.

  • Problem

    LLM reasoning relies on statistical likelihood rather than logical deduction, leaving generated answers vulnerable to hallucinations and contradictions in high-stakes domains.

  • Method

    VERGE decomposes answers into atomic claims, verifies logic-amenable claims with SMT, routes other claims to soft verification, and refines answers using structured feedback and aggregate scoring.

  • Results

    VERGE consistently outperforms standard prompting and existing neurosymbolic baselines on 5 of 6 evaluated benchmarks, including GPT-OSS-120B HLE improvement from 14.2% CoT to 30.5%.

  • Takeaways & Limitations

    VERGE provides formal guarantees for verifiable claims while retaining soft consensus verification for ambiguous reasoning, supporting convergence across evaluated datasets.

  • Takeaways & Limitations

    VERGE has substantial latency, requires capable frontier models for full semantic verification, and cannot formally verify claims outside its decidable logic fragments.

Abstract

from arXiv · show

Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. Our approach decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. We introduce three key innovations: (1) multi-model consensus via formal semantic equivalence checking to ensure logic-level alignment between candidates, eliminating the syntactic bias of surface-form metrics, (2) semantic routing that directs different claim types to appropriate verification strategies: symbolic solvers for logical claims and LLM ensembles for commonsense reasoning, and (3) precise logical error localization via Minimal Correction Subsets (MCS), which pinpoint the exact subset of claims to revise, transforming binary failure signals into actionable feedback. Our framework classifies claims by their logical status and aggregates multiple verification signals into a unified score with variance-based penalty. The system iteratively refines answers using structured feedback until acceptance criteria are met or convergence is achieved. This hybrid approach delivers formal guarantees where possible and consensus verification elsewhere, advancing trustworthy AI. With the GPT-OSS-120B model, VERGE demonstrates an average performance uplift of 18.7% at convergence across a set of reasoning benchmarks compared to single-pass approaches.

1 Introduction

VERGE addresses the gap between fluent LLM generation and provable correctness by combining SMT-based formal verification with semantic routing and iterative refinement. Its consensus and MCS mechanisms align candidate logic and turn detected inconsistencies into targeted revisions.

  • Motivation: LLMs remain prone to hallucinations and internal contradictions because statistical likelihood maximization does not provide provable correctness.This matters in high-stakes domains including legal policy compliance, healthcare, and finance.
  • Framework: VERGE combines LLMs with SMT solvers to produce verification-guided answers with formal guarantees for logical and mathematical claims.The framework applies iterative refinement rather than relying only on a single generated answer.
  • Framework: Semantic routing applies formal verification to mathematical and logical claims while using consensus-based verification for commonsense and vague claims.This hybrid design preserves formal guarantees for a verifiable subset while handling broader reasoning tasks.
  • Innovations: Formal semantic equivalence checking makes multi-model consensus logic-level rather than surface-form based, while MCS identifies specific claims requiring revision.The framework uses these mechanisms to avoid syntactic bias and replace generic failure signals with actionable feedback.

2 Related Work

Prior approaches provide probabilistic confidence, self-critique, or consensus but not logical soundness guarantees. VERGE extends neuro-symbolic reasoning with MCS-based natural-language repair feedback for iterative LLM refinement.

  • Probabilistic verification: Self-consistency, process supervision, and self-refinement offer heuristic verification, while multi-agent debate establishes consensus without implying correctness.Self-refinement can also fail because model reasoning may not match its output.
  • Neuro-symbolic integration: Neuro-symbolic approaches connect language with logical forms and theorem proving, but existing methods can require expensive supervision or symbolic augmentation.These efforts motivate combining language models with formal solvers while addressing the semantic gap.
  • Automated repair: VERGE adapts Minimal Correction Subsets from constraint programming to identify constraints whose removal restores satisfiability.Its greedy approximation prioritizes interpretability and convergence speed over theoretical optimality.
  • Automated repair: VERGE translates MCS outputs into natural-language feedback that guides the LLM to rewrite specific atomic claims.This converts abstract unsatisfiable cores into actionable guidance for iterative reasoning repair.

3 Methodology

VERGE decomposes answers into typed atomic claims, formalizes logic-amenable claims for SMT verification, routes unsuitable claims to soft or hybrid verification, and iteratively refines answers using structured feedback and aggregate scoring.

  • Problem formulation: The system seeks a refined answer maximizing verification score while requiring consistency with, and entailment by, the formalized context.Consistency checks satisfiability of the context with each claim; entailment checks that the context cannot satisfy the claim’s negation.
  • Pipeline: The pipeline iteratively performs entity extraction, generation, claim decomposition, formalization and verification, then refinement.The overview organizes these operations into Setup, Generation, Formalization, Verification, and Decision stages.
  • Claim classification: Claims are classified as mathematical, logical, temporal, probabilistic, commonsense, or vague to reduce false formalization of ambiguous language.Vague predicates lacking binary truth values are prevented from becoming brittle SMT assertions.
  • SMT formalization: Logic-amenable claims target QF_UF and QF_LIA, with candidate formulas compared through semantic equivalence and majority consensus.Round-trip translation provides an additional semantic sanity check, and failed consensus triggers constrained self-correction.
  • Verification cascade: Semantic routing sends mathematical, logical, and temporal claims to SMT while directing commonsense, vague, and probabilistic claims to soft verification.Hybrid verification falls back to soft verification when SMT encounters correctable syntax, declaration, or timeout errors.
  • Feedback and verification: For contradictions, MCS identifies a minimal clause subset whose removal restores satisfiability and yields targeted feedback such as removing a specific constraint.Soft verification instead uses confidence-weighted LLM judge votes, while soft-verified claims receive a lower score cap.
  • Score aggregation: The aggregate score weights entailed claims at 1.0, supported claims at 0.9, and possible claims at 0.7, with contradictions scoring 0.0.A variance-based penalty discourages mutually contradictory claims that appear individually confident.
  • Iterative refinement: Refinement continues until S(A) ≥ 0.75 and joint satisfiability holds, or until score convergence satisfies ΔS < 0.01.Feedback includes unsatisfiable cores and MCS, joint conflicts, and formalization alerts.

4 Results

VERGE consistently outperforms standard prompting and most neurosymbolic baselines, while its ablations show that MCS, semantic routing, SMT verification, and actionable feedback each matter. The system also improves efficiency and converges reliably, but specialized PoT remains stronger on ProofWriter and smaller models face a formalization barrier.

  • General Performance Trends and Robustness: VERGE outperforms standard prompting and existing neurosymbolic baselines on 5 of 6 benchmarks.On GPT-OSS-120B, HLE improves from 14.2% with CoT to 30.5% with VERGE.
  • Limitations and Outliers: Proof of Thought remains dominant on ProofWriter, scoring 98.4% versus VERGE’s 89.9%.The paper attributes this outlier to PoT’s specialized monolithic execution on a rigid synthetic dataset.
  • Efficiency: VERGE at T=1 uses fewer tokens than SR while outperforming it, and SC at k=10 matches its token budget but trails on benchmark accuracy.Compared with ToT-BFS, VERGE also achieves higher scores with fewer tokens and calls on FOLIO and AR-LSAT.
  • Component Ablations: 91.7% to 83.0%: removing MCS sharply reduces AR-LSAT performance, showing the value of precise deletion guidance for scheduling conflicts.The full pipeline consistently outperforms ablated variants, with MCS particularly important for strict constraint satisfaction.
  • Component Ablations: 30.5% to 15.2%: forcing all claims into formal logic halves HLE performance, supporting semantic routing for ambiguous reasoning.Routing permits fallback to soft verification when formalization is brittle.
  • Feedback and Verification: Soft-Only causes a 22.8% average drop, while Unsat-Core-Only and MSF trail the full model by 10.9% and 15.3% on average.These ablations indicate that SMT precision and structurally actionable feedback complement semantic routing.
  • Convergence: VERGE improves monotonically across six datasets and converges at iteration 6.2 on average, with gains beyond T=10 below 0.3%.The reported convergence criterion is ΔS < ε = 0.01.
  • Model Scaling: GPT-OSS-20B achieves only approximately 30% SMT syntax validity, whereas GPT-OSS-120B and Sonnet exceed 90%, enabling semantic contradiction repair.The paper identifies this capability threshold as the Formalization Barrier.

5 Conclusions

VERGE combines LLMs with SMT solvers for verified reasoning through iterative refinement. Its three innovations are multi-sample formalization consensus, semantic routing, and MCS-based error localization.

  • VERGE combines LLMs with SMT solvers to provide verified reasoning through iterative refinement.
  • Multi-sample consensus improves formalization fidelity by aligning candidate logical representations.
  • Semantic routing balances symbolic solvers with soft verification for different claim types.
  • Minimal Correction Subsets localize errors by identifying specific claims for revision.
  • VERGE achieves convergence across all evaluated datasets, unlike the degradation often observed in probabilistic self-refinement.

6 Limitations

VERGE has substantial computational and capability constraints. Its latency limits interactive deployment, while formal verification depends on model scale and restricted logical expressiveness.

  • Problems with more than 20 atomic claims require 15-30 seconds per iteration, compared with over 2 seconds for standard Chain-of-Thought prompting.
  • VERGE’s higher latency limits deployment in applications requiring sub-second responses.
  • Models under 20B parameters achieve only approximately 30% formalization validity, restricting solver feedback to syntax checking.
  • Formal verification is restricted to decidable logics, so claims requiring universal quantification, nonlinear arithmetic, or recursion fall back to soft verification.

7 Ethical Considerations

VERGE’s logical verification does not establish ethical soundness or factual truth. Its verification labels can also create overconfidence, especially for soft-verified or incorrectly formalized claims.

  • VERGE checks internal consistency and logical entailment, not moral soundness or factual truth.
  • Formally consistent reasoning can still support harmful policies, cybersecurity exploits, or false conspiracy theories.
  • High-stakes deployment requires provenance tracking, orthogonal factuality checks, and human expert review.
  • High scores for soft-verified commonsense claims may create false confidence because they lack mathematical guarantees.
  • Incorrect autoformalization can produce syntactically valid SMT code that verifies the wrong statement.

B Rationale for Greedy MCS Computation

VERGE uses claim decomposition, semantic routing, formalization consensus, and SMT-based consistency checks to generate actionable MCS feedback. Greedy MCS computation replaces exponential subset search with a linear-scan approximation, trading optimality for speed.

  • Rationale for Greedy MCS Computation: An MCS is the minimal subset of atomic claims whose removal restores consistency, equivalent to the complement of an MSS.
  • Verification Pipeline: Candidate claims are decomposed into self-contained atomic units before formalization, verification, joint consistency checking, scoring, and feedback generation.
  • Rationale for Greedy MCS Computation: Exact MCS search explores all subsets and has exponential complexity O(2^n), making it infeasible for latency-sensitive pipelines.
  • Rationale for Greedy MCS Computation: The greedy algorithm scans claims sequentially, retaining each claim when adding it preserves satisfiability and marking conflicting claims for removal.
  • Rationale for Greedy MCS Computation: Greedy MCS reduces complexity to O(n × SAT), enabling correction signals for moderate claim counts.
  • Rationale for Greedy MCS Computation: The method is order-dependent and may delete more claims than a globally optimal correction, but prioritizes actionable feedback during iterative refinement.
  • Rationale for Greedy MCS Computation: Claims are sorted by descending verification confidence so stronger claims are retained and weaker links are modified first.
  • Verification Pipeline: Semantic routing sends deterministically provable claims to SMT and claims requiring world knowledge or subjective interpretation to consensus verification.

C.2.3 Verification Implementation

VERGE checks whether candidate formalizations are logically equivalent by testing the unsatisfiability of their negated biconditional. This solver-based check is robust to equivalent forms such as variable renaming and provides a formal consensus guarantee.

  • VERGE verifies semantic equivalence by checking whether the negated biconditional is unsatisfiable in the SMT solver.If SOLVE(Q) returns UNSAT, no model permits the candidate formulas to differ, so they are logically equivalent.
  • The method handles variable renaming, including equivalent formulas such as ∀x.P(x) and ∀y.P(y).Canonicalization or finite instantiation is used for this case.
  • The equivalence check compares candidate formulas at the logical level rather than through string matching or embedding similarity.This provides a mathematically rigorous guarantee that consensus candidates represent the same logical constraint.

C.3 Semantic Router Stress-Test Dataset

The Semantic Router stress-test dataset contains 54 atomic claims spanning formal logic, commonsense ambiguity, and adversarial cases designed to test routing stability. Its examples probe whether numerical or logical language is used literally or rhetorically.

  • The evaluation set contains N = 54 atomic claims divided into three subsets for testing the formal-versus-ambiguous routing boundary.The subsets are Logic & Math, Commonsense & Vague, and Adversarial Edge Cases.
  • The Logic & Math subset contains 22 claims with explicit logical operators, arithmetic constraints, or temporal sequences.Examples include meeting times and numerical comparisons.
  • The Commonsense & Vague subset contains 20 claims involving subjective predicates, probability, or world knowledge not strictly definable in SMT.Examples include likelihood of rain and aesthetic judgments.
  • The Adversarial Edge Cases subset contains 12 manually crafted claims targeting keyword-based routing errors.It includes numeric idioms, rhetorical logical homonyms, and perturbed contexts.
  • Adversarial examples include numeric idioms, rhetorical uses of logical terms, and inverted constraints that test routing consistency under contradiction.Examples include “110% effort,” rhetorical “follows,” and swapping “banned” with “permitted.”

D Adversarial Robustness and Context Faithfulness

VERGE addresses the faithfulness gap by testing whether answers follow perturbed premises rather than parametric memory. Its routing, formalization, and refinement components support context-sensitive verification, with adversarial results reported as fully robust in the tested categories.

  • The faithfulness gap occurs when a reasoning model ignores provided context in favor of its parametric memory.The paper uses counterfactual premises such as “Cats are not mammals” to illustrate this failure mode.
  • The routing module assigns claims to SMT-LIB2 formalization or multi-model consensus according to their semantic claim type.Group A claims are autoformalized, while Group B claims use consensus verification.
  • The stress test uses adversarial pairs with inverted or perturbed logical constraints, including changes from “banned” to “permitted” and swapped temporal order.These perturbations test whether the system remains faithful to the altered context.
  • 100% robustness was reported across the tested adversarial categories, with an average verification score of 0.91.The results state that MCS-guided feedback aligned answers with perturbed contexts rather than standard prior answers.
  • VERGE decomposes answers into atomic claims, routes them to an appropriate verifier, translates formalizable claims into solver code, and feeds MCS feedback into refinement.The prompts define semantic types, SMT-LIB2 output, and contradiction-specific revision instructions.
  • VERGE’s iterative refinement shows perfect monotonic improvement across 10 iterations, with Kendall’s τ = 1.0 and p < 0.001 across all datasets.The figure reports 95% confidence bands around the accuracy progression.
  • Formalization consensus generates K = 3 candidates and accepts a representative when an equivalence clique reaches majority size; otherwise, the claim is routed to Soft Verification.Candidate equivalence is established through solver checks of negated formulas.
  • The final score uses weighted claim-status averages and a variance penalty to discourage internally inconsistent answers.The statuses are Entailed=1.0, Soft-Pass=0.9, Possible=0.7, and Fail=0.0.

E.4 Pipeline Reliability and Failure Modes

VERGE’s reliability analysis audits decomposition, formalization, routing, and verification safeguards across benchmarks and case studies. The evidence identifies protections against common errors while preserving explicit limits for soft verification and formalization scope.

  • On 80 audited trajectories, decomposition errors were dominated by omissions rather than fabrications, with omitted claims resurfacing as joint inconsistencies repaired by MCS feedback.This audit targets decomposition as a potential source of silent verification corruption.
  • Consensus and round-trip alignment form sequential formalization gates: misformalizations must appear in at least 2/3 samples, while invalid SMT triggers soft fallback.The funnel is described as degrading gracefully below the formalization barrier.
  • On GPT-OSS-120B, logic-heavy benchmarks are more than 76% SMT-verified, whereas HLE and BBEH are soft-dominated because of their claim characteristics.The routing distribution is presented as an honest reflection of verification coverage.
  • Three formalization failure modes—predicate mismatches, quantifier scope, and missing axioms—are addressed by parse-error fallback, consensus disagreement, or context refinement.The Soft-Only ablation reduces average performance by 22.8%, indicating that these safeguards are load-bearing.
  • Entity extraction accuracy ranges from 93−99% across benchmarks, while gold entities on AR-LSAT increase consensus by 2.1% and accuracy by 0.7%.The study interprets these results as robustness to extraction noise.
  • Soft verification remains vulnerable to correlated judge errors, which the variance penalty, 0.9 contribution cap, and joint check mitigate but do not eliminate.The paper treats shared hallucinations as fundamental to consensus-based verification.
  • Beyond T=10, performance changes are negligible at less than 0.3% across benchmarks, supporting the convergence criterion ∆S < ϵ = 0.01.The convergence evidence comes from the extended-iteration analysis.
Loading 2601.20055v2…