Resumen Técnico: SymDiag – Diagnóstico Explicable para el Razonamiento de LLM mediante Verificación Neuro-Simbólica

1. Planteamiento del Problema

Los Modelos de Lenguaje de Gran Escala (LLMs) han demostrado una fuerte capacidad de razonamiento de múltiples pasos, pero sus Cadenas de Pensamiento (CoT) suelen sufrir una brecha crítica entre la corrección del resultado y la validez del proceso. Un modelo puede llegar a la respuesta correcta a través de pasos intermedios infieles, que incluyen lógica inconsistente, suposiciones ocultas o transformaciones que no implican lógicamente la conclusión.

Los métodos de verificación existentes no proporcionan los conocimientos diagnósticos necesarios para una reparación dirigida:

• Verificación basada solo en el resultado (Coincidencia de Respuesta): Solo puede detectar si la respuesta final es correcta o incorrecta, fallando al localizar errores en derivaciones largas o al identificar trazas que son correctas pero infieles.
• LLM-como-Juez (LLM-as-Judge): Proporciona críticas en lenguaje natural que son subjetivas, inconsistentes y difíciles de auditar o convertir en acciones de reparación específicas.
• Recompensas Escalares (PRMs/RMs): Reducen modos de fallo ricos a una única puntuación, ofreciendo poca guía sobre dónde o por qué falló una derivación.
• Enfoques Neuro-Simbólicos: Aunque métodos como Logic-LM o SymbCoT introducen estructuras simbólicas, a menudo tienen dificultades para distinguir entre defectos de razonamiento genuinos y artefactos de traducción neuro-simbólica (p. ej., ruido de parseo). Sin esta distinción, los verificadores pueden "diagnosticar erróneamente" errores de traducción como fallos lógicos, lo que conduce a un feedback poco fiable.

El desafío central es pasar de la mera puntuación o el juicio subjetivo hacia un diagnóstico de fallos estructurado que localice los errores, atribuya sus causas y produzca evidencia verificable para la reparación.

2. Metodología: Marco de Trabajo SymDiag

SymDiag es un marco neuro-simbólico de dos etapas diseñado para replantear la verificación del razonamiento como un problema de diagnóstico de fallos explicable.

Etapa I: Diagnóstico de Fallos Explicable

Esta etapa transforma la CoT de lenguaje natural en restricciones simbólicas verificables y realiza la validación a nivel de paso.

1. Generador Neuro-Simbólico (Codificación de Doble Rama):
   Para mitigar la fragilidad de la traducción, el sistema genera dos codificaciones simbólicas independientes para cada paso de la CoT:

   • Rama de Traducción Formal: Compila el problema de entrada y la CoT en una representación formal (usando Prolog como backend), normalizando entidades, predicados y relaciones.
   • Rama de Reexpresión Crítica: Reexpresa el paso de la CoT en una declaración con un alcance más estricto y explícito para exponer suposiciones ocultas antes de compilarla en un segundo programa simbólico.
   • Objetivo: Las codificaciones duales reducen el sesgo de traducción de vía única y aumentan la robustez ante la variabilidad de la paráfrasis.

2. Auto-Auditor (Desentrelazamiento de Errores):
   Un componente crítico que distingue entre Errores de Traducción (artefactos de la conversión de neuro a simbólico) y Errores de Razonamiento (defectos lógicos genuinos).

   • Verificación de Consistencia de Traducción: Compara hechos y restricciones entre las dos ramas. Las divergencias grandes sugieren ambigüedad de traducción.
   • Verificación de Crítica Lógica: Ejecuta pruebas de sanidad ligeras (p. ej., contradicciones inmediatas). Si un fallo desaparece bajo reescrituras mínimas y consistentes con el texto (p. ej., renombramiento de variables), se atribuye a la traducción y no al razonamiento.
   • Salida: Una atribución binaria ($ErrorDeTraducción$ vs. $ErrorDeRazonamiento$) que filtra diagnósticos erróneos espurios.

3. Verificación Simbólica a Nivel de Paso:
   Los estados simbólicos aprobados se someten a controles rigurosos:

   • Satisfacibilidad: Verifica si las premisas y restricciones acumuladas son satisfactorias ($SAT(P_i \land C_i)$).
   • Implicación Local: Verifica si la afirmación del paso actual se sigue lógicamente de las premisas previas ($P_{i-1} \land C_{i-1} \models \phi_i$). Esto se operacionaliza mediante la comprobación de la insatisfacibilidad de la negación.
   • Generación de Evidencia: Ante un fallo, el sistema genera evidencia verificable como contraejemplos, testigos de inconsistencia (núcleos insatisfechos/unsat cores) e indicadores de premisas faltantes.

Etapa II: Reparación Guiada por el Diagnóstico

La salida diagnóstica se convierte en feedback accionable para el LLM:

• Localización: Identifica los índices específicos que fallan en la CoT.
• Atribución: Asigna etiquetas de error (p. ej., error aritmético, inferencia inválida, premisa faltante).
• Estrategia de Reparación:
  • Parche Local: Si el defecto es aislado (p. ej., un error de cálculo), se le pide al modelo que edite mínimamente el paso específico.
  • Reescritura Global: Si el fallo se propaga (p. ej., una premisa faltante que afecta pasos posteriores), se le pide al modelo que reescriba el razonamiento desde el primer punto de fallo.

3. Contribuciones Clave

1. Perspectiva Centrada en el Diagnóstico: Formaliza la verificación del razonamiento como un problema de diagnóstico de fallos, con el objetivo de localizar errores, atribuir causas y apoyar la reparación dirigida, en lugar de simplemente puntuar resultados.
2. Desentrelazamiento Auto-Auditado: Introduce un mecanismo para separar explícitamente los artefactos de traducción de los fallos de razonamiento genuinos mediante codificaciones simbólicas duales y comprobaciones de consistencia entre ramas, permitiendo un diagnóstico fiable bajo observabilidad parcial.
3. Pipeline Basado en Evidencia: Propone un sistema de bucle cerrado que produce evidencia diagnóstica verificable (contraejemplos, núcleos insatisfechos) para guiar la reparación iterativa, mejorando significativamente la corrección del razonamiento de múltiples rondas.
4. Benchmark Diagnóstico Transversal de Dominios: Construye un conjunto de datos unificado que abarca matemáticas (AIME), razonamiento lógico (AR-LSAT), razonamiento científico (GPQA) y razonamiento general (MMLU), demostrando que diversos errores de razonamiento pueden analizarse dentro de un marco simbólico compartido.

4. Resultados Experimentales

Los experimentos se realizaron sobre un conjunto de oro auditado manualmente de 240 instancias a través de cuatro dominios.

• Detección de Fidelidad: SymDiag logró el F1 score general más alto (70.7) en la detección de razonamiento infiel, superando significativamente a Answer Matching, LLM-as-Judge, Reward Models y LogicReward. La brecha de rendimiento fue particularmente pronunciada en los benchmarks de razonamiento lógico y general donde las respuestas correctas suelen enmascarar pasos intermedios inválidos.
• Reparación de Razonamiento: En tareas de reparación de múltiples rondas, SymDiag demostró ganancias de precisión más rápidas y sostenidas en comparación con las líneas base. Mientras que Answer Matching proporcionó una mejora mínima debido a la falta de guía localizada, y el feedback de LLM-as-Judge se saturó rápidamente debido a su imprecisión, los diagnósticos de SymDiag, a nivel de paso y basados en evidencia, permitieron correcciones dirigidas.
• Estudios de Ablación: Eliminar el Auto-Auditor o la verificación simbólica a nivel de paso causó caídas significativas en el rendimiento, confirmando que el éxito del sistema depende de la interacción entre la robustez de la traducción y la comprobación lógica explícita.
• Análisis de Atribución de Errores: SymDiag reveló distintos modos de fallo según la escala de los modelos. Los modelos más pequeños (p. ej., 1B parámetros) cometieron frecuentemente errores aritméticos y omitieron premisas, mientras que los modelos más grandes (p. ej., 20B) mostraron menos errores de bajo nivel pero una mayor incidencia de reglas alucinadas y desajustes de tipos.

5. Significación y Reivindicaciones

El artículo posiciona a SymDiag no simplemente como un "mejor verificador" o una "mejor señal de recompensa", sino como un sistema de diagnóstico neuro-simbólico explicable. Su principal significación radica en:

• Confiabilidad: Al proporcionar evidencia verificable (contraejemplos, testigos de inconsistencia) en lugar de puntuaciones subjetivas, ofrece una base fundamentada para diagnosticar el razonamiento de los LLM.
• Escalabilidad: El marco está diseñado para manejar diversos dominios de razonamiento (matemáticas, lógica, ciencia, general) dentro de un marco de diagnóstico simbólico unificado.
• Accionabilidad: A diferencia de otros métodos que devuelven una puntuación o una traza corregida, SymDiag localiza los fallos y los atribuye a causas específicas (traducción vs. razonamiento), permitiendo reparaciones dirigidas que son más efectivas para la mejora iterativa.

Los autores concluyen que, aunque los modelos base más fuertes mejoran la calidad de la traducción, el pipeline neuro-simbólico estructurado de SymDiag sigue siendo robusto a través de las escalas de los modelos, ofreciendo un camino escalable hacia un diagnóstico de razonamiento confiable.