Resumen Técnico: Redes Neuronales de Impulsos Binarios como Modelos Causales

Planteamiento del Problema

El artículo aborda el compromiso entre la precisión y la explicabilidad de las Redes Neuronales Artificiales (ANN). Aunque las Redes Neuronales Binarizadas (BNN) y las Redes Neuronales de Impulsos Binarios (BSNN) ofrecen ventajas en términos de eficiencia de hardware y representabilidad lógica, sus procesos internos de toma de decisiones siguen siendo opacos. Los métodos existentes de IA explicable (XAI), como SHAP, a menudo tratan a los modelos como "cajas negras", sin tener en cuenta las estructuras causales internas. En consecuencia, estos métodos pueden identificar características como relevantes incluso cuando no tienen una conexión causal con la salida de la red (por ejemplo, conexiones de peso cero). Los autores pretenden cerrar esta brecha mediante el mapeo formal de la dinámica de las BSNN a un marco causal, permitiendo la generación de explicaciones rigurosas basadas en la lógica que garanticen la relevancia causal de las características incluidas.

Metodología

1. Formalización de las BSNN

Los autores definen una arquitectura BSNN $S$ como una tupla que comprende neuronas de entrada ($I$), neuronas que no son de entrada ($L$), relaciones de conectividad ($R$), funciones de peso ($W$) y umbrales de disparo ($\tau$). Modelan la dinámica de impulsos utilizando un mecanismo de Integración y Disparo (IF) sin fugas, donde el estado de disparo de una neurona en el tiempo $t$ depende recursivamente de su estado anterior y de la suma ponderada de los impulsos entrantes.

• Cuantificación de Pesos: El estudio se centra en redes con pesos cuantificados a conjuntos binarios $\{0, 1\}$ o ternarios $\{-1, 0, 1\}$.
• Codificación de Impulsos: Los experimentos utilizan codificación de tasa de Poisson y esquemas de binarización por umbral. Los autores evitan explícitamente la codificación temporal compleja para gestionar la complejidad computacional de la generación de explicaciones.

2. Mapeo a Modelos Causales Binarios (BCM)

Una contribución metodológica central es el mapeo de la dinámica de impulsos de la BSNN a un Modelo Causal Binario (BCM).

• Variables: A cada neurona $X$ en cada paso de tiempo $t$ se le asigna una variable booleana $p_{X,t}$. Las neuronas de entrada corresponden a variables exógenas, mientras que las neuronas que no son de entrada corresponden a variables endógenas.
• Dependencias Causales: La lógica de disparo se traduce en un conjunto de ecuaciones booleanas (ecuaciones estructurales). Para que una neurona dispare, una combinación específica de impulsos predecesores debe satisfacer la condición de umbral.
• Equivalencia: Los autores demuestran (Teorema 5.2) que las funciones de disparo de la BSNN son compatibles con el BCM si y solo si la interpretación booleana satisface todas las ecuaciones del modelo.

3. Generación de Explicaciones Abductivas (AXp)

El artículo emplea Explicaciones Abductivas (AXp), definidas como conjuntos de características de entrada (literales) mínimamente suficientes que garantizan una clasificación de salida específica.

• Definición: Una AXp $\lambda$ para una salida $\omega_0$ debe satisfacer: (i) $\lambda$ es verdadera dado el input; (ii) $\lambda$ implica lógicamente $\omega_0$ bajo las restricciones del BCM; y (iii) $\lambda$ es mínima (ningún subconjunto propio implica $\omega_0$).
• Algoritmos: Se implementan dos enfoques basados en solvers para encontrar las AXp:
  1. Basado en SAT: Codifica el BCM y las condiciones de explicación en Lógica Proposicional.
  2. Basado en SMT: Codifica el modelo utilizando Satisfacibilidad Modulo Teorías (específicamente Aritmética Entera Lineal), lo que evita la cuantificación universal sobre conjuntos de variables, ofreciendo mejoras significativas en la velocidad de búsqueda.
• Estrategia de Búsqueda: El algoritmo comienza con un término completo que representa el input total e itera eliminando literales mientras verifica que la implicación hacia la salida siga siendo válida.

4. Configuración Experimental

La metodología se probó con el conjunto de datos MNIST para el reconocimiento de dígitos escritos a mano.

• Arquitecturas: Redes totalmente conectadas con tamaños de capa oculta variables ($k \in \{8, 16, 32, 64, 128\}$) y cuantificaciones de peso (binarias y ternarias).
• Tareas: Clasificación de subconjuntos de 3 dígitos y el conjunto completo de 10 dígitos.
• Validación: Se logró una alta precisión (hasta ~95% para tareas de 3 dígitos) utilizando redes cuantificadas binarias y ternarias.

Principales Contribuciones

1. Primer Mapeo Causal de las BSNN: El artículo presenta el primer mapeo formal de una Red Neuronal de Impulsos Binarios sobre un Modelo Causal Binario, capturando las dependencias causales temporales entre las unidades neuronales.
2. Marco de Explicación Basado en Lógica: Demuestra que la naturaleza booleana de las BSNN permite el uso de solvers SAT y SMT para calcular explicaciones abductivas directamente desde el modelo causal.
3. Garantía de Relevancia Causal: Una contribución teórica crítica es la Proposición 6.2, que demuestra que cualquier característica incluida en una explicación abductiva derivada de este marco debe tener una conexión de peso no nula con la capa oculta de la red. Esto asegura que la explicación no contenga características completamente irrelevantes.
4. Análisis Comparativo con SHAP: El artículo proporciona una comparación rigurosa con SHAP (SHapley Additive exPlanations), destacando la tendencia de SHAP a asignar relevancia a características con conexiones de peso cero debido a su naturaleza agnóstica al modelo.

Resultados

• Eficiencia Computacional: El enfoque basado en SMT superó significativamente al enfoque basado en SAT. Para redes de pesos binarios ($S^{bin}_k$), SMT redujo los tiempos de búsqueda de horas (SAT) a segundos (por ejemplo, ~11 horas frente a ~12 segundos para $k=32$). Para redes de pesos ternarios ($S^{tern}_k$), los tiempos de búsqueda de SMT oscilaron entre 0.27 y 1.0 horas.
• Calidad de la Explicación: Las explicaciones generadas fueron conjuntos mínimos de píxeles activos o inactivos suficientes para activar la clasificación.
• Comparación con SHAP:
  • SHAP identificó incorrectamente características con conexiones de peso cero como relevantes en aproximadamente el 47% de los casos (promediado entre tamaños de muestra).
  • Aumentar el tamaño de la muestra para SHAP redujo esta tasa de error pero aumentó drásticamente el tiempo de computación (por ejemplo, 173 segundos para 1M de muestras).
  • En contraste, el método basado en lógica propuesto garantiza matemáticamente que ninguna característica de peso cero se incluya en la explicación.

Significado y Reivindicaciones

Los autores posicionan este trabajo como un paso fundacional para hacer que las BSNN sean interpretables mediante la lógica formal. Afirman que, al aprovechar la estructura causal inherente a las BSNN, es posible generar explicaciones que no solo son eficientes, sino que están formalmente garantizadas para estar libres de características irrelevantes, una propiedad que los métodos estadísticos o agnósticos al modelo como SHAP no pueden proporcionar.

El artículo señala modestamente que el trabajo actual se centra exclusivamente en explicaciones abductivas (AXp) y arquitecturas totalmente conectadas. Los autores sugieren que el marco es extensible a conceptos causales más complejos (como la causa real y las causas NESS) y otras arquitecturas, como las BSNN Convolucionales (C-BSNNs) y las redes entrenadas en conjuntos de datos de lenguaje, aunque estas se identifican como direcciones para la investigación futura más que como logros actuales.