Resumen Técnico: Reparación de FOLIO y MALLS

Declaración del Problema

La traducción de Lenguaje Natural (NL) a Lógica de Primer Orden (FOL) es un componente crítico de la IA neurosimbólica y la Inferencia de Lenguaje Natural (NLI). Sin embargo, la calidad de los benchmarks existentes utilizados para entrenar y evaluar estos sistemas no ha sido auditada rigurosamente. Este artículo identifica que los conjuntos de datos ampliamente utilizados, específicamente FOLIO y MALLS, contienen errores significativos de anotación y ambigüedades en sus etiquetas de verdad fundamental (ground truth). Estos errores distorsionan la evaluación de los Modelos de Lenguaje de Gran Escala (LLMs) de vanguardia, lo que conduce a métricas de rendimiento inexactas. Además, la revisión manual exhaustiva de grandes conjuntos de datos es prohibitivamente costosa y no escala, lo que requiere un método más eficiente para la curación de conjuntos de datos.

Metodología

1. Auditoría y Corrección Humana Sistemática

Los autores llevaron a cabo una inspección humana sistemática de la división de validación de FOLIO (275 instancias) y de un subconjunto del conjunto de prueba de MALLS (100 instancias). Dos revisores experimentados (estudiante de doctorado y miembro investigador) anotaron los datos de forma independiente, cotejaron los resultados y resolvieron los conflictos mediante consenso.

• Manejo de la Ontología: Dado que los conjuntos de datos carecen de ontologías explícitas, los autores extrajeron firmas (predicados, aridades, constantes) de las fórmulas FOL y utilizaron un LLM para asignar significados en lenguaje natural, seguido de una verificación manual. Distinguieron entre inconsistencias (significados/aridades conflictivas), que fueron corregidas, y laxitud ontológica (convenciones no convencionales pero consistentes), que se preservaron para evitar la reescritura de todo el conjunto de datos.
• Clasificación de Errores: La auditoría categorizó los errores en:
  • Errores Sintácticos: Desajustes de paréntesis, erratas, uso indebido de la ontología (10.5% en FOLIO, 3% en MALLS).
  • Errores Semánticos: Fórmulas válidas que representan erróneamente el significado de NL, incluyendo errores de alcance de cuantificadores e información faltante (28.3% en FOLIO, 33% en MALLS).
  • Ambigüedades: Oraciones en NL que admiten múltiples formalizaciones no equivalentes pero defendibles (16.4% en FOLIO, 48% en MALLS).
  • Inconsistencias de Etiquetas de NLI: Etiquetas (Verdadero/Falso/Desconocido) inconsistentes con las formalizaciones proporcionadas (8.4% en FOLIO).
• Grupo de Control: Los autores también revisaron 213 instancias del conjunto de datos GGC (Barker-Plummer et al., 2011b), un corpus de alta calidad validado por instructores, para verificar que su marco de curación no introduce ruido en datos que ya son correctos.

2. Marco de Supervisión Asistido por LLM

Para abordar el problema de la escalabilidad de la revisión manual, los autores proponen un marco que utiliza LLMs para priorizar el esfuerzo humano.

• Tarea de Veredicto y Refinamiento (V&R): Un LLM tiene la tarea de evaluar un triplete $(p, \Omega, \phi)$, donde $p$ es una oración en NL, $\Omega$ es una ontología y $\phi$ es una fórmula candidata de FOL. El LLM produce:
  1. Un veredicto $v \in \{yes, no, ?\}$ (correcto, incorrecto o ambiguo/incierto).
  2. Un refinamiento $\psi$ (una fórmula corregida si $v \neq yes$).
• Pipelines: Se probaron dos diseños de pipeline:
  • Pipeline 1 (V&R Directo): El LLM juzga la fórmula original $\phi$ directamente.
  • Pipeline 2 (Regeneración): El LLM primero genera un nuevo candidato $\hat{\phi}$ a partir de $p$ y $\Omega$, y luego juzga este nuevo candidato.
