🤖 AI

ExplAIner: A Declarative Query Language for Explaining Classification Models

Este artículo presenta ExplAIner, un lenguaje de consulta declarativo que unifica diversas nociones de explicación para modelos de clasificación booleana y establece que su evaluación es tratable mediante un número fijo de llamadas a un solver SAT, mientras que su fragmento orientado a la optimización, Opt-FOIL, permite computar explicaciones mínimas con llamadas polinómicas.

Autores originales: Marcelo Arenas, Pablo Barceló, Diego Bustamante, Jose Caraball, María Alejandra Schild, Bernardo Subercaseaux

Publicado 2026-07-08

📖 6 min de lectura🧠 Análisis profundo

CC BY 4.0

Autores originales: Marcelo Arenas, Pablo Barceló, Diego Bustamante, Jose Caraball, María Alejandra Schild, Bernardo Subercaseaux

Artículo original bajo licencia CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta es una explicación generada por IA del artículo a continuación. No ha sido escrita ni avalada por los autores. Para mayor precisión técnica, consulte el artículo original. Leer descargo de responsabilidad completo

Imagina que tienes un robot muy inteligente, pero misterioso, que toma decisiones. Tal vez decide quién recibe un préstamo, o si un escaneo médico parece sospechoso. Le preguntas al robot: "¿Por qué dijiste 'sí' a esta persona en específico?".

El robot no te da una razón simple. Tiene una caja negra en su interior. Para entenderla, los investigadores han inventado docenas de formas diferentes de hacer preguntas: "¿Cuál es la razón más pequeña?", "¿Qué pasaría si cambiamos una sola cosa?", "¿Qué características eran absolutamente necesarias?".

Este artículo argumenta que tener tantas formas diferentes de hacer preguntas es un caos. Es como tener mil llaves diferentes para mil cerraduras distintas, cuando en realidad solo necesitas un llavero universal. Los autores quieren crear un lenguaje universal (un lenguaje de consulta) donde puedas hacer cualquiera de estas preguntas utilizando el mismo conjunto de reglas, y quieren saber exactamente qué tan difícil es para una computadora responderlas.

Aquí está el desgido de su viaje, utilizando algunas analogías de la vida cotidiana:

1. La herramienta antigua: FOIL (La "linterna rota")

Los investigadores primero analizaron una herramienta existente llamada FOIL. Piensa en FOIL como una linterna que usas para mirar dentro de la caja negra del robot.

El problema: La linterna es demasiado débil. No puede iluminar las razones "más pequeñas" o "mejores" (como encontrar el mínimo número de características necesarias). Es como intentar encontrar la piedra más pequeña en un montón de arena con una linterna que solo muestra rocas grandes.
El peligro: Peor aún, la linterna es demasiado poderosa de una manera negativa. Hacerle ciertas preguntas hace que el cerebro de la computadora explote. Las matemáticas muestran que, para algunas preguntas, la computadora tendría que comprobar un número imposible de posibilidades, incluso para modelos simples como los árboles de decisión. Es como pedirle a una calculadora que cuente cada grano de arena en una playa; toma demasiado tiempo.

2. La nueva herramienta: ExplAIner (El "mapa inteligente por capas")

Para solucionar esto, los autores construyeron un nuevo lenguaje llamado ExplAIner. Imagina esto como un mapa de alta tecnología con capas del proceso de toma de decisiones del robot.

Capa 1 (La capa atómica): Esta es la geografía básica. Sabe cómo comparar piezas de información (como "esta pieza tiene 3 partes faltantes, esa tiene 5"). Los autores demostraron que esta capa es fácil de leer; una computadora puede manejarla instantáneamente.
Capa 2 (La capa cuantificada): Esta capa hace preguntas sobre el comportamiento del robot. "¿Si relleno estas partes faltantes, el robot siempre dice sí?" o "¿Siempre dice no?". Esta capa es un poco más difícil, pero sigue siendo manejable (cae en una categoría llamada NP, lo que significa que es difícil pero resoluble con una búsqueda inteligente).
Capa 3 (El ExplAIner completo): Esta es la capa superior donde combinas todo. Puedes hacer preguntas complejas como: "¿Existe una razón que sea mínima y que involucre la característica X?".
La magia: Los autores demostraron que, incluso con estas preguntas complejas, la computadora no necesita volverse loca. Puede responderlas preguntándole a un "ayudante" (un resolvedor de SAT, que es como un resolvedor de acertijos súper inteligente) un número fijo de veces. Es como tener un bibliotecario que puede encontrar cualquier libro en la biblioteca preguntándole al bibliotecario jefe exactamente tres preguntas, sin importar qué tan grande sea la biblioteca.

