Resumen Técnico: SymboUQ

Declaración del Problema

Los Modelos de Lenguaje Extensos (LLMs) a menudo generan trazas de razonamiento fluidas para tareas de razonamiento espacial, pero los pasos relacionales intermedios pueden fallar al sustentar la conclusión final. Un solo paso incorrecto de dirección o contención puede corromper la configuración espacial inferida, dejando la explicación aparentemente coherente. Los métodos de cuantificación de la incertidumbre (UQ) existentes se basan en estadísticas a nivel de token, acuerdo semántico o representaciones internas, que pueden correlacionarse con la corrección sin evaluar directamente la semántica espacial. Por el contrario, los verificadores formales proporcionan evidencia semántica más fuerte, pero sufren de una aplicabilidad parcial: una afirmación puede ser parseada con éxito en un lenguaje formal (simbolizable), pero producir un resultado de "desconocido" o "no evaluable" debido a premisas insuficientes o inconsistencias de contexto. En consecuencia, la cobertura de parseo por sí sola es un proxy insuficiente para la cantidad de evidencia utilizable que proporciona un verificador.

Metodología: SymboUQ

Los autores proponen SymboUQ, un marco de cuantificación de la incertidumbre simbólica que estima la fiabilidad de la respuesta final distinguiendo entre simbolizabilidad (si una afirmación puede traducirse al lenguaje formal del verificador) y determinación semántica (si la ejecución de esa afirmación produce un veredicto de implicación o contradicción definida). El marco consta de tres componentes principales:

1. Auditor de Diseño (Layout Auditor)

El Auditor de Diseño ejecuta afirmaciones espaciales ordenadas secuencialmente contra una descripción de escena de confianza.

• Generación de Restricciones: Mapea enunciados de lenguaje natural en un sistema de relaciones canónico (tripletas de sujeto, relación, objeto) que cubre dirección, contención, distancia y topología.
• Ejecución y Veredictos: Mantiene un contexto activo (la escena de confianza más las afirmaciones simbolizables precedentes) y evalúa cada afirmación $c_k$ contra este contexto. Las afirmaciones reciben uno de cuatro estados:
  • Implicada ($en$): La afirmación se sigue del contexto activo.
  • Contradicha ($co$): La afirmación entra en conflicto con el contexto activo.
  • Desconocida ($un$): La afirmación es simbolizable pero el contexto carece de información suficiente para resolverla.
  • No Evaluable ($no$): El contexto activo ya es infactible (debido a contradicciones previas), lo que impide la evaluación posterior.
• Extracción de Evidencia: El auditor extrae características relacionadas con la factibilidad, la detección de conflictos y los costos de reparación acotados (eliminar relaciones generadas para restaurar la factibilidad manteniendo fija la escena de confianza).

2. Perfil de Determinación (Determinacy Profile)

Este módulo genera un perfil sin etiquetas $\phi(r)$ que caracteriza la "cobertura ejecutable efectiva" de una traza de razonamiento, independientemente de la polaridad del veredicto.

• Simbolizabilidad ($\pi(r)$): La fracción de afirmaciones que pueden ser parseadas en el lenguaje formal.
• Tasa de Desconocidos ($\nu(r)$): La fracción de afirmaciones parseadas que permanecen sin resolver (desconocidas).
• Determinación Semántica ($d(r)$): La fracción de afirmaciones parseadas que reciben un veredicto definido ($en$o$co$) bajo un contexto factible. Crucialmente, las afirmaciones marcadas como "no evaluables" reducen la determinación, ya que representan una pérdida de evidencia utilizable.
• Aplicabilidad del Verificador ($\delta(r)$): Definida como $\pi(r) \times d(r)$, representa la fracción de todas las afirmaciones que son tanto simbolizables como semánticamente determinadas.

3. Compositor de Fiabilidad Consciente de la Determinación (DARC)

DARC integra señales de fiabilidad heterogéneas (basadas en restricciones, en representaciones y en decodificación) condicionadas al perfil de aplicabilidad de la traza.

