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 & tables
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 C and entities E ; Generation produces and refines answers A(t) iteratively; Formalization classifies claim types τi and generates SMT formulas φci ; Verification routes claims to SMT, Soft, or Hybrid verifiers based on semantic type; and Decision computes the aggregate score S(A) to either accept the answer A∗ or generate feedback F(t) for the next iteration.
Architectural Components
Feedback Granularity
Dataset
Full
w/o MCS
w/o Routing
Soft-Only
Unsat-Core Only
MSF
FOLIO
84.7
80.7
81.6
80.8
79.3
76.5
ProofWriter
89.9
88.7
84.6
75.8
82.4
80.1
ZebraLogic
91.0
88.9
90.9
70.2
85.3
72.5
AR-LSAT
91.7
83.0
87.4
84.6
89.4
89.2
BBEH
58.9
54.1
50.2
41.7
42.7
40.1
Table 2: Ablation Study on Component Contributions (GPT-OSS-120B). We isolate the impact of Minimal Correction Subsets (MCS), Semantic Routing (Rt), and the SMT Solver itself. Full represents the complete VERGE pipeline. w/o Routing forces SMT verification for all claims. Soft-Only removes the SMT solver entirely, relying solely on LLM consensus. Unsat-Core-Only and MSF vary the granularity of the feedback.
Dataset
Unanimous fidelity
Non-una fidelity
Conservative errors
False assertions
FOLIO
76.7%
56.0%
91.9%
3.0%
ProofWriter
80.5%
70.6%
94.3%
1.4%
Table 3: Gold-referenced natural-language-to-SMT fidelity. Conservative errors replace a gold True or False verdict with Uncertain rather than asserting an incorrect polarity.
Appendix figures & tables11 assets
Supplementary material from the paper’s appendix.
Appendix
Type
Definition
Example
Router
Group A: SMT-Amenable Claims (Hard Verification)
τM
Mathematical : Claims involving arithmetic operations, algebraic constraints, numerical comparisons, or unit conversions.
"x is a prime number greater than 5 and less than 20."
SMT
τL
Logical : Claims involving formal entailment, set theory inclusion, boolean logic, or syllogistic structure.
"All entities in set A must also belong to set B."
SMT
τT
Temporal : Claims involving linear sequencing, specific timestamps, duration, or precedence constraints.
"The event occurred 3 days after the signing."
SMT
Group B: LLM-Consensus Claims (Soft Verification)
τC
Commonsense : Claims relying on general world knowledge, causality, or physical properties not strictly definable by axioms.
"Glass typically shatters when dropped on concrete."
Soft
Appendix
Table 4: Definitions of Semantic Claim Types ( τ ) used in the Routing Module. Claims in Group A are autoformalized into SMT-LIB2 logic; Claims in Group B are verified via multi-model consensus.
Figure 3: The Correlation Cliff in Iterative Refinement. Accuracy progression over 10 iterations (GPT-OSS-120B). VERGE exhibits perfect monotonic improvement (Kendall’s τ=1.0 , p<0.001 across all datasets). Probabilistic Self-Refinement shows systematic degradation ( τ=−0.84 average, p<0.001 ), stagnating below the CoT baseline in 85% of trials ( χ2=26.7 , p<0.001 ). Shaded regions show 95% confidence bands.
Category
Example Claim
Correct Route
Numeric Idiom
“The team gave 110% effort.”
Soft
Numeric (Real)
“The score was 110 points.”
SMT
Logical Homonym
“It follows that he felt sad.”
Soft
Logical (Real)
“It follows that A⊂B .”
SMT
Vague Quantifier
“Many people attended.”
Soft
Exact Quantifier
“More than 50 people attended.”
SMT
Appendix
Table 5: Examples from the Semantic Router Stress-Test Dataset, highlighting adversarial pairs used to test the router’s discrimination capabilities.
Method
LLM Calls
Solver Calls
Tokens (I+O)
Wall (s)
CoT (1-pass)
1
0
2.1K
3.2
SC ( k=3 )
3
0
6.3K
8.7
SC ( k=10 )
10
0
21.0K
28.3
SR ( n=3 )
6
0
11.4K
15.3
PoT
2
1
4.8K
5.4
LINC
3
1
5.1K
6.1
Appendix
Table 6: Per-problem cost on GPT-OSS-120B, averaged across six benchmarks. VERGE at T=1 requires fewer tokens than Self-Refine while yielding higher accuracy.
Benchmark
Claims/Ans.
Precision
Recall
FOLIO
3.2
0.96
0.94
ProofWriter (PW)
4.1
0.97
0.95
ZebraLogic (ZL)
5.8
0.93
0.91
AR-LSAT
6.4
0.94
0.92
BBEH
4.7
0.92
0.90
HLE
5.3
0.91
0.89
Appendix
Table 7: Decomposition quality based on 80 audited trajectories.
Stage
20B
120B
Routed to hard (SMT)
68.1%
72.3%
Syntactically valid
30.2%
92.3%
Consensus ( ≥2/3 )
41.2%
87.1%
Round-trip aligned
79.4%
94.6%
Verified by solver
12.1%
83.8%
Soft fallback
55.9%
16.2%
Appendix
Table 8: Formalization funnel by scale. VERGE degrades gracefully below the formalization barrier.
Benchmark
Hard
Soft
Hybrid
FOLIO
82.4%
12.1%
5.5%
PW
91.3%
4.2%
4.5%
ZL
88.7%
6.8%
4.5%
AR-LSAT
76.3%
16.2%
7.5%
BBEH
54.1%
35.8%
10.1%
HLE
41.2%
47.3%
11.5%
Appendix
Table 9: Routing percentages on GPT-OSS-120B.
ws
FOLIO
PW
ZL
AR-LSAT
BBEH
HLE
0.70
83.9
89.2
90.6
90.8
57.4
29.1
0.80
84.3
89.5
90.8
91.2
58.1
29.7
0.90
84.7
89.9
91.0
91.7
58.9
30.5
0.95
84.4
89.7
90.9
91.4
58.5
30.2
1.00
84.0
89.3
90.5
91.0
57.8
29.4
Appendix
Table 10: Sensitivity to the ws parameter on GPT-OSS-120B
Table 12: Adversarial Robustness results. “Safe” indicates the system either rejected the invalid premise or, in these cases, successfully adapted its reasoning to the counterfactual context (faithfulness), achieving high verification scores ( >0.9 ) on the perturbed inputs.
Parameter
Value
LLM Generation
Temperature ( Tgen )
1.0
Top-P
0.99
Max Output Tokens
10,000
Thinking Budget
4,000
VERGE Pipeline
Appendix
Table 13: Hyperparameters for the VERGE pipeline. These values were held constant across all datasets (FOLIO, ZebraLogic, etc.) to demonstrate robustness.