3. La herramienta de optimización: Opt-FOIL (El "chef eficiente")

Hay un inconveniente. El hecho de que puedas hacer la pregunta (comprobar si existe una razón) no significa que puedas encontrar fácilmente la respuesta específica (la razón real). Es como saber que existe una receta de pastel perfecta, pero no saber cómo hornearla sin quemar la cocina.

Para resolver esto, crearon un subconjunto especial de su lenguaje llamado Opt-FOIL.

El concepto: Esto es como un chef que no solo busca cualquier pastel, sino específicamente el pastel más pequeño que todavía sepa bien, o el pastel con la menor cantidad de azúcar.
El resultado: Demostraron que para estas preguntas de "mejor posible", la computadora puede realmente encontrar la respuesta de manera eficiente. Puede hacer esto preguntando al "ayudante" (el resolvedor de acertijos) un número de veces que crece razonablemente con el tamaño del problema (tiempo polinomial). Es como si el chef tuviera una guía paso a paso que garantiza un pastel perfecto sin quemar la cocina.

4. Por qué esto es importante (El "llavero universal")

La conclusión principal es que los autores han creado un marco estandarizado para explicar la IA.

Uniformidad: En lugar de escribir un nuevo programa de computadora para cada tipo de explicación (abductiva, contrastiva, basada en características), simplemente escribes una consulta en este nuevo lenguaje.
Seguridad: Demostraron matemáticamente que estas consultas no harán que la computadora falle. Se mantienen dentro de una "zona segura" de complejidad, lo que significa que pueden ser resueltas utilizando herramientas estándar y potentes (resolvedores de SAT) que ya se utilizan en la industria.
Flexibilidad: Puedes mezclar y combinar diferentes tipos de explicaciones. Puedes pedir la razón más pequeña, la más grande, o una razón que ignore una característica específica (como el género), todo usando las mismas reglas.

Analogía de resumen

Imagina que el modelo de IA es un cofre del tesoro cerrado con llave.

FOIL era una llave que a veces no encajaba (no podía encontrar la razón más pequeña) y a veces trababa la cerradura con tanta fuerza que rompía la puerta (demasiado complejo de computar).
ExplAIner es un llavero maestro. Tiene diferentes llaves para diferentes cerraduras (diferentes tipos de explicaciones), pero todas encajan en el mismo mecanismo. Los autores demostraron que usar estas llaves no romperá la cerradura.
Opt-FOIL es una herramienta especializada en ese llavero que no solo abre el cofre, sino que también encuentra automáticamente la cerradura más pequeña o la gema más valiosa en su interior, haciéndolo de manera rápida y eficiente.

El artículo no afirma que esto curará enfermedades o predecirá el mercado de valores mañana. Simplemente dice: "Hemos construido una forma mejor, más segura y más organizada de preguntar '¿Por qué?' a los modelos de IA, y hemos demostrado matemáticamente que nuestra nueva forma funciona sin romper la computadora".

Resumen Técnico: ExplAIner: Un Lenguaje de Consulta Declarativo para Explicar Modelos de Clasificación

1. Planteamiento del Problema

El campo de la Inteligencia Artificial Explicable (XAI) ha producido una proliferación de nociones, puntuaciones y consultas de explicación distintas (por ejemplo, abductivas, contrastivas, de necesidad de características, contrafácticas). Desde la perspectiva de la gestión de datos, esta diversidad carece de un marco unificado. Los enfoques actuales suelen requerir el diseño de algoritmos separados para cada tarea de explicación. El artículo postula que se necesita un lenguaje de consulta declarativo para especificar, combinar y analizar estas nociones de manera uniforme.

