Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues

El artículo presenta Elenchus, un sistema de diálogo que utiliza un modelo de lenguaje como oponente para construir bases de conocimiento mediante la explicitación de compromisos inferenciales bajo una semántica inferencialista, demostrando su eficacia al generar y verificar formalmente la ontología de procedencia PROV-O.

Lo esencial

Imagina que quieres construir una casa de conocimientos muy sólida, como una biblioteca o un mapa de reglas para una inteligencia artificial. Tradicionalmente, los ingenieros de conocimiento han intentado hacer esto como si fueran mineros: pensaban que los expertos humanos ya tenían todas las respuestas perfectas y estructuradas dentro de sus cabezas, y que el trabajo era simplemente "extraerlas" y escribirlas en un libro.

El problema es que, a menudo, los expertos no tienen esas respuestas listas. Sus ideas son como un bosque denso: tienen sentido cuando están caminando por él, pero es difícil dibujar un mapa exacto sin tropezar.

Elenchus es una nueva herramienta que cambia completamente esta idea. En lugar de ser un minero, Elenchus actúa como un entrenador de debate o un espejo crítico.

Aquí te explico cómo funciona, usando analogías sencillas:

1. El Juego de "El Abogado y el Escéptico"

Imagina que tienes un experto humano (el "Abogado") que conoce mucho sobre un tema, y una Inteligencia Artificial (el "Escéptico").

• El Abogado dice: "Creo que A es verdad y B es verdad".
• El Escéptico (la IA) no le da la razón automáticamente. En su lugar, piensa: "Espera, si A es verdad y B es verdad, ¿no significa eso que C también debe ser verdad? Pero tú dijiste que C es falso. ¡Hay una contradicción aquí!".
• Esta contradicción se llama "tensión".

2. La IA no es la que sabe, es la que pregunta

Aquí está la magia: La IA no es la que tiene la verdad. La IA es un "oráculo defectuoso". A veces se equivoca, a veces inventa cosas. Pero eso no importa.

• Si la IA dice: "¡Oye, hay un error!", el experto humano puede decir: "Tienes razón, me equivoqué, retiro lo que dije" (retracción).
• O puede decir: "No, te has equivocado tú, mi idea tiene sentido si la matizo un poco" (refinamiento).
• O puede decir: "Esa contradicción no existe, tu lógica falla" (controversia).

La analogía: Piensa en la IA como un detective de errores que a veces grita "¡Fuego!" cuando solo es humo de una tostadora. El experto es el bombero. El experto decide si hay fuego real o no. Si el experto acepta que hay fuego, entonces la regla "si hay humo, hay fuego" se escribe en el libro de reglas. Si el experto dice "no es fuego", la regla se descarta.

3. El resultado: Un mapa de "lo que no puede ir junto"

Al final de la conversación, no tenemos una lista de "lo que el experto cree". Tenemos un mapa de lo que el experto ha defendido y lo que ha rechazado.

En lugar de decir "A implica B", el sistema registra: "El experto aceptó que no puede creer en A y negar B al mismo tiempo". Esto crea una estructura lógica muy robusta llamada Base Material.

• Analogía: Imagina que estás armando un rompecabezas. No pegas las piezas porque "se ven bien juntas". Las pegas porque, después de probarlas y empujarlas, descubriste que solo encajan de esa manera y no de otra. Elenchus es el proceso de empujar las piezas hasta que encajan perfectamente.

4. ¿Por qué es genial? (El caso de PROV-O)

Los autores probaron esto con un estándar real de internet llamado PROV-O (que explica cómo rastrear el origen de los datos).

• Lo tradicional: Habría tomado años de reuniones y correos electrónicos para decidir las reglas.
• Con Elenchus: En una sola sesión de conversación, el experto y la IA descubrieron las mismas reglas complejas que los creadores originales habían decidido tras miles de correos.
• La prueba: Usaron un "máster de lógica" (llamado pyNMMS) para verificar el resultado. El sistema confirmó que las reglas generadas tenían las propiedades exactas que los diseñadores originales querían: no eran rígidas (podían cambiar con nueva información), no eran transitivas (A no siempre lleva a C) y eran independientes entre sí.

En resumen

Elenchus es como un gimnasio para la mente.

