<?xml version="1.0" encoding="UTF-8"?>
<modsCollection xmlns="http://www.loc.gov/mods/v3">
<mods ID="singh-etal-2026-verge">
    <titleInfo>
        <title>VERGE : Formal Refinement and Guidance Engine for Verifiable LLM Reasoning</title>
    </titleInfo>
    <name type="personal">
        <namePart type="given">Vikash</namePart>
        <namePart type="family">Singh</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Darion</namePart>
        <namePart type="family">Cassel</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Nathaniel</namePart>
        <namePart type="family">Weir</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Nick</namePart>
        <namePart type="family">Feng</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <name type="personal">
        <namePart type="given">Sam</namePart>
        <namePart type="family">Bayless</namePart>
        <role>
            <roleTerm authority="marcrelator" type="text">author</roleTerm>
        </role>
    </name>
    <originInfo>
        <dateIssued>2026-10</dateIssued>
    </originInfo>
    <typeOfResource>text</typeOfResource>
    <relatedItem type="host">
        <titleInfo>
            <title>Findings of the Association for Computational Linguistics: EMNLP 2026</title>
        </titleInfo>
        <name type="personal">
            <namePart type="given">Hung-Yi</namePart>
            <namePart type="family">Lee</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Sunipa</namePart>
            <namePart type="family">Dev</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Jessy</namePart>
            <namePart type="family">Li</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <name type="personal">
            <namePart type="given">Desmond</namePart>
            <namePart type="family">Elliott</namePart>
            <role>
                <roleTerm authority="marcrelator" type="text">editor</roleTerm>
            </role>
        </name>
        <originInfo>
            <publisher>Association for Computational Linguistics</publisher>
            <place>
                <placeTerm type="text">Budapest, Hungary</placeTerm>
            </place>
        </originInfo>
        <genre authority="marcgt">conference publication</genre>
        <identifier type="isbn">979-8-89176-462-0</identifier>
    </relatedItem>
    <abstract>Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present VERGE, a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. VERGE decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. VERGE 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. VERGE 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.</abstract>
    <identifier type="citekey">singh-etal-2026-verge</identifier>
    <location>
        <url>https://aclanthology.org/2026.findings-emnlp.1309/</url>
    </location>
    <part>
        <date>2026-10</date>
        <extent unit="page">
            <start>27677</start>
            <end>27702</end>
        </extent>
    </part>
</mods>
</modsCollection>

%0 Conference Proceedings
%T VERGE : Formal Refinement and Guidance Engine for Verifiable LLM Reasoning
%A Singh, Vikash
%A Cassel, Darion
%A Weir, Nathaniel
%A Feng, Nick
%A Bayless, Sam
%Y Lee, Hung-Yi
%Y Dev, Sunipa
%Y Li, Jessy
%Y Elliott, Desmond
%S Findings of the Association for Computational Linguistics: EMNLP 2026
%D 2026
%8 October
%I Association for Computational Linguistics
%C Budapest, Hungary
%@ 979-8-89176-462-0
%F singh-etal-2026-verge
%X Despite the syntactic fluency of Large Language Models (LLMs), ensuring their logical correctness in high-stakes domains remains a fundamental challenge. We present VERGE, a neurosymbolic framework that combines LLMs with SMT solvers to produce verification-guided answers through iterative refinement. VERGE decomposes LLM outputs into atomic claims, autoformalizes them into first-order logic, and verifies their logical consistency using automated theorem proving. VERGE 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. VERGE 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.
%U https://aclanthology.org/2026.findings-emnlp.1309/
%P 27677-27702

Markdown (Informal)

[VERGE : Formal Refinement and Guidance Engine for Verifiable LLM Reasoning](https://aclanthology.org/2026.findings-emnlp.1309/) (Singh et al., Findings 2026)

• VERGE : Formal Refinement and Guidance Engine for Verifiable LLM Reasoning (Singh et al., Findings 2026)

ACL

• Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, and Sam Bayless. 2026. VERGE : Formal Refinement and Guidance Engine for Verifiable LLM Reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2026, pages 27677–27702, Budapest, Hungary. Association for Computational Linguistics.