• Estrategia de Priorización: El marco aprovecha el hallazgo empírico de que los LLM rara vez marcan formalizaciones correctas como incorrectas (tasa de falsos positivos $\approx 3\%$ en FOLIO). Al dirigir a los revisores humanos a las instancias marcadas como "no" (incorrecto) o "?" (ambiguo) primero, el marco busca maximizar las ganancias de precisión por unidad de esfuerzo humano.

Contribuciones Clave

1. Conjuntos de Datos Corregidos: Los autores lanzaron versiones revisadas de las verdades fundamentales para la división de validación de FOLIO y un subconjunto de prueba de MALLS, corrigiendo el 39% y el 36% de las entradas respectivamente, junto con las etiquetas de NLI corregidas cuando correspondía.
2. Análisis de Impacto en la Evaluación: El artículo demuestra que los errores de anotación penalizan significativamente la evaluación de los modelos. La reevaluación de tres LLMs de vanguardia (Gemma 4 31B-it, Qwen3-30B-A3B, GPT-4o-mini) contra las verdades fundamentales corregidas resultó en ganancias de precisión que oscilan entre +9 y +22 puntos porcentuales.
3. Marco de Supervisión Asistido por LLM: Una estrategia novedosa que reduce el costo de la curación de conjuntos de datos. Al centrar la revisión humana en el subconjunto de instancias marcadas como propensas a errores por el LLM, el marco logra una precisión del conjunto de datos del 90% tras revisar solo el 24% de las instancias de FOLIO y el 13% de las de MALLS. Esto representa una reducción sustancial en comparación con la revisión aleatoria no guiada, que requiere más del 70% de las instancias para alcanzar la misma precisión.

Resultados

• Tasas de Error: La auditoría humana confirmó que aproximadamente el 39% de las instancias de FOLIO y el 36% de las de MALLS contienen formalizaciones FOL incorrectas. Además, el 16.4% de FOLIO y el 48% de MALLS contienen oraciones en NL ambiguas.
• Cambios en el Rendimiento: Al ser probados en los conjuntos de datos curados, todos los modelos evaluados mostraron una mejora en la precisión de la traducción. Por ejemplo, Gemma 4 31B-it experimentó un aumento de +21.8% en FOLIO (todas las instancias) y de +18.0% en MALLS.
• Eficiencia de la Supervisión:
  • El Pipeline 1 superó al Pipeline 2 y a los métodos de base (revisión aleatoria de datos originales o regenerados) en todas las métricas (Área bajo la curva, $T_{90}$, $T_{95}$).
  • Utilizando el orden de priorización (salidas malformadas $\to$ ? $\to$ no $\to$ sí), el marco alcanzó un 90% de precisión con un esfuerzo humano mínimo (24% para FOLIO, 13% para MALLS).
  • En el conjunto de datos de alta calidad GGC, el marco introdujo un ruido insignificante (degradación $\le 5\%$), confirmando su fiabilidad cuando se aplica a datos que ya son mayoritariamente correctos.

Significado y Reivindicaciones

El artículo sostiene que la calidad de los benchmarks de NL-a-FOL ha sido una "caja negra" que ha distorsionado la evaluación de los sistemas de IA neurosimbólica. Al proporcionar verdades fundamentales corregidas, los autores demuestran que las estimaciones de rendimiento previas estaban artificialmente suprimidas por el ruido de anotación.

El marco asistido por LLM propuesto ofrece una solución práctica al problema de "escalabilidad" de la curación de conjuntos de datos. Demuestra que es posible lograr conjuntos de datos de alta calidad sin el costo prohibitivo de una revisión humana exhaustiva. Los autores posicionan este marco como una herramienta para:

1. Curación de Conjuntos de Datos: Permitiendo a los curadores centrarse exclusivamente en las instancias sospechosas.
2. Métodos Formales: Actuando como una capa de advertencia para expertos que revisan especificaciones en NL.
3. Verificación en Tiempo de Ejecución: Proporcionando retroalimentación inmediata sobre si las fórmulas generadas capturan los requisitos previstos en escenarios donde la revisión manual es imposible.

Los autores liberan los conjuntos de datos corregidos y el código del marco para apoyar la reproducibilidad, al tiempo que señalan que las conclusiones son específicas para los conjuntos de datos y LLMs probados y pueden requerir adaptación para otros formalismos lógicos o dominios.