Resumen Técnico: SHAP Verificado (VERISHAP)

Enunciado del Problema

Las Explicaciones Aditivas de Shapley (SHAP) son un método estándar de explicabilidad post-hoc para atribuir las predicciones de modelos de aprendizaje automático a características de entrada. Sin embargo, se considera ampliamente que el cálculo exacto de los valores de SHAP para redes neuronales es computacionalmente intratable debido al espacio de búsqueda exponencial sobre subconjuntos de características ($2^n$). Si bien el cálculo exacto es factible para modelos basados en árboles y aditivos, es #P-difícil para redes neuronales generales. En consecuencia, la literatura depende de estimadores estadísticos (por ejemplo, KERNELSHAP, FASTSHAP, LEVERAGESHAP). Estos estimadores enfrentan dos limitaciones fundamentales:

1. Inexactitud: Proporcionan aproximaciones que pueden ser poco fiables en modelos altamente no lineales o en escenarios con fuertes interacciones entre características.
2. Falta de Verdad Terrenal: Dado que el cálculo exacto de los valores de SHAP es prohibitivamente costoso para redes neuronales, los estimadores suelen evaluarse en modelos de tamaño juguetón donde el cálculo exacto es posible. Estos entornos a menudo no generalizan a redes neuronales reales de alta dimensión.

Metodología: SHAP Verificado (VERISHAP)

El artículo introduce VERISHAP, el primer algoritmo que aprovecha los avances recientes en verificación de redes neuronales para calcular valores exactos de SHAP y cotas demostrables para redes neuronales. El enfoque adapta técnicas de verificación por ramificación y acotación a la naturaleza discreta, probabilística y de suma intensiva de SHAP.

Algoritmo Central

VERISHAP emplea una estrategia incremental de ramificación y acotación para particionar recursivamente el espacio de características (el conjunto de todas las coaliciones $S_i$ para una característica $i$).

1. Particionamiento: El algoritmo define ramas $B$ basadas en conjuntos de características incluidas ($I$) y excluidas ($E$). Una rama representa un subconjunto de coaliciones donde las características en $I$ están presentes y las características en $E$ están ausentes.
2. Acotación mediante Propagación: Para cada rama, el algoritmo calcula cotas inferiores y superiores sobre la contribución marginal $\Delta_i(S) = v(S \cup \{i\}) - v(S)$.
   • Para aplicar la propagación de cotas continuas (por ejemplo, CROWN, IBP) a conjuntos discretos, el algoritmo relaja las máscaras de características booleanas $m \in \{0, 1\}^n$ al dominio continuo $[0, 1]^n$.
   • Utiliza Propagación de Cotas Lineales (LBP) (específicamente CROWN-IBP) para derivar cotas ajustadas sobre la función de valor $v(S)$ en el dominio relajado.
3. Agregación: Las cotas totales del valor de SHAP se calculan sumando las cotas ponderadas de todas las ramas:
   $$\phi_i^{(t)} = \sum_{B \in \mathcal{B}^{(t)}} \Lambda_B \Delta_i^B \leq \phi_i \leq \sum_{B \in \mathcal{B}^{(t)}} \Lambda_B \Delta_i^B = \bar{\phi}_i^{(t)}$$
   donde $\Lambda_B$ es la suma en forma cerrada de los pesos de Shapley para las coaliciones en la rama $B$, derivada combinatoriamente.
4. Refinamiento: El algoritmo selecciona iterativamente ramas para dividir (utilizando estrategias como MAXDIAM) y características sobre las cuales dividir (utilizando estrategias como SMEARS), refinando las cotas hasta que convergen al valor exacto o a una precisión deseada.

Propiedades Teóricas Clave