• No asume que el experto ya tiene el músculo (el conocimiento formal) listo.
• Usa a la IA como un compañero de entrenamiento que empuja, cuestiona y busca debilidades.
• A través del esfuerzo de defender sus ideas, el experto construye el conocimiento formal paso a paso.

Es una forma de decir: "El conocimiento no es algo que tienes en la cabeza esperando a ser sacado; es algo que creas mientras hablas, defiendes y ajustas tus ideas". Y lo mejor de todo: cada regla final tiene una "huella digital" que te dice exactamente en qué momento de la conversación se decidió.

Resumen técnico

Aquí tienes un resumen técnico detallado del artículo "Elenchus: Generating Knowledge Bases from Prover-Skeptic Dialogues" en español, estructurado según los puntos solicitados.

1. El Problema: La Cuello de Botella de la Adquisición de Conocimiento

El artículo aborda el persistente problema de la adquisición de conocimiento en la ingeniería de conocimientos. Tradicionalmente, este campo ha intentado formalizar el conocimiento experto extrayendo estructuras preexistentes de la mente de los expertos o de textos naturales.

• Limitación actual: Se asume erróneamente que el conocimiento experto es un contenido interno determinista que solo necesita ser transcripido. Sin embargo, el conocimiento no está determinado antes de su articulación; se constituye a través de prácticas de expresión y negociación.
• Consecuencia: Los enfoques tradicionales (sistemas expertos, ontologías, grafos de conocimiento) siguen enfrentando dificultades para formalizar el conocimiento expresado en lenguaje natural, manteniéndose como un cuello de botella tras 50 años de esfuerzo.

2. Metodología: Elenchus y Semántica Inferencialista

El paper propone Elenchus, un sistema de diálogo que re-conceptualiza la ingeniería de conocimientos como explicitación en lugar de extracción. Se basa en la semántica inferencialista (Brandom, Hlobil), donde el significado de una oración se define por su rol inferencial (qué sigue de ella, qué la contradice) y no por sus condiciones de verdad.

El Protocolo de Diálogo Bilateral

Elenchus implementa un protocolo de diálogo Probar-Escepticismo (Prover-Skeptic) entre un experto humano y un modelo de lenguaje grande (LLM):

1. Roles:
   • Experto (Respondiente): Desarrolla una posición bilateral (un conjunto de compromisos/afirmaciones y denegaciones) sobre un tema.
   • LLM (Oponente): Actúa como un oráculo de derivabilidad defeasible. Su función es desafiar la coherencia de la posición del experto, proponiendo "tensiones" (afirmaciones de que ciertas combinaciones de compromisos y denegaciones son incoherentes).
2. Resolución de Tensiones: El experto resuelve las tensiones propuestas por el LLM mediante:
   • Retracción: Eliminar un compromiso o denegación.
   • Refinamiento: Ajustar la proposición para disolver el conflicto.
   • Contestación: Rechazar la incoherencia alegada por el LLM.
3. Control de Calidad: La autoridad epistémica recae en el humano. El LLM puede proponer falsos positivos (tensiones inexistentes), pero estos son filtrados por la contestación del experto. El LLM no genera el conocimiento, sino que descubre relaciones inferenciales implícitas que el experto debe validar.

De Estados Dialécticos a Bases Materiales

El sistema mapea los estados del diálogo a Bases Materiales en la lógica NMMS (NonMonotonic MultiSuccedent) de Hlobil y Brandom:

• Una Base Material ($B = \langle L_B, \vdash_B \rangle$) consiste en un lenguaje atómico y una relación de consecuencia base.
• La relación $\Gamma \vdash_B \Delta$ se mantiene si la posición de afirmar todo en $\Gamma$ y negar todo en $\Delta$ es incoherente.
• Contención (Containment): La base satisface la condición mínima de coherencia: afirmar y negar la misma sentencia es incoherente.
• Estructura de la Base: La relación de consecuencia se construye uniendo dos componentes:
  1. $I$ (Implicaciones Materiales): Descubiertas dialécticamente (tensiones aceptadas por el experto).
  2. $Cont$ (Contención): Normas pragmáticas de coherencia bilateral (afirmar y negar lo mismo).

