VERGE: Motor de Refinamiento Formal y Guía para el Razonamiento Verificable en LLM

VERGE: Formal Refinement and Guidance Engine for Verifiable LLM Reasoning

January 27, 2026

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

cs.AI

Resumen

A pesar de la fluidez sintáctica de los Modelos de Lenguaje a Gran Escala (LLMs), garantizar su corrección lógica en dominios de alto riesgo sigue siendo un desafío fundamental. Presentamos un marco neurosimbólico que combina LLMs con solucionadores SMT para producir respuestas guiadas por verificación mediante refinamiento iterativo. Nuestro enfoque descompone las salidas de los LLMs en afirmaciones atómicas, las autoformaliza en lógica de primer orden y verifica su coherencia lógica mediante demostración automática de teoremas. Introducimos tres innovaciones clave: (1) consenso multi-modelo mediante verificación de equivalencia semántica formal para garantizar la alineación a nivel lógico entre candidatos, eliminando el sesgo sintáctico de las métricas de forma superficial, (2) enrutamiento semántico que dirige diferentes tipos de afirmaciones a estrategias de verificación apropiadas: solucionadores simbólicos para afirmaciones lógicas y conjuntos de LLMs para razonamiento de sentido común, y (3) localización precisa de errores lógicos mediante Subconjuntos de Corrección Mínima (MCS), que identifican el subconjunto exacto de afirmaciones a revisar, transformando señales de fallo binarias en retroalimentación accionable. Nuestro marco clasifica las afirmaciones por su estado lógico y agrega múltiples señales de verificación en una puntuación unificada con penalización basada en varianza. El sistema refina iterativamente las respuestas utilizando retroalimentación estructurada hasta que se cumplen los criterios de aceptación o se logra la convergencia. Este enfoque híbrido ofrece garantías formales donde es posible y verificación por consenso en otros casos, avanzando hacia una IA confiable. Con el modelo GPT-OSS-120B, VERGE demuestra una mejora de rendimiento promedio del 18.7% en convergencia a través de un conjunto de benchmarks de razonamiento en comparación con enfoques de pasada única.

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.