Delta1 with LLM: symbolic and neural integration for credible and explainable reasoning

Este trabajo presenta un pipeline neuro-simbólico que integra el generador de teoremas determinista Delta1 con modelos de lenguaje grandes (LLM) para producir razonamientos explicables, auditables y alineados con el dominio mediante la construcción automática de demostraciones lógicas y su verbalización en lenguaje natural.

Lo esencial

Imagina que quieres construir un edificio muy seguro, pero tienes dos arquitectos muy diferentes trabajando en el proyecto:

1. El Arquitecto Lógico (∆1): Es un robot extremadamente preciso, estricto y aburrido. Sigue las reglas de la física y las matemáticas al pie de la letra. Si hay un error en los planos, él lo detecta al instante y te dice: "Aquí hay un conflicto". Pero tiene un problema: solo habla en código binario y fórmulas matemáticas. No sabe explicar por qué el edificio se va a caer, solo sabe decirte que se va a caer.
2. El Arquitecto Creativo (LLM): Es un humano muy talentoso, elocuente y capaz de hablar con cualquier persona. Puede describir el edificio con palabras bonitas, contar historias sobre cómo se usará y explicar los problemas de forma que todos entiendan. Pero, a veces, se equivoca en los cálculos o inventa cosas que no son ciertas porque quiere que la historia suene bien.

El problema: Si usas solo al robot, nadie entiende el reporte. Si usas solo al humano, el edificio podría colapsar porque sus explicaciones no son matemáticamente correctas.

La solución de este papel (∆1 + LLM):
Los autores de este artículo han creado un equipo perfecto donde estos dos arquitectos trabajan juntos en una sola cadena de montaje. Lo llaman "Explicabilidad por Construcción".

¿Cómo funciona? (La analogía del Detective y el Traductor)

Imagina que tienes un montón de reglas para un hospital, un contrato legal o una ley de tráfico. A veces, estas reglas entran en conflicto (por ejemplo: "Si tienes fiebre, toma medicina" vs. "Si tienes fiebre, no tomes medicina").

1. Paso 1: El Traductor (LLM): Primero, el modelo de lenguaje (el humano) lee las reglas en español y las convierte en "bloques de construcción" lógicos simples (como: Si A, entonces B).
2. Paso 2: El Detective Matemático (∆1): Estos bloques pasan al robot ∆1. Este robot no "adivina" ni busca al azar. Usa una fórmula mágica llamada Contradicción Triangular Estándar Completa (FTSC).
   • Piensa en esto como un juego de dominó. El robot coloca todas las fichas de dominó de una manera específica. Si el sistema es inconsistente, el robot sabe exactamente qué ficha, si la quitas, hace que todo el sistema deje de caer.
   • Lo genial es que el robot encuentra todas las formas posibles en que las reglas pueden chocar, de manera rápida y garantizada. No se equivoca.
3. Paso 3: El Explicador (LLM de nuevo): Una vez que el robot encuentra el conflicto exacto (la ficha que causa el problema), lo pasa de nuevo al modelo de lenguaje.
   • El LLM toma ese dato matemático frío y dice: "¡Ah! El problema es que la regla de 'tomar medicina' choca con la de 'no tomar medicina' si el paciente tiene fiebre. Para arreglarlo, deberíamos añadir una condición: 'solo si la fiebre es alta'".

¿Por qué es especial?

• Sin adivinanzas: La mayoría de las inteligencias artificiales actuales "adivinan" la respuesta basándose en patrones. Este sistema garantiza que la lógica es correcta. Es como tener un sello de aprobación oficial en cada explicación.
• Explicaciones reales: No solo te dice "hay un error". Te dice cuál es el error mínimo necesario para arreglarlo y te da una sugerencia en lenguaje natural para solucionarlo.
• Transparencia total: Puedes seguir el rastro de cada paso. Desde la regla original hasta la explicación final, todo está conectado por una cadena de verdad matemática.

Ejemplos de la vida real que menciona el papel:

• En Medicina: Si un sistema dice "Si el paciente tiene infección, necesita antibióticos" y "Si tiene infección, no necesita antibióticos", el sistema detecta el conflicto y sugiere: "Necesitamos especificar qué tipo de infección es".
• En Contratos: Si un contrato dice "El proveedor debe entregar a tiempo" y "El cliente puede cancelar sin causa si hay retraso", pero también "El proveedor es exclusivo y no puede ser cancelado", el sistema ve el nudo y sugiere cómo desatarlo legalmente.
• En Leyes: Detecta cuando una ley de privacidad de un país choca con una ley de protección de datos de otro país.

En resumen

Este papel presenta una nueva forma de hacer Inteligencia Artificial que combina la fuerza de las matemáticas (para asegurar que no mentimos) con la suavidad del lenguaje (para asegurar que nos entienden).

Es como tener un juez infalible (el robot) que dicta la sentencia exacta, y un abogado experto (el LLM) que se la explica al cliente de forma que pueda entenderla y saber cómo arreglar su problema. Juntos, crean un sistema donde la verdad y la explicación van de la mano, construyendo confianza en la IA.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "∆1–LLM: Symbolic–Neural Integration for Credible and Explainable Reasoning", presentado en español:

1. El Problema

El razonamiento neuro-simbólico actual enfrenta una dicotomía fundamental:

• Enfoques Simbólicos (Lógica): Ofrecen rigor formal, corrección demostrable (soundness) y estructuras de inferencia transparentes, pero carecen de expresividad lingüística y dificultad para interactuar con humanos en lenguaje natural.
• Enfoques Neuronales (LLMs): Proporcionan fluidez, adaptabilidad y capacidad de generar explicaciones coherentes, pero carecen de garantías de corrección, son estocásticos y sus procesos de razonamiento son a menudo "cajas negras" no verificables.

Existe una necesidad crítica de un marco que unifique la validez lógica formal con la explicabilidad en lenguaje natural, permitiendo sistemas que sean tanto verificables por máquinas como comprensibles por humanos, especialmente en dominios de alto riesgo como la salud, el cumplimiento normativo y la gestión de contratos.

2. Metodología: El Marco ∆1 + LLM

Los autores proponen un pipeline de extremo a extremo llamado "Explicabilidad por Construcción" (Explainability-by-Construction), que integra dos componentes principales:

A. El Generador de Teoremas Automático ∆1 (Capa Simbólica)

• Base Teórica: Se fundamenta en la Contradicción Estándar Triangular Completa (FTSC - Full Triangular Standard Contradiction).
• Funcionamiento:
  • ∆1 opera de manera determinista (sin búsqueda estocástica ni retroceso).
  • Dado un conjunto de $n$ literales de entrada (predicados atómicos), construye un conjunto de cláusulas $S$ que forma una FTSC.
  • Genera automáticamente $n!$ teoremas no redundantes y no equivalentes.
  • Para cada cláusula $C$ en el conjunto, demuestra que $S \setminus \{C\} \vdash \neg C$. Esto significa que al eliminar una cláusula, el resto del conjunto la refuta, identificándola como una fuente de contradicción mínima.
• Garantías:
  • Corrección (Soundness): Los teoremas son válidos por construcción.
  • Minimalidad: Identifica conjuntos de cláusulas insatisfacibles mínimos (MUS - Minimal Unsatisfiable Subsets).
  • Complejidad: La generación de un conjunto de cláusulas canónico opera en $O(n^3)$, y la enumeración total es $O(n \cdot n!)$, pero cada teorema es mínimo y no requiere verificación externa.
  • Trazabilidad: Produce una "traza de prueba" explícita y reproducible.

B. La Capa de LLM (Capa Neural)

• Función: Actúa como un intérprete semántico.
• Proceso:
  1. Extracción de Predicados: Convierte el texto natural de entrada en predicados lógicos formales (sintaxis tipo TPTP).
  2. Verbalización: Traduce las trazas de prueba formales de ∆1 en explicaciones en lenguaje natural coherentes.
  3. Ranking y Recomendación: Prioriza los teoremas según su relevancia contextual y sugiere "remedios" o correcciones específicas para resolver las contradicciones detectadas.

Flujo de Trabajo

1. Entrada: Texto natural (ej. políticas médicas, contratos).
2. Procesamiento LLM: Extracción de predicados atómicos ($L = \{x_1, ..., x_n\}$).
3. Generación ∆1: Construcción determinista de la FTSC y generación de teoremas de contradicción mínima.
4. Salida LLM: Explicación humana de por qué ocurre la contradicción y sugerencias de reparación (ej. "Añadir un criterio de calificación", "Modificar una cláusula").

3. Contribuciones Clave

1. Pipeline de Integración Neuro-Simbólica: Un marco que acopla la generación de teoremas determinista de ∆1 con las capacidades interpretativas de los LLMs, logrando tanto corrección formal como interpretabilidad a nivel humano.
2. Justificación Teórica y Validación Empírica: Demostración de que ∆1 + LLM proporciona corrección formal y explicabilidad en dominios de alto riesgo, superando las limitaciones de los sistemas puramente estocásticos o puramente simbólicos opacos.
3. Explicabilidad por Construcción: A diferencia de la interpretabilidad post-hoc (explicar después de generar), este sistema garantiza que cada explicación esté fundamentada en una traza de prueba determinista y verificable desde el momento de la generación.
4. Nuevo Paradigma de Descubrimiento: Presenta a ∆1 como un "motor de descubrimiento" formalmente garantizado que genera un universo de teoremas mínimos y ortogonales, sirviendo como un estándar de referencia ("TPTP para la explicabilidad") para evaluar la coherencia lógica en IA.

4. Resultados y Estudios de Caso

El marco fue evaluado en dominios de lógica proposicional y de primer orden, mostrando resultados en:

• Razonamiento Médico:
  • Escenario: Reglas sobre infecciones, recuento de glóbulos blancos, fiebre y antibióticos.
  • Resultado: ∆1 identificó contradicciones mínimas (ej. la imposibilidad de que todas las condiciones se cumplan simultáneamente sin restricciones). El LLM tradujo esto a guías clínicas accionables, como la necesidad de confirmar la infección antes de prescribir antibióticos automáticamente.
• Gestión de Cumplimiento y Regulación:
  • Escenario: Conflictos entre políticas de privacidad, transparencia y leyes de protección de datos (GDPR vs. HIPAA).
  • Resultado: El sistema detectó incompatibilidades lógicas entre obligaciones legales (ej. portabilidad de datos vs. retención de datos) y sugirió remedios específicos para restaurar la satisfacibilidad.
• Gestión de Contratos:
  • Escenario: Análisis de cláusulas contractuales complejas (exclusividad, penalizaciones, terminación).
  • Resultado: Identificación de inconsistencias en borradores de contratos que podrían afectar su ejecutabilidad, proporcionando redacciones alternativas para resolver conflictos lógicos.

En todos los casos, el sistema logró detectar, explicar y reparar inconsistencias normativas, ofreciendo salidas auditables y alineadas con el dominio.

5. Significado e Impacto

• Puente entre Lógica y Lenguaje: Este trabajo representa un paso crucial hacia la IA neuro-simbólica verdaderamente confiable, donde la rigurosidad lógica y la coherencia comunicativa se refuerzan mutuamente.
• Transparencia y Auditoría: Al eliminar la búsqueda estocástica en la generación de pruebas, el sistema permite una trazabilidad completa desde el texto original hasta la explicación final, esencial para la gobernanza de IA en sectores regulados.
• Cambio de Paradigma: Transita de la "Demostración Automática de Teoremas" (ATP) a la "Comprensión Automática de Teoremas", donde el sistema no solo prueba la verdad, sino que explica el significado y cómo corregir errores.
• Aplicabilidad Futura: El marco sienta las bases para agentes de descubrimiento de teoremas auto-reflexivos, educación en lógica asistida por IA y generación de hipótesis científicas verificables.

En resumen, ∆1–LLM propone una arquitectura donde la corrección es intrínseca (garantizada por la lógica constructiva de ∆1) y la comprensión es accesible (lograda mediante la interpretación de LLM), resolviendo el dilema histórico entre la precisión formal y la interpretabilidad humana.