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.
Large Language Models (LLMs) have demonstrated remarkable proficiency in natural language understanding, yet they struggle with strict multi-step reasoning, frequently suffering from hallucinations and inconsistency. Existing solutions like Chain-of-Thought (CoT) lack rigorous verification mechanisms, while standard Retrieval-Augmented Generation (RAG) often misses the complex, structural dependencies inherent in logical tasks. To bridge this gap, we propose a Neuro-Symbolic architecture that integrates a Logical Knowledge Graph (LKG) with dynamic solver routing. Specifically, we introduce an ontology-based LKG that treats logical rules and constraints as first-class topological nodes, enabling explicit modeling of dependencies extracted from text. We further design a Logic Router to dynamically dispatch tasks to the optimal symbolic engine, which is supported by a topology-aware hybrid retrieval mechanism. Experimental results on logical reasoning benchmarks demonstrate that our framework significantly outperforms state-of-the-art prompting and RAG baselines, delivering higher accuracy and verifiable reasoning paths.
Chain-of-Thought (CoT) reasoning has been shown to improve the performance of large language models (LLMs), yet existing optimization methods largely rely on outcome-based feedback, leaving the logical validity of intermediate reasoning steps largely unverified. To address the gap whereby LLMs arrive at correct final answers through logically flawed intermediate reasoning chains, we propose LogicTrack, a neuro-symbolic framework that audits reasoning trajectories by auto-formalizing each reasoning step into symbolic representations and verifying it with automated theorem provers. LogicTrack introduces Solver-Based Backtracking Reward (SBR), a step-wise scoring mechanism that quantifies logical soundness and guides backtracking tree search at inference time. We further extend LogicTrack to construct supervised fine-tuning (SFT) data with backtracking traces from its trajectories, enabling fine-tuned models to internalize step-wise auditing as an intrinsic capability. Extensive experiments across 8 reasoning benchmarks and 7 LLMs demonstrate that LogicTrack effectively improves both the verifiability of reasoning chains and final answer pass rate, thereby enhancing overall CoT quality and trustworthiness in high-stakes domains.
Jingyu Hu, Shu Yang, Weiru Liu +1
University of Bristol · King Abdullah University of Science and Technology
Verifiers are crucial components for enhancing modern LLMs' reasoning capability. Typicalverifiers require resource-intensive superviseddataset construction, which is costly and faceslimitations in data diversity. In this paper, wepropose LOVER, an unsupervised verifier regularized by logical rules. LOVER treats theverifier as a binary latent variable, utilizinginternal activations and enforcing three logical constraints on multiple reasoning paths:negation consistency, intra-group consistency,and inter-group consistency (grouped by thefinal answer). By incorporating logical rulesas priors, LOVER can leverage unlabeled examples and is directly compatible with any offthe-shelf LLMs. Experiments on 10 datasetsdemonstrate that LOVER significantly outperforms unsupervised baselines, achieving performance comparable to the supervised verifier(reaching its 95% level on average). The sourcecode is publicly available at https://github.com/wangxinyufighting/llm-lover.
Xinyu Wang, Changzhi Sun, Lian Cheng +4
Department of Computer Science and Technology, East China Normal University · Institute of Artificial Intelligence (TeleAI), China Telecom