# VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

arXiv: https://arxiv.org/abs/2601.20055 · HTML: https://mlsanity.com/paper/2601.20055/

## Key facts

- Cited by 12 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 20 of its 61 references that are in the map.
- First posted on arXiv 27 Jan 2026.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 20 of 20)

- [Evaluating Large Language Models Trained on Code](https://mlsanity.com/paper/2107.03374/) (2021)
- [Let's Verify Step by Step](https://mlsanity.com/paper/2305.20050/) (2023)
- [Program Synthesis with Large Language Models](https://mlsanity.com/paper/2108.07732/) (2021)
- [Improving Factuality and Reasoning in Language Models through Multiagent Debate](https://mlsanity.com/paper/2305.14325/) (2023)
- [Large Language Models Cannot Self-Correct Reasoning Yet](https://mlsanity.com/paper/2310.01798/) (2023)
- [Encouraging Divergent Thinking in Large Language Models through Multi-Agent Debate](https://mlsanity.com/paper/2305.19118/) (2023)
- [Solving math word problems with process- and outcome-based feedback](https://mlsanity.com/paper/2211.14275/) (2022)
- [Humanity's Last Exam](https://mlsanity.com/paper/2501.14249/) (2025)
- [Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning](https://mlsanity.com/paper/2305.12295/) (2023)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Faithful Chain-of-Thought Reasoning](https://mlsanity.com/paper/2301.13379/) (2023)
- [ZebraLogic: On the Scaling Limits of LLMs for Logical Reasoning](https://mlsanity.com/paper/2502.01100/) (2025)
- [ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematics](https://mlsanity.com/paper/2302.12433/) (2023)
- [AR-LSAT: Investigating Analytical Reasoning of Text](https://mlsanity.com/paper/2104.06598/) (2021)
- [VERUS-LM: a Versatile Framework for Combining LLMs with Symbolic Reasoning](https://mlsanity.com/paper/2501.14540/) (2025)
- [VeriCoT: Neuro-symbolic Chain-of-Thought Validation via Logical Consistency Checks](https://mlsanity.com/paper/2511.04662/) (2025)
- [Automated Theorem Provers Help Improve Large Language Model Reasoning](https://mlsanity.com/paper/2408.03492/) (2024)
- [Mid-Think: Training-Free Intermediate-Budget Reasoning via Token-Level Triggers](https://mlsanity.com/paper/2601.07036/) (2026)
- [Efficient Fine-Grained GPU Performance Modeling for Distributed Deep Learning of LLM](https://mlsanity.com/paper/2509.22832/) (2025)

## Built on by (most cited first, 12 of 12)

- [Toward Guarantees for Clinical Reasoning in Vision Language Models via Formal Verification](https://mlsanity.com/paper/2602.24111/) (2026)
- [MANTRA: Synthesizing SMT-Validated Compliance Benchmarks for Tool-Using LLM Agents](https://mlsanity.com/paper/2605.06334/) (2026)
- [Path-Lock Expert: Separating Reasoning Mode in Hybrid Thinking via Architecture-Level Separation](https://mlsanity.com/paper/2604.27201/) (2026)
- [Know Your Limits : On the Faithfulness of LLMs as Solvers and Autoformalizers in Legal Reasoning](https://mlsanity.com/paper/2606.16118/) (2026)
- [NeuroProlog: Multi-Task Fine-Tuning for Neurosymbolic Mathematical Reasoning via the Cocktail Effect](https://mlsanity.com/paper/2603.02504/) (2026)
- [Reliability-Gated Source Anchoring for Continual Test-Time Adaptation](https://mlsanity.com/paper/2605.14063/) (2026)
- [LogicTrack: Auditing Reasoning Trajectories of Large Language Models with Formal Logic Solvers](https://mlsanity.com/paper/2609.21492/) (2026)
- [TraceFix: Repairing Agent Coordination Protocols with TLA+ Counterexamples](https://mlsanity.com/paper/2605.07935/) (2026)
- [CausalGuard: Conformal Inference under Graph Uncertainty](https://mlsanity.com/paper/2605.21928/) (2026)
- [ADVENT: LLM-Driven Automatic Predicate Invention for ILP](https://mlsanity.com/paper/2607.01585/) (2026)
- [Beyond Solver Verdicts: Generative Reward Models for Autoformalization](https://mlsanity.com/paper/2609.11085/) (2026)
- [Sequent-Prover: Training Agents for Formal, Checkable SMT-based Reasoning](https://mlsanity.com/paper/2610.15258/) (2026)

## Abstract (arXiv)

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.