• Banco de Candidatos: Utiliza un banco de estimadores pre-entrenados o libres de entrenamiento (por ejemplo, entropía de tokens, sondas neuronales, solucionadores de restricciones).
• Adaptación de Objetivo: Utilizando un conjunto de validación etiquetado del dominio objetivo, DARC filtra candidatos (eliminando puntuaciones casi aleatorias) y los orienta (invirtiendo puntuaciones si el AUROC es $<0.5$).
• Composición Condicionada a la Aplicabilidad: DARC construye vectores de características que interactúan las puntuaciones de los candidatos con el perfil de determinación. Específicamente, utiliza términos de interacción como $\delta(r) \cdot s_j(r)$ para modular la contribución de la evidencia basada en restricciones según la determinación semántica. Esto permite al modelo disminuir el peso de la evidencia simbólica cuando la determinación es baja, preservando las puntuaciones puras de las fuentes neuronales/de decodificación. La puntuación de fiabilidad final $p(r)$ se calcula mediante una función logística con regularización $\ell_2$.

Contribuciones Clave

1. Distinción Conceptual: El trabajo distingue la simbolizabilidad textual de la determinación semántica, proporcionando una base principled para determinar cuándo la evidencia derivada del verificador es informativa. Argumentan que la cobertura de parseo por sí sola es insuficiente porque no tiene en cuenta las afirmaciones no resueltas o bloqueadas.
2. Marco Técnico: SymboUQ introduce un flujo de tres etapas (Auditor de Diseño, Perfil de Determinación, DARC) que maneja explícitamente los regímenes de "desconocido" y "no evaluable" de la verificación formal, integrándolos con señales neuronales.
3. Rendimiento Empírico: El marco demuestra mejoras consistentes sobre bases sólidas en diversos benchmarks de razonamiento espacial y diferentes backbones de LLM.

Resultados Experimentales

Los autores evaluaron SymboUQ en cinco benchmarks de razonamiento espacial (StepGame, SpaRTQA, SpaRTUN, SpaceNLI, SpaRP) utilizando cuatro backbones de LLM congelados (Mistral-7B, Llama-3.1-8B, Gemma-2-9B, Qwen3-8B).

• Rendimiento: SymboUQ logró el mejor rendimiento general en el ranking de trazas (AUROC) y en la estimación de probabilidad (pérdida Brier balanceada por clase). Mostró una mejora relativa promedio del 8% en AUROC y una reducción relativa del 7% en la pérdida Brier balanceada por clase en comparación con la base externa más fuerte.
• Estudios de Ablación:
  • Conciencia de Aplicabilidad: Eliminar las interacciones conscientes de la determinación (usando solo apilamiento de puntuaciones) resultó en una caída de rendimiento de 0.032–0.052 en AUROC, confirmando que condicionar la aplicabilidad es crítico.
  • Determinación vs. Cobertura de Parseo: El análisis mostró que la separación de la puntuación de restricciones aumenta monótonamente con la determinación semántica, pero no con la cobertura de parseo, validando que la determinación es un mejor caracterizador de la utilidad del verificador.
  • Semántica del Contexto: El uso de un "contexto asumido" (permitiendo hipótesis no verificadas) en lugar de un "contexto fundamentado" estrictamente proporcionó ganancias significativas, ya que permite al sistema detectar autocontradicciones dentro de la cadena generada.
• Eficiencia: El método es computacionalmente eficiente, procesando aproximadamente 159 trazas por segundo con un pequeño número de parámetros entrenables (8.13M) y requiriendo solo un corto tiempo de entrenamiento (9 minutos) en el conjunto de validación del objetivo.

Significancia

El artículo afirma que SymboUQ aborda una brecha crítica en la estimación de la fiabilidad de los LLM: la desconexión entre la capacidad de parsear una afirmación y la capacidad de resolverla semánticamente. Al tratar los resultados de "desconocido" y "no evaluable" como distintos de "contradicho" y al modelar explícitamente la pérdida de evidencia debido a la infactibilidad del contexto, el marco proporciona una medida más fiel de la aplicabilidad del verificador. Los resultados sugieren que, para el razonamiento espacial, la estimación de la fiabilidad se beneficia significativamente de la integración de señales de verificación formal con señales neuronales, siempre que la integración esté condicionada a la determinación semántica de la traza y no meramente a su parseabilidad. El trabajo establece que la cuantificación de la incertidumbre simbólica puede aplicarse eficazmente a trazas de razonamiento de formato libre sin requerir etiquetas de verdad para los pasos intermedios durante el proceso de auditoría.