VERGE : Moteur de Raffinement Formel et de Guidage pour le Raisonnement Vérifiable des LLM

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

Malgré l'aisance syntaxique des modèles de langage de grande taille (LLM), garantir leur exactitude logique dans des domaines à haut risque demeure un défi fondamental. Nous présentons un cadre neurosymbolique qui combine les LLM avec des solveurs SMT pour produire des réponses guidées par la vérification via un raffinement itératif. Notre approche décompose les sorties des LLM en affirmations atomiques, les auto-formalise en logique du premier ordre et vérifie leur cohérence logique à l'aide de la démonstration automatique de théorèmes. Nous introduisons trois innovations clés : (1) un consensus multi-modèles via la vérification d'équivalence sémantique formelle pour assurer un alignement au niveau logique entre les candidats, éliminant le biais syntaxique des métriques de forme de surface, (2) un routage sémantique qui dirige différents types d'affirmations vers des stratégies de vérification appropriées : les solveurs symboliques pour les affirmations logiques et des ensembles de LLM pour le raisonnement de sens commun, et (3) une localisation précise des erreurs logiques via les Sous-ensembles de Correction Minimale (MCS), qui identifient le sous-ensemble exact d'affirmations à réviser, transformant les signaux d'échec binaires en un retour d'information actionnable. Notre cadre classe les affirmations selon leur statut logique et agrège de multiples signaux de vérification en un score unifié avec une pénalité basée sur la variance. Le système affine itérativement les réponses en utilisant un retour structuré jusqu'à ce que les critères d'acceptation soient satisfaits ou qu'une convergence soit atteinte. Cette approche hybride offre des garanties formelles lorsque cela est possible et une vérification par consensus ailleurs, faisant progresser l'IA digne de confiance. Avec le modèle GPT-OSS-120B, VERGE démontre une amélioration moyenne des performances de 18,7 % à la convergence sur un ensemble de benchmarks de raisonnement par rapport aux approches en une seule passe.

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.