• Terminación: El algoritmo está garantizado para terminar con valores exactos de SHAP después de un número finito de iteraciones (como máximo $2^{n-1}$), ya que la partición eventualmente aísla coaliciones individuales.
• Terminación Temprana para Modelos Lineales: Para modelos lineales, el algoritmo termina en la primera iteración porque la contribución marginal es constante, y LBP no introduce error de aproximación para composiciones lineales.
• Linealidad a Trozos: Para redes activadas con ReLU, el algoritmo puede terminar anticipadamente si la partición restringe la búsqueda a regiones donde la red se comporta de manera lineal.

Contribuciones Clave

1. Primer SHAP Exacto para Redes Neuronales: VERISHAP es el primer algoritmo que calcula valores exactos de SHAP para redes neuronales generales, escalando a espacios de búsqueda órdenes de magnitud mayores que los métodos exactos anteriores.
2. Cotas Demostrables: El método proporciona cotas inferiores y superiores arbitrariamente ajustadas sobre los valores de SHAP, permitiendo insights explicativos confiables incluso antes de la convergencia completa.
3. Línea Base de Verdad Terrenal: Establece un marco principista para evaluar estimadores estadísticos de SHAP en espacios de búsqueda más grandes y realistas donde la verdad terrenal era previamente inalcanzable.
4. Eficiencia mediante Verificación: Al explotar la descomposición de redes neuronales en regiones casi lineales, el algoritmo evita enumerar todas las $2^n$ coaliciones en muchos casos prácticos.

Resultados Experimentales

Los autores evaluaron VERISHAP en tabulares (conjuntos de datos UCI) y visión (MNIST, FashionMNIST, CIFAR10, GTSRB).

• Escalabilidad vs. ExactSHAP: VERISHAP supera significativamente al método exacto más avanzado (EXACTSHAP). Mientras que EXACTSHAP agota la memoria de la GPU para espacios de búsqueda mayores que $2^{20}$, VERISHAP calcula valores exactos para instancias de hasta $2^{25}$ ($\approx 3 \times 10^7$ coaliciones) y proporciona cotas ajustadas para espacios de hasta $2^{60}$ ($\approx 10^{18}$ coaliciones).
• Comparación con Estimadores: Al compararse con estimadores estadísticos (KERNELSHAP, TREEMSR, LEVERAGESHAP), VERISHAP demuestra que los estimadores a menudo no logran la misma precisión dentro de las restricciones de memoria. Además, VERISHAP revela que el rendimiento del estimador varía significativamente entre conjuntos de datos (por ejemplo, TREEMSR muestra un rendimiento volátil en redes neuronales en comparación con modelos basados en árboles).
• Versatilidad de Arquitectura: El algoritmo calcula con éxito valores exactos de SHAP para diversas arquitecturas, incluidas redes totalmente conectadas con activaciones ReLU, tanh y Swish, así como ResNets.
• Convergencia: En experimentos (por ejemplo, MNIST), las cotas se vuelven informativas (revelando patrones de atribución) mucho antes de que se calcule el valor exacto, a menudo en segundos, mientras que el cálculo exacto puede tardar decenas de segundos.

Significado y Afirmaciones

El artículo posiciona a VERISHAP como un primer paso hacia la escalabilidad del cálculo exacto de SHAP para redes neuronales. Su importancia radica en tres áreas:

1. Escalabilidad: Cierra la brecha entre la intratabilidad teórica de SHAP exacto y la aplicación práctica mediante el aprovechamiento de la verificación de redes neuronales.
2. Confianza: Ofrece un método para obtener explicaciones de "verdad terrenal" con garantías demostrables, abordando la incertidumbre inherente a las aproximaciones estadísticas.
3. Marco de Evaluación: Proporciona un referente riguroso para evaluar y mejorar los estimadores de SHAP en espacios de búsqueda más grandes, superando los modelos de juguete.

Los autores reconocen que calcular SHAP exacto sigue siendo #P-difícil y que VERISHAP podría seguir siendo lento para ciertas redes complejas. Sin embargo, argumentan que la capacidad de calcular cotas demostrables y el potencial de mejoras continuas en la verificación de redes neuronales convierten a esto en un avance fundamental para la explicabilidad confiable de la IA.