VERGE: Motore di Raffinamento Formale e Guida per il Ragionamento Verificabile dei LLM

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

January 27, 2026

Autori: Vikash Singh, Darion Cassel, Nathaniel Weir, Nick Feng, Sam Bayless

cs.AI

Abstract

Nonostante la fluidità sintattica dei Large Language Model (LLM), garantire la loro correttezza logica in domini ad alto rischio rimane una sfida fondamentale. Presentiamo un framework neurosimbolico che combina LLM con risolutori SMT per produrre risposte guidate dalla verifica attraverso raffinamenti iterativi. Il nostro approccio scompone gli output degli LLM in asserzioni atomiche, le autoformalizza in logica del primo ordine e ne verifica la coerenza logica utilizzando il teorema automatico di dimostrazione. Introduciamo tre innovazioni chiave: (1) consenso multi-modello tramite verifica dell'equivalenza semantica formale per garantire l'allineamento a livello logico tra i candidati, eliminando il bias sintattico delle metriche di forma superficiale, (2) instradamento semantico che indirizza diversi tipi di asserzioni a strategie di verifica appropriate: risolutori simbolici per affermazioni logiche e ensemble di LLM per il ragionamento di senso comune, e (3) localizzazione precisa degli errori logici tramite Insiemi di Correzione Minima (MCS), che individuano l'esatto sottoinsieme di asserzioni da revisionare, trasformando segnali di fallimento binari in feedback azionabili. Il nostro framework classifica le asserzioni in base al loro stato logico e aggrega molteplici segnali di verifica in un punteggio unificato con penalità basata sulla varianza. Il sistema raffina iterativamente le risposte utilizzando feedback strutturato finché non vengono soddisfatti i criteri di accettazione o si raggiunge la convergenza. Questo approccio ibrido fornisce garanzie formali dove possibile e verifica di consenso altrove, promuovendo l'IA affidabile. Con il modello GPT-OSS-120B, VERGE dimostra un miglioramento prestazionale medio del 18,7% alla convergenza su una serie di benchmark di ragionamento rispetto agli approcci a passaggio singolo.

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.