Resumo Técnico: Redes Neurais de Espículas Binárias como Modelos Causais

Declaração do Problema

O artigo aborda o compromisso entre a precisão e a explicabilidade das Redes Neurais Artificiais (ANNs). As Redes Neurais Binarizadas (BNNs) e as Redes Neurais de Espículas Binárias (BSNNs) oferecem vantagens em termos de eficiência de hardware e representabilidade lógica, mas seus processos internos de tomada de decisão permanecem opacos. Os métodos existentes de IA explicável (XAI), como o SHAP, frequentemente tratam os modelos como "caixas pretas", falhando em considerar estruturas causais internas. Consequentemente, esses métodos podem identificar características como relevantes mesmo quando elas não possuem conexão causal com a saída da rede (por exemplo, conexões de peso zero). Os autores visam preencher essa lacuna mapeando formalmente a dinâmica das BSNNs para um framework causal, permitindo a geração de explicações rigorosas baseadas em lógica que garantam a relevância causal das características incluídas.

Metodologia

1. Formalização de BSNNs

Os autores definem uma arquitetura de BSNN $S$ como uma tupla composta por neurônios de entrada ($I$), neurônios não-entrada ($L$), relações de conectividade ($R$), funções de peso ($W$) e limiares de disparo ($\tau$). Eles modelam a dinâmica de espículas usando um mecanismo de Integração e Disparo (IF) sem vazamentos, onde o estado de disparo de um neurônio no tempo $t$ depende recursivamente de seu estado anterior e da soma ponderada das espículas recebidas.

• Quantização de Peso: O estudo foca em redes com pesos quantizados para conjuntos binários $\{0, 1\}$ ou ternários $\{-1, 0, 1\}$.
• Codificação de Espículas: Os experimentos utilizam codificação de taxa de Poisson e esquemas de binarização por limiar. Os autores evitam explicitamente codificações temporais complexas para gerenciar a complexidade computacional da geração de explicações.

2. Mapeamento para Modelos Causais Binários (BCMs)

Uma contribuição metodológica central é o mapeamento da dinâmica de espículas da BSNN para um Modelo Causal Binário (BCM).

• Variáveis: Cada neurônio $X$ em cada passo de tempo $t$ recebe uma variável booleana $p_{X,t}$. Neurônios de entrada correspondem a variáveis exógenas, enquanto neurônios não-entrada correspondem a variáveis endógenas.
• Dependências Causais: A lógica de disparo é traduzida em um conjunto de equações booleanas (equações estruturais). Para que um neurônio dispare, uma combinação específica de espículas predecessoras deve satisfazer a condição de limiar.
• Equivalência: Os autores provam (Teorema 5.2) que as funções de disparo da BSNN são compatíveis com o BCM se, e somente se, a interpretação booleana satisfizer todas as equações no modelo.

3. Geração de Explicação Abdutiva (AXp)

O artigo emprega Explicações Abdutivas (AXp), definidas como conjuntos minimamente suficientes de características de entrada (literais) que garantem uma classificação de saída específica.

• Definição: Uma AXp $\lambda$ para uma saída $\omega_0$ deve satisfazer: (i) $\lambda$ é verdadeiro dado o input; (ii) $\lambda$ implica logicamente $\omega_0$ sob as restrições do BCM; e (iii) $\lambda$ é minimal (nenhum subconjunto próprio implica $\omega_0$).
• Algoritmos: Duas abordagens baseadas em solvers são implementadas para encontrar AXps:
  1. Baseada em SAT: Codifica o BCM e as condições de explicação em Lógica Proposicional.
  2. Baseada em SMT: Codifica o modelo usando Satisfatibilidade Modulo Theories (especificamente Aritmética Inteira Linear), o que evita a quantificação universal sobre conjuntos de variáveis, oferecendo melhorias significativas de velocidade.
• Estratégia de Busca: O algoritmo começa com um termo completo representando o input total e remove iterativamente literais enquanto verifica se a implicação para a saída permanece válida.

4. Configuração Experimental

A metodologia foi testada no conjunto de dados MNIST para reconhecimento de dígitos manuscritos.

• Arquiteturas: Redes totalmente conectadas com tamanhos de camada oculta variados ($k \in \{8, 16, 32, 64, 128\}$) e quantizações de peso (binária e ternária).
• Tarefas: Classificação de subconjuntos de 3 dígitos e o conjunto completo de 10 dígitos.
• Validação: Alcançou alta precisão (até ~95% para tarefas de 3 dígitos) usando redes quantizadas binárias e ternárias.

Principais Contribuições

1. Primeiro Mapeamento Causal de BSNNs: O artigo apresenta o primeiro mapeamento formal de uma Rede Neural de Espículas Binária sobre um Modelo Causal Binário, capturando dependências causais temporais entre unidades neurais.
2. Framework de Explicação Baseado em Lógica: Demonstra que a natureza booleana das BSNNs permite o uso de solvers SAT e SMT para computar explicações abdutivas diretamente do modelo causal.
3. Garantia de Relevância Causal: Uma contribuição teórica crítica é a Proposição 6.2, que prova que qualquer característica incluída em uma explicação abdutiva derivada deste framework deve ter uma conexão de peso não-zero com a camada oculta da rede. Isso garante que a explicação não contenha características completamente irrelevantes.
4. Análise Comparativa com SHAP: O artigo fornece uma comparação rigorosa com o SHAP (SHapley Additive exPlanations), destacando a tendência do SHAP de atribuir relevância a características com conexões de peso zero devido à sua natureza agnóstica ao modelo.

Resultados

• Eficiência Computacional: A abordagem baseada em SMT superou significativamente a abordagem baseada em SAT. Para redes de peso binário ($S^{bin}_k$), o SMT reduziu os tempos de busca de horas (SAT) para segundos (ex: ~11 horas vs. ~12 segundos para $k=32$). Para redes de peso ternário ($S^{tern}_k$), os tempos de busca SMT variaram de 0,27 a 1,0 hora.
• Qualidade da Explicação: As explicações geradas foram conjuntos mínimos de pixels ativos ou inativos suficientes para disparar a classificação.
• Comparação com SHAP:
  • O SHAP identificou incorretamente características com conexões de peso zero como relevantes em aproximadamente 47% dos casos (média entre amostras).
  • Aumentar o tamanho da amostra para o SHAP reduziu essa taxa de erro, mas aumentou drasticamente o tempo de computação (ex: 173 segundos para 1 milhão de amostras).
  • Em contraste, o método baseado em lógica proposto garante matematicamente que nenhuma característica de peso zero seja incluída na explicação.

Significância e Alegações

Os autores posicionam este trabalho como um passo fundamental para tornar as BSNNs interpretáveis através de lógica formal. Eles alegam que, ao aproveitar a estrutura causal inerente às BSNNs, é possível gerar explicações que não são apenas eficientes, mas também formalmente garantidas de estarem livres de características irrelevantes — uma propriedade que métodos estatísticos ou agnósticos ao modelo, como o SHAP, não podem fornecer.

O artigo nota modestamente que o trabalho atual foca exclusivamente em explicações abdutivas (AXp) e arquiteturas totalmente conectadas. Os autores sugerem que o framework é extensível para conceitos causais mais complexos (como causa real e causas NESS) e outras arquiteturas, como BSNNs Convolucionais (C-BSNNs) e redes treinadas em conjuntos de dados de linguagem, embora estes sejam identificados como direções para pesquisas futuras e não como conquistas atuais.