3. Contribuciones Clave

El artículo presenta tres contribuciones técnicas principales:

1. Protocolo Elenchus: Un protocolo dialéctico bilateral que utiliza un LLM como oráculo para estructurar el conocimiento experto mediante la resolución de tensiones, generando un registro explícito de compromisos y denegaciones.
2. Mapeo Formal a Lógica NMMS: Una definición formal que mapea los estados dialécticos de Elenchus a bases materiales en la lógica NMMS. Este mapeo satisface la propiedad de Contención y permite la explicitación del vocabulario lógico: la lógica hace explícitas las relaciones inferenciales materiales descubiertas en el diálogo.
3. Implementación y Caso de Estudio: Una implementación funcional utilizando Claude Code (con almacenamiento persistente en GitHub para el estado del diálogo) y su aplicación al caso de estudio de la ontología PROV-O (W3C), demostrando la integración de extremo a extremo desde el diálogo hasta el razonamiento formal.

4. Resultados del Caso de Estudio (PROV-O)

El sistema se probó utilizando la especificación en prosa de la sección 3.1 de la recomendación PROV-O (350 palabras) y un experto del dominio.

• Proceso: El LLM extrajo 10 compromisos iniciales y planteó 7 desafíos sobre especificaciones insuficientes. El experto resolvió las tensiones, retractando un compromiso inicial y refinando otros.
• Resultado Formal: Se generó una base material con 19 compromisos y 9 implicaciones materiales aceptadas.
• Verificación con pyNMMS: Se utilizó el razonador automático pyNMMS para verificar las propiedades estructurales de la base resultante:
  • No Transitividad: Se verificó que la cadena de inferencias (ej. Entidad $\to$ Individuación $\to$ Términos Expandidos) no implica transitividad automática en la base, preservando la distinción entre el núcleo y las extensiones de la ontología.
  • No Monotonía: Se demostró que añadir contexto (ej. detalles de la cadena de procedencia) puede derrotar inferencias que eran válidas en un contexto "desordenado" (scruffy).
  • Independencia: Las resoluciones de diseño de diferentes desafíos (cadenas de inferencia) resultaron ser inferencialmente independientes entre sí, confirmando que el protocolo identificó tensiones de diseño genuinas y distintas.
  • Correspondencia con Racional de Diseño: Las propiedades estructurales de la base generada coincidieron exactamente con las decisiones de diseño documentadas retrospectivamente en Moreau et al. (2015), que analizaron miles de correos y reuniones del grupo de trabajo original.

5. Significado e Impacto

El trabajo de Elenchus tiene implicaciones profundas para la ingeniería de conocimientos y la lógica filosófica:

• Reconceptualización del Conocimiento: Cambia el paradigma de "extraer" conocimiento preformado a "constituirlo" mediante la negociación dialéctica. La base de conocimientos no es una descripción de lo que el experto cree, sino un registro de lo que ha sido articulado y defendido.
• Manejo de la Incertidumbre de los LLM: En lugar de tratar las alucinaciones de los LLM como un fallo de fiabilidad, Elenchus las integra estructuralmente. El LLM actúa como un generador de hipótesis (tensiones) que el humano valida. Esto convierte el potencial error del LLM en una característica del protocolo de descubrimiento.
• Razonamiento Subestructural: A diferencia de las ontologías clásicas (OWL) que a menudo asumen lógica monotónica y transitiva, Elenchus produce bases materiales que preservan la no transitividad y no monotonicidad inherentes al conocimiento experto real.
• Trazabilidad Completa: Cada relación inferencial en la base final tiene una justificación dialéctica explícita (un movimiento específico en el diálogo), resolviendo el problema de la opacidad en la generación de conocimientos asistida por IA.
• Explicitación Lógica: Demuestra cómo el vocabulario lógico (conectivas como $\to$, $\neg$) puede elaborarse a partir de la práctica lingüística para hacer explícitas las relaciones materiales, cumpliendo el programa inferencialista de Brandom.

En resumen, Elenchus ofrece un marco viable y formalmente riguroso para construir bases de conocimientos que respetan la naturaleza defeasible y contextual del razonamiento experto, utilizando la interacción humano-IA no para generar contenido, sino para estructurar y validar inferencias.