VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

TL;DR

VERGE presents a neurosymbolic framework that couples large language models with SMT solvers to achieve verification-guided reasoning through iterative refinement. It decomposes outputs into atomic claims, autoformalizes them into first-order logic, and uses a verification cascade with semantic routing to apply formal verification where possible and soft consensus where not, guided by Minimal Correction Subsets to localize errors. The approach yields formal guarantees for verifiable claims and consensus verification for open-domain reasoning, demonstrating robustness and convergence across multiple benchmarks, with an average uplift of 18.7% at convergence on a strong backbone model. A key finding is the Formalization Barrier, where formal verification becomes viable only at larger model scales, highlighting the need for frontier models and careful interface design to prevent overreliance on automated guarantees in practice.

Abstract

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.

Figures (3)

• Figure 1: VERGE correcting LLM Hallucinations via Formal Verification. The solver detects an unsupported claim and guides the LLM to a consistent answer through MCS-based feedback.
• Figure 2: Overview of VERGE: The pipeline is structured into five distinct stages: Setup prepares the context $\mathcal{C}$ and entities $\mathcal{E}$; Generation produces and refines answers $\mathcal{A}^{(t)}$ iteratively; Formalization classifies claim types $\tau_i$ and generates SMT formulas $\varphi_{c_i}$; Verification routes claims to SMT, Soft, or Hybrid verifiers based on semantic type; and Decision computes the aggregate score $\mathcal{S}(\mathcal{A})$ to either accept the answer $\mathcal{A}^*$ or generate feedback $\mathcal{F}^{(t)}$ for the next iteration.
• Figure 3: The Correlation Cliff in Iterative Refinement. Accuracy progression over 10 iterations (GPT-OSS-120B). VERGE exhibits perfect monotonic improvement (Kendall's $\tau = 1.0$, $p < 0.001$ across all datasets). Probabilistic Self-Refinement shows systematic degradation ($\tau = -0.84$ average, $p < 0.001$), stagnating below the CoT baseline in 85% of trials ($\chi^2 = 26.7$, $p < 0.001$). Shaded regions show 95% confidence bands.