VERGE: Formale Verfeinerungs- und Lenkungs-Engine für verifizierbare LLM-Argumentation

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

January 27, 2026

papers.authors: Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless

cs.AI

papers.abstract

Trotz der syntaktischen Flüssigkeit großer Sprachmodelle (LLMs) bleibt die Gewährleistung ihrer logischen Korrektheit in hochriskanten Domänen eine grundlegende Herausforderung. Wir stellen einen neurosymbolischen Rahmen vor, der LLMs mit SMT-Solvern kombiniert, um verifizierungsgeleitete Antworten durch iterative Verfeinerung zu erzeugen. Unser Ansatz zerlegt LLM-Ausgaben in atomare Behauptungen, formalisiert diese automatisch in Logik erster Stufe und überprüft ihre logische Konsistenz mittels automatischem Theorembeweisen. Wir führen drei Schlüsselinnovationen ein: (1) Multi-Modell-Konsens durch formale Äquivalenzprüfung auf Semantikebene, um Logikebene-Übereinstimmung zwischen Kandidaten sicherzustellen und die syntaktische Verzerrung oberflächenbasierter Metriken zu eliminieren, (2) semantisches Routing, das verschiedene Behauptungstypen zu geeigneten Verifikationsstrategien lenkt: symbolische Löser für logische Behauptungen und LLM-Ensembles für Common-Sense-Reasoning, und (3) präzise logische Fehlerlokalisierung durch Minimale Korrektureilmengen (MCS), die die exakte Teilmenge der zu revidierenden Behauptungen identifizieren und binäre Fehlersignale in umsetzbares Feedback verwandeln. Unser Rahmen klassifiziert Behauptungen nach ihrem logischen Status und aggregiert multiple Verifikationssignale zu einem einheitlichen Score mit varianzbasiertem Penalty. Das System verfeinert Antworten iterativ unter Verwendung strukturierten Feedbacks, bis Akzeptanzkriterien erfüllt sind oder Konvergenz erreicht wird. Dieser hybride Ansatz liefert formale Garantien, wo möglich, und Konsensverifikation andernorts, was vertrauenswürdige KI voranbringt. Mit dem GPT-OSS-120B-Modell demonstriert VERGE eine durchschnittliche Leistungssteigerung von 18,7 % bei Konvergenz über eine Reihe von Reasoning-Benchmarks im Vergleich zu Single-Pass-Ansätzen.

English

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.