Resumo Técnico: SHAP Verificado (VERISHAP)

Declaração do Problema

As Explicações Aditivas de Shapley (SHAP) são um método padrão de explicabilidade post-hoc para atribuir previsões de modelos de aprendizado de máquina a características de entrada. No entanto, o cálculo exato dos valores de SHAP para redes neurais é amplamente considerado computacionalmente intratável devido ao espaço de busca exponencial sobre subconjuntos de características ($2^n$). Embora o cálculo exato seja viável para modelos baseados em árvores e aditivos, é #P-difícil para redes neurais gerais. Consequentemente, a literatura depende de estimadores estatísticos (por exemplo, KERNELSHAP, FASTSHAP, LEVERAGESHAP). Esses estimadores enfrentam duas limitações fundamentais:

1. Inexatidão: Eles fornecem aproximações que podem ser pouco confiáveis em modelos altamente não lineares ou cenários com fortes interações entre características.
2. Falta de Verdade Terrena: Como os valores exatos de SHAP são proibitivamente caros para calcular em redes neurais, os estimadores são tipicamente avaliados em modelos de tamanho reduzido (toy-sized), onde o cálculo exato é possível. Essas configurações frequentemente falham em generalizar para redes neurais do mundo real e de alta dimensão.

Metodologia: SHAP Verificado (VERISHAP)

O artigo introduz o VERISHAP, o primeiro algoritmo a aproveitar avanços recentes em verificação de redes neurais para calcular valores exatos de SHAP e limites prováveis para redes neurais. A abordagem adapta técnicas de verificação por ramificação e limite (branch-and-bound) à natureza discreta, probabilística e pesada em somações do SHAP.

Algoritmo Central

O VERISHAP emprega uma estratégia incremental de ramificação e limite para particionar recursivamente o espaço de características (o conjunto de todas as coalizões $S_i$ para uma característica $i$).

1. Particionamento: O algoritmo define ramificações $B$ baseadas em conjuntos de características incluídas ($I$) e excluídas ($E$). Uma ramificação representa um subconjunto de coalizões onde as características em $I$ estão presentes e as características em $E$ estão ausentes.
2. Limitação via Propagação: Para cada ramificação, o algoritmo calcula limites inferiores e superiores na contribuição marginal $\Delta_i(S) = v(S \cup \{i\}) - v(S)$.
   • Para aplicar propagação de limites contínuos (por exemplo, CROWN, IBP) a conjuntos discretos, o algoritmo relaxa máscaras de características booleanas $m \in \{0, 1\}^n$ para o domínio contínuo $[0, 1]^n$.
   • Ele utiliza Propagação de Limites Lineares (LBP) (especificamente CROWN-IBP) para derivar limites apertados sobre a função de valor $v(S)$ no domínio relaxado.
3. Agregação: Os limites totais do valor de SHAP são calculados somando os limites ponderados de todas as ramificações:
   $$\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)}$$
   onde $\Lambda_B$ é a soma em forma fechada dos pesos de Shapley para as coalizões na ramificação $B$, derivada combinatoriamente.
4. Refinamento: O algoritmo seleciona iterativamente ramificações para dividir (usando estratégias como MAXDIAM) e características para dividir (usando estratégias como SMEARS), refinando os limites até que eles converjam para o valor exato ou uma precisão desejada.

Propriedades Teóricas Chave

• Terminação: O algoritmo é garantido a terminar com valores exatos de SHAP após um número finito de iterações (no máximo $2^{n-1}$), à medida que a partição eventualmente isola coalizões únicas.
• Terminação Antecipada para Modelos Lineares: Para modelos lineares, o algoritmo termina na primeira iteração porque a contribuição marginal é constante, e a LBP não introduz erro de aproximação para composições lineares.
• Linearidade por Partes: Para redes ativadas por ReLU, o algoritmo pode terminar antecipadamente se a partição restringir a busca a regiões onde a rede se comporta linearmente.

Contribuições Principais

1. Primeiro SHAP Exato para Redes Neurais: O VERISHAP é o primeiro algoritmo a calcular valores exatos de SHAP para redes neurais gerais, escalando para espaços de busca ordens de magnitude maiores do que métodos exatos anteriores.
2. Limites Prováveis: O método fornece limites inferiores e superiores arbitrariamente apertados sobre os valores de SHAP, permitindo insights explicativos confiáveis mesmo antes da convergência total.
3. Base de Verdade Terrena: Ele estabelece uma estrutura principial para avaliar estimadores estatísticos de SHAP em espaços de busca maiores e mais realistas, onde a verdade terrena era anteriormente inatingível.
4. Eficiência via Verificação: Ao explorar a decomposição de redes neurais em regiões quase lineares, o algoritmo evita enumerar todas as $2^n$ coalizões em muitos casos práticos.

Resultados Experimentais

Os autores avaliaram o VERISHAP em benchmarks tabulares (conjuntos de dados UCI) e de visão (MNIST, FashionMNIST, CIFAR10, GTSRB).

• Escalabilidade vs. EXACTSHAP: O VERISHAP supera significativamente o método exato mais avançado (EXACTSHAP). Enquanto o EXACTSHAP esgota a memória da GPU para espaços de busca maiores que $2^{20}$, o VERISHAP calcula valores exatos para instâncias de até $2^{25}$ ($\approx 3 \times 10^7$ coalizões) e fornece limites apertados para espaços de até $2^{60}$ ($\approx 10^{18}$ coalizões).
• Comparação com Estimadores: Quando comparado a estimadores estatísticos (KERNELSHAP, TREEMSR, LEVERAGESHAP), o VERISHAP demonstra que os estimadores frequentemente falham em alcançar a mesma precisão dentro das restrições de memória. Além disso, o VERISHAP revela que o desempenho do estimador varia significativamente entre conjuntos de dados (por exemplo, o TREEMSR mostra desempenho volátil em redes neurais em comparação com modelos baseados em árvores).
• Versatilidade de Arquitetura: O algoritmo calcula com sucesso valores exatos de SHAP para várias arquiteturas, incluindo redes totalmente conectadas com ativações ReLU, tanh e Swish, bem como ResNets.
• Convergência: Em experimentos (por exemplo, MNIST), os limites tornam-se informativos (revelando padrões de atribuição) muito antes de o valor exato ser calculado, frequentemente em segundos, enquanto o cálculo exato pode levar dezenas de segundos.

Significado e Alegações

O artigo posiciona o VERISHAP como um primeiro passo para escalar o cálculo exato de SHAP para redes neurais. Seu significado reside em três áreas:

1. Escalabilidade: Ele preenche a lacuna entre a intratabilidade teórica do SHAP exato e a aplicação prática, aproveitando a verificação de redes neurais.
2. Confiabilidade: Oferece um método para obter explicações de "verdade terrena" com garantias prováveis, abordando a incerteza inerente às aproximações estatísticas.
3. Estrutura de Avaliação: Fornece um benchmark rigoroso para avaliar e melhorar estimadores de SHAP em espaços de busca maiores, indo além de modelos de tamanho reduzido.

Os autores reconhecem que calcular SHAP exato permanece #P-difícil e que o VERISHAP pode ainda ser lento para certas redes complexas. No entanto, eles argumentam que a capacidade de calcular limites prováveis e o potencial para melhorias contínuas na verificação de redes neurais tornam este um avanço fundamental para a explicabilidade confiável de IA.