Sin embargo, los lenguajes fundacionales existentes enfrentan dos limitaciones críticas:

Expresividad: A menudo no logran capturar nociones de explicación basadas en la optimalidad (por ejemplo, explicaciones abductivas mínimas).
Complejidad: Sus problemas de evaluación pueden ser intratables, alcanzando niveles altos de la jerarquía polinómica (PH), lo que los hace poco prácticos para la implementación mediante motores basados en SAT.

El desafío central es diseñar una lógica que equilibre una expresividad suficiente para capturar una amplia familia de consultas de explicación con una complejidad de evaluación controlada (específicamente, la tractabilidad mediante resolvedores SAT, correspondiente a la jerarquía booleana sobre NP).

2. Metodología y Marco de Trabajo

Los autores desarrollan un marco para explicar modelos booleanos (funciones $M: \{0, 1\}^n \to \{0, 1\}$ ) tratando a los modelos como estructuras sobre las cuales se evalúan las consultas. La metodología procede en tres etapas:

2.1 Análisis de FOIL

El artículo revisa primero FOIL (Lógica de Interpretabilidad de Primer Orden), una lógica agnóstica al modelo que trata a los modelos como cajas negras con acceso a instancias positivas y a la relación de subsunción ( $\subseteq$ ) sobre instancias parciales.

Limitación de Expresividad: Los autores demuestran que FOIL no puede expresar la consulta de explicaciones abductivas mínimas (mAXp), incluso cuando se restringe a árboles de decisión. Esto se demuestra mediante juegos de Ehrenfeucht-Fraïssé para mostrar que FOIL no puede distinguir entre modelos donde existe una explicación mínima y aquellos donde no existe, basándose únicamente en la subsunción.
Limitación de Complejidad: Se demuestra que el problema de evaluación para FOIL sobre árboles de decisión es difícil para cada nivel de la jerarquía polinómica ( $\Sigma^P_k$ -duro). Esto implica que FOIL no puede ser evaluado con un número polinomial de llamadas a un oráculo NP, lo que lo hace inadecuado para la evaluación práctica basada en SAT.

2.2 Introducción de ExplAIner

Para abordar estas limitaciones, los autores introducen ExplAIner, una lógica de primer orden por capas con un vocabulario extendido.

Extensión del Vocabulario: ExplAIner añade una relación binaria $\preceq$ que compara instancias parciales basándose en el número de características definidas (cardinalidad). Los autores demuestran que $\subseteq$ y $\preceq$ son independientes; ninguna puede definirse en términos de la otra sobre árboles de decisión.
Estructura por Capas:
1. Capa Atómica: Fórmulas sobre $\{\subseteq, \preceq\}$ . Estas dependen solo de la estructura de las instancias parciales, no del modelo. La evaluación está en P (tiempo polinomial) y la validez es decidible mediante la reducción a la aritmética de Presburger.
2. Capa Cuantificada: Extiende la capa atómica con los predicados AllPos y AllNeg (que comprueban si todas las completaciones de una instancia parcial son clasificadas positivamente/negativamente) y cuantificadores guardados. Los cuantificadores guardados restringen la cuantificación universal a instancias parciales con exactamente una característica definida. Si AllPos y AllNeg son tratables (en P) para una clase de modelos, la evaluación de esta capa está en NP.
3. Capa Completa de ExplAIner: Permite combinaciones booleanas de fórmulas de la capa cuantificada. Esta capa captura toda la Jerarquía Booleana (BH) sobre NP.

2.3 Introducción de Opt-FOIL

Reconociendo que la evaluación (comprobar si una instancia es una explicación) difiere de la computación (encontrar una explicación), los autores definen Opt-FOIL.

Mecanismo: Opt-FOIL es un fragmento de ExplAIner aumentado con un operador de minimización (min) sobre órdenes parciales estrictos definibles.
Sintaxis: Una fórmula $\Psi = \min[\varphi, \rho]$ computa una instancia $x$ que satisface una especificación lógica $\varphi$ que es mínima con respecto a un orden parcial estricto $\rho$ .
Decidibilidad de la Sintaxis: El artículo proporciona un algoritmo (basado en la aritmética de Presburger) para verificar si una fórmula atómica dada define un orden parcial estricto, asegurando que la sintaxis de Opt-FOIL sea decidible.

3. Contribuciones Clave y Resultados

3.1 Limitaciones de FOIL

Teorema 3.1: Ninguna fórmula FOIL puede definir la consulta de explicación abductiva mínima sobre árboles de decisión.
Teorema 3.4: Para cada nivel $k$ de la jerarquía polinómica, existe una fórmula FOIL fija cuya evaluación sobre árboles de decisión es $\Sigma^P_k$ -dura.

3.2 Expresividad y Complejidad de ExplAIner

Expresividad: ExplAIner codifica con éxito una amplia gama de nociones de explicación, incluyendo:
- Explicaciones débiles/abductivas/mínimas abductivas (wAXp, AXp, mAXp).
- Explicaciones débiles/contrastivas/máximas contrastivas (wCXp, CXp, mCXp).
- Cambio Mínimo Requerido (MCR) y Cambio Máximo Permitido (MCA).
- Características Necesarias y Relevantes (NF, RF).
Límites de Complejidad:
- Capa Atómica: La evaluación está en P.
- Capa Cuantificada: Si AllPos y AllNeg están en P, la evaluación está en NP. Existen consultas en esta capa que son NP-completas sobre árboles de decisión.
- Capa Completa: Si AllPos y AllNeg están en P, la evaluación está en la Jerarquía Booleana (BH). Específicamente, para cada nivel $BH_k$ , existe una consulta de ExplAIner que es $BH_k$ -dura sobre árboles de decisión.
- Aplicabilidad: Estos límites se mantienen para árboles de decisión, circuitos d-DNNF (forma normal conjunta de negación decomponible determinista), 2CNF y Horn CNF.

3.3 Garantías Computacionales de Opt-FOIL

Teorema 5.3: Si AllPos y AllNeg están en P, el problema de computación para cualquier fórmula Opt-FOIL está en FPNP (funciones computables en tiempo polinomial con un número polinomial de llamadas a un oráculo NP).
Algoritmo: La computación implica la construcción de un camino en el orden parcial estricto. Dado que la longitud de tales caminos está acotada polinomialmente (Lema 5.5), el algoritmo termina con un número polinomial de llamadas a un resolvedor SAT.
Contención Estricta: Asumiendo que la jerarquía polinómica no colapsa, Opt-FOIL está estrictamente contenido en ExplAIner, que a su vez está estrictamente contenido en FOIL (con predicados extendidos). Esto confirma que Opt-FOIL sacrifica cierta potencia expresiva (por ejemplo, no puede expresar ciertas consultas de no-optimalidad que ExplAIner sí puede) para ganar tractabilidad computacional para encontrar respuestas.

4. Significación y Reivindicaciones

El artículo afirma que ExplAIner y Opt-FOIL proporcionan una base declarativa y unificada para la XAI formal.

Uniformidad: Ofrecen un único lenguaje para especificar diversas nociones de explicación, permitiendo la combinación de criterios (por ejemplo, encontrar una explicación común para múltiples instancias).
Tractabilidad: Al restringir la lógica a capas donde la evaluación está en la jerarquía booleana y la computación es en FPNP, el marco se alinea con las capacidades de los resolvedores SAT modernos. Esto es crucial porque la XAI formal a menudo depende de codificaciones SAT para modelos como árboles de decisión y circuitos d-DNNF.
Separación de Preocupaciones: El marco separa la especificación lógica de las consultas de explicación de la complejidad de evaluación dependiente de la representación. Esto permite que el mismo lenguaje de consulta se aplique a diferentes clases de modelos (árboles, circuitos) siempre que soporten comprobaciones de consistencia eficientes (AllPos/AllNeg).

Los autores concluyen que, si bien FOIL sirve como una herramienta teórica fundacional, es inadecuada para la implementación práctica debido a su alta complejidad y expresividad limitada respecto a la optimalidad. ExplAIner y Opt-FOIL resuelven estos problemas, permitiendo la especificación y la computación eficiente de explicaciones para modelos booleanos.