Rethinking Explanations: Formalizing Contrast in Description Logics

Resumen Técnico: Repensando las Explicaciones: Formalizando el Contraste en Lógicas de Descripción

Enunciado del Problema
Las formalizaciones existentes de explicaciones para bases de conocimiento (BK) en Lógica de Descripción (LD) se centran principalmente en justificaciones (explicar por qué un axioma $P$ es verdadero) y en razonamiento abductivo (explicar por qué un axioma ausente $P$ podría ser verdadero). Sin embargo, estos enfoques carecen de una perspectiva centrada en el usuario. No abordan las necesidades cognitivas específicas de un inquiriente que a menudo se sorprende por un hecho $P$ porque anticipaba un evento alternativo $Q$. Proporcionar explicaciones separadas para "por qué $P$" y "por qué no $Q$" suele ser insatisfactorio, ya que los usuarios buscan comprender la diferencia específica entre el resultado real y la alternativa esperada. Aunque las explicaciones contrastivas (EC) están bien estudiadas en el aprendizaje automático y en marcos de argumentación, siguen siendo poco exploradas en el contexto de las LD, a pesar de que estas son la base para ontologías como OWL utilizadas en dominios críticos como la atención sanitaria (por ejemplo, SNOMED CT).

Metodología
Los autores proponen un marco formal para generar explicaciones contrastivas dentro de BK en LD, adaptando el modelo filosófico de explicación contrastiva de Peter Lipton al entorno lógico de las LD.

1. Formalización de Preguntas Contrastivas (PC):
   Una PC se define como un par $(P, Q)$ donde $P$ es un hecho (una afirmación de ABox derivada, por ejemplo, $C(x)$) y $Q$ es un contrapunto (una afirmación no derivada). El artículo se centra en dos tipos específicos de contrapuntos:

   • Contrastes de Entidad: $Q$ es $C(y)$, contrastando el mismo concepto contra un individuo diferente.
   • Contrastes de Concepto: $Q$ es $D(x)$, contrastando un concepto diferente para el mismo individuo.

2. Definición de la Explicación Contrastiva (EC):
   Los autores van más allá de una simple diferencia simétrica entre la justificación de $P$ y la hipótesis abductiva para $Q$. Introducen una definición basada en tuplas $E = \langle E_{fact}, E_{foil+}, E_{foil-} \rangle$ (y opcionalmente un conjunto de conflicto $C$) basada en tres principios:

   • Condición de Diferencia: La explicación debe citar la diferencia entre las razones para $P$ y los hechos ausentes para $Q$.
   • Conocimiento Conocido vs. Conocimiento Asumido: La explicación debe distinguir entre axiomas que son verdaderos en la BK con respecto al contrapunto ($E_{foil+}$) y los axiomas ausentes necesarios para derivar el contrapunto ($E_{foil-}$).
   • Contabilización de Axiomas Similares: El marco introduce un operador de "diferencia de conjunto renombrada" ($\ddagger$). Este operador elimina axiomas que son estructuralmente similares entre el hecho y el contrapunto (por ejemplo, $C(x)$ y $C(y)$, o $E \sqsubseteq C$ y $E \sqsubseteq D$) para asegurar que la explicación destaque únicamente los factores distintivos.

3. Manejo de Inconsistencias:
   Si agregar los axiomas faltantes para el contrapunto ($E_{foil-}$) crea un conflicto con la BK existente, el marco incluye un conjunto de conflicto $C$. Este conjunto representa el subconjunto mínimo de afirmaciones de ABox existentes que deben eliminarse para que el contrapunto sea derivado, modelando efectivamente un escenario contrafáctico.

4. Criterios de Preferencia:
   Para seleccionar entre múltiples EC posibles, los autores proponen una métrica de divergencia sintáctica ($\sigma_{div}$). Esta métrica mide la diferencia simétrica entre los axiomas relevantes para el hecho y aquellos relevantes para el contrapunto. Una EC preferida es aquella que minimiza esta divergencia, alineando las estructuras de razonamiento del hecho y del contrapunto lo más estrechamente posible para facilitar la comparación.

Contribuciones Clave

• Definiciones Formales: El artículo proporciona las primeras definiciones formales de explicaciones contrastivas para BK en LD, abordando específicamente tanto los contrastes de entidad como los de concepto.
• Esquema General: Presenta un esquema general para EC que integra justificaciones e hipótesis abductivas, distinguiendo entre afirmaciones verdaderas y ausentes.
• Análisis de Complejidad: Los autores analizan la complejidad computacional de las EC en dos LD:
  • $\mathcal{EL}$: Demuestran que decidir la existencia de una EC de un tamaño dado es NP-completo para contrastes de concepto. Sin embargo, para contrastes de entidad, una EC preferida por $\sigma_{div}$ (con divergencia 0) puede calcularse en tiempo polinómico.
  • $\mathcal{ALC}$: Se demuestra que el problema de decidir la existencia de una EC de un tamaño dado es ExpTime-completo.
• Implementación y Evaluación: Se desarrolló una implementación prototipo en Java (utilizando OWL API y el razonador ELK). Se realizaron experimentos en aproximadamente 41 BK OWL del mundo real.

Resultados
La evaluación experimental arrojó los siguientes hallazgos:

• Eficiencia: El prototipo calcula EC de manera eficiente, con un tiempo de ejecución promedio de aproximadamente 392 ms.
• Tamaño de la Explicación: Las explicaciones generadas son compactas, abarcando típicamente hasta cuatro axiomas de ABox.
• Comúnidad: Se encontró que la "Ratio de Axiomas Comunes" (la superposición entre las justificaciones del hecho y del contrapunto) es baja (promedio del 13.5%), lo que sugiere que en muchos casos, el hecho y el contrapunto dependen de conjuntos distintos de afirmaciones.
• Consistencia: La tasa de conflicto fue baja (4.00%), lo que indica que en la mayoría de los casos, los axiomas faltantes para el contrapunto no contradicen la BK existente.

Significado y Afirmaciones
El artículo afirma cerrar una brecha significativa en la literatura al introducir explicaciones contrastivas en el dominio de las Lógicas de Descripción. Los autores argumentan que este enfoque ofrece una manera más intuitiva y centrada en el usuario de explicar los resultados del razonamiento al modelar explícitamente las expectativas del inquiriente (el contrapunto).

El trabajo se presenta como un paso preliminar en esta área. Los autores notan modestamente que, aunque sus definiciones se extienden a cualquier LD que soporte hipótesis abductivas, se necesita más trabajo para manejar LD más expresivas (por ejemplo, con restricciones de cardinalidad) y desarrollar algoritmos que escalen eficientemente a grandes conjuntos de datos. También identifican la necesidad de futuros estudios con usuarios para validar si estas explicaciones contrastivas son realmente preferidas sobre las justificaciones estándar por los usuarios finales. El artículo concluye que su marco proporciona un mecanismo riguroso y formal para combinar justificaciones y explicar la diferencia entre un hecho y un contrapunto, sentando las bases para una toma de decisiones más informada en aplicaciones de la web semántica.