VERGE: Motor de Refinamento Formal e Orientação para Raciocínio Verificável em 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

Resumo

Apesar da fluência sintática dos Modelos de Linguagem de Grande Porte (LLMs), garantir sua correção lógica em domínios de alta criticidade permanece um desafio fundamental. Apresentamos uma estrutura neurosimbólica que combina LLMs com solucionadores SMT para produzir respostas guiadas por verificação através de refinamento iterativo. Nossa abordagem decompõe as saídas dos LLMs em afirmações atômicas, as autoformaliza em lógica de primeira ordem e verifica sua consistência lógica usando provas de teoremas automatizadas. Introduzimos três inovações principais: (1) consenso multi-modelo via verificação de equivalência semântica formal para garantir alinhamento em nível lógico entre candidatos, eliminando o viés sintático de métricas de forma superficial, (2) roteamento semântico que direciona diferentes tipos de afirmações para estratégias de verificação apropriadas: solucionadores simbólicos para afirmações lógicas e conjuntos de LLMs para raciocínio de senso comum, e (3) localização precisa de erros lógicos via Conjuntos de Correção Mínima (MCS), que identificam o subconjunto exato de afirmações a revisar, transformando sinais binários de falha em *feedback* acionável. Nossa estrutura classifica as afirmações por seu status lógico e agrega múltiplos sinais de verificação em uma pontuação unificada com penalidade baseada em variância. O sistema refina respostas iterativamente usando *feedback* estruturado até que os critérios de aceitação sejam atendidos ou a convergência seja alcançada. Esta abordagem híbrida oferece garantias formais onde possível e verificação por consenso em outros casos, avançando a IA confiável. Com o modelo GPT-OSS-120B, o VERGE demonstra uma melhoria média de desempenho de 18,7% na convergência em um conjunto de *benchmarks* de raciocínio em comparação com abordagens de passagem ú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.