Resumen Técnico: ForEx – Un Marco de Verificación Formal para el Razonamiento Explicable en la Detección de Falacias Lógicas

1. Declaración del Problema

Las evaluaciones actuales de los Modelos de Lenguaje de Gran Escala (LLM) en la detección de falacias lógicas dependen predominantemente de la precisión de la predicción (corrección de la etiqueta). Sin embargo, este enfoque no logra verificar si el razonamiento proporcionado por el modelo realmente respalda la etiqueta predicha. Las predicciones correctas pueden derivarse de correlaciones superficiales en lugar de una verdadera derivación lógica, mientras que las predicaciones incorrectas podrían estar acompañadas de un razonamiento que es formalmente sólido bajo una interpretación específica, pero que diverge de las anotaciones humanas.

Además, los enfoques simbólicos existentes (por ejemplo, NL2FOL) suelen formalizar el argumento de entrada para comprobar su satisfacibilidad, en lugar de formalizar la cadena de razonamiento generada por el modelo. Adicionalmente, las prácticas de anotación estándar suelen comprimir las variaciones interpretativas en etiquetas "doradas" únicas, lo que puede oscurecer lecturas alternativas plausibles de un argumento. Existe una falta de un marco que analice conjuntamente las etiquetas predichas, las explicaciones generadas y la derivabilidad formal de dichas explicaciones.

2. Metodología: El Marco ForEx

Los autores proponen ForEx (Formal Verification for Explainable Reasoning), un marco que traduce las explicaciones en lenguaje natural generadas por LLM a Lean4 (un asistente de pruebas formal) para verificar si el razonamiento traducido es derivable bajo premisas codificadas. El flujo de trabajo consta de tres etapas:

A. Generación de Candidatos de Razonamiento

Un modelo "Reasoner" recibe una declaración de entrada y genera hasta $k$ candidatos. Cada candidato es una tupla $(f_i, a_i, s_i)$ que contiene:

• $f_i$: El tipo de falacia lógica predicha.
• $a_i$: La explicación en lenguaje natural (razonamiento).
• $s_i$: La estructura en Lean4 que formaliza la explicación.

Un "Modifier" convierte $s_i$ en código Lean4 inicial.

B. Retroalimentación de Ejecución y Verificación en Lean4

Esta etapa emplea un bucle de reparación iterativo para asegurar que el código Lean4 generado compile:

1. Intento de Compilación: El "Executor" intenta compilar el código Lean4.
2. Bucle de Retroalimentación: Si la compilación falla (estado F), el Executor recibe el mensaje de error y la explicación original $a_i$ para revisar el código.
3. Restricciones: Las revisiones están estrictamente limitadas a la explicación original y al código inicial para evitar la deriva semántica; el Executor no puede introducir nuevo contenido lógico.
4. Terminación: El bucle continúa hasta que el código compila con éxito (estado T) o se agota el máximo de iteraciones de reparación ($iter_{max}$).

C. Evaluación de Consistencia de Etiquetas

El marco introduce la Matriz de Verificación de Argumentos de LLM para desacoplar la corrección de la etiqueta de la situación de verificación formal. La matriz clasifica las salidas en cuatro cuadrantes basados en dos ejes:

1. Verificación en Lean4: Pasa (compila) vs. Falla (no compila).
2. Consistencia de Etiqueta: Coincidencia (la predicción es igual a la anotación humana) vs. Desajuste.

Las cuatro categorías resultantes son:

• Compilable-Correcto (CC): Pasa y Coincide.
• Compilable-Alternativo (CA): Pasa y Desajuste (indica una cadena de razonamiento formalmente válida que respalda una etiqueta diferente de la anotación humana).
• No Compilable-Correcto (UC): Falla y Coincide.
• No Compilable-Incorrecto (UI): Falla y Desajuste.

D. Pipeline de Anotación Guiado por Consenso

Para abordar la ambigüedad de la anotación, los autores proponen un pipeline que:

1. Representa los modelos y las anotaciones humanas como vectores multi-hot sobre categorías de falacias.
2. Utiliza el Análisis de Componentes Principales (PCA) y la distancia de Mahalanobis para identificar y filtrar modelos atípicos (outliers).
3. Calcula distancias de Jaccard por pares para identificar declaraciones de "alto consenso" (bajo desacuerdo).
4. Aumenta las anotaciones para las declaraciones de alto consenso si al menos el 50% de los modelos retenidos asignan una etiqueta específica bajo verificación formal.

3. Contribuciones Clave

1. Marco ForEx: Un sistema novedoso que traduce las explicaciones generadas por LLM a Lean4, permitiendo el análisis verificable por máquina de cadenas de razonamiento formalizadas en lugar de solo argumentos de entrada.
2. Matriz de Verificación de Argumentos de LLM: Una métrica que separa la consistencia de la etiqueta del estatus de verificación formal, exponiendo casos donde los modelos proporcionan un razonamiento formalmente derivable que contradice las etiquetas humanas existentes (la categoría "Compilable-Alternativo").
3. Pipeline de Anotación Guiado por Consenso: Un método que combina estándares humanos, acuerdo entre múltiples LLM y verificación formal para apoyar el análisis de anotación y el aumento conservador de etiquetas, tratando el desacuerdo en la anotación como una señal de variación interpretativa en lugar de ruido.

4. Resultados Experimentales

El marco fue evaluado en el conjunto de datos LOGIC-Climate (1,074 instancias, 13 categorías de falacias), utilizando un subconjunto muestreado del 10% y 15 modelos de Reasoner diferentes (incluyendo variantes con y sin procesos de pensamiento/thinking).

• Éxito de Compilación: La tasa de aprobación promedio para la compilación en Lean4 aumentó del 36.70% (inicial) al 98.65% después de cuatro iteraciones de reparación. La mayor parte de las ganancias ocurrieron tras la primera iteración.
• Verificación vs. Acuerdo de Etiquetas:
  • La tasa combinada de Compilable-Correcto (CC) + Compilable-Alternativo (CA) fue consistentemente alta, superando el 90% para la mayoría de los modelos (alcanzando un máximo de 97.59%). Esto indica que la gran mayoría de las salidas de los LLM pueden traducirse en cadenas de razonamiento formal que pasan la verificación.
  • Sin embargo, la tasa CC (acuerdo con las etiquetas humanas) fue significativamente menor, situándose aproximadamente entre el 17% y el 23% en los mejores modelos.
  • La tasa CA fue dominante, sugiriendo que muchas cadenas de razonamiento formalmente verificadas respaldan etiquetas distintas de las anotaciones humanas.
• Análisis de Errores:
  • Las tasas de No Compilable-Correcto (UC) fueron muy bajas (<2%), lo que indica que las etiquetas correctas rara vez surgen sin una cadena de razonamiento verificable en este entorno.
  • Los fallos de No Compilable-Incorrecto (UI) se debieron a menudo a predicciones de "Sin Falacia" (NF), potencialmente causadas por la falta de contexto en entradas de una sola oración aislada.
• Aumento de Anotación: El pipeline guiado por consenso identificó un subconjunto de declaraciones de alto consenso. Las anotaciones aumentadas lograron un 0.77 de recall respecto a las anotaciones humanas originales, preservando la mayoría de las etiquetas originales mientras añadían alternativas soportadas formalmente.

5. Significancia y Reivindicaciones

El artículo afirma que ForEx mueve la evaluación de los LLM más allá de la simple corrección de etiquetas hacia un análisis de cadenas de razonamiento formalizadas verificable por máquina.

• Brecha Sistemática: Los resultados exponen una brecha sistemática entre la derivabilidad formal y el acuerdo de etiquetas. La alta prevalencia de salidas "Compilable-Alternativo" sugiere que las anotaciones humanas existentes pueden no capturar plenamente las interpretaciones plausibles de los argumentos de entrada, o que los modelos están razonando correctamente bajo diferentes supuestos.
• Más allá de la Predicción: El marco demuestra que un modelo puede proporcionar una cadena de razonamiento que es formalmente válida (derivable bajo las premisas codificadas) incluso si discrepa de la etiqueta "dorada". Esta distinción es invisible para las métricas estándar basadas en la predicción.
• Utilidad de la Anotación: ForEx se presenta no solo como una herramienta de verificación, sino como un mecanismo para el análisis de anotación downstream. Puede identificar casos donde las etiquetas doradas podrían ser insuficientes o donde existen múltiples interpretaciones válidas, apoyando el aumento de los conjuntos de datos con etiquetas alternativas basadas en el consenso.

Los autores mantienen la modestia respecto a las implicaciones, señalando que la verificación formal en Lean4 certifica la derivabilidad bajo premisas codificadas, pero no garantiza la alineación semántica con la declaración original en lenguaje natural. Reconocen que el lenguaje natural carece de una base semántica totalmente especificada y, por lo tanto, los resultados formales pueden sobreestimar la capacidad del modelo si la formalización misma es imperfecta. Se propone trabajo futuro para mejorar la alineación entre los resultados de verificación y la corrección semántica mediante la incorporación de estructuras de argumento más ricas e información contextual.