Sintesi Tecnica: Reti Neurali Spiking Binarie come Modelli Causali

Definizione del Problema

Il documento affronta il compromesso tra accuratezza e spiegabilità delle Reti Neurali Artificiali (ANN). Sebbene le Reti Neurali Binarizzate (BNN) e le Reti Neurali Spiking Binarie (BSNN) offrano vantaggi in termini di efficienza hardware e rappresentabilità logica, i loro processi decisionali interni rimangono opachi. I metodi esistenti di intelligenza artificiale spiegabile (XAI), come SHAP, trattano spesso i modelli come "black box", fallendo nel considerare le strutture causali interne. Di conseguenza, tali metodi possono identificare caratteristiche come rilevanti anche quando non hanno una connessione causale con l'output della rete (ad esempio, connessioni a peso zero). Gli autori mirano a colmare questo divario mappando formalmente la dinamica delle BSNN in un framework causale, consentendo la generazione di spiegazioni rigorose e basate sulla logica che garantiscano la rilevanza causale delle caratteristiche incluse.

Metodologia

1. Formalizzazione delle BSNN

Gli autori definiscono un'architettura BSNN $S$ come una tupla composta da neuroni di input ($I$), neuroni non di input ($L$), relazioni di connettività ($R$), funzioni di peso ($W$) e soglie di attivazione ($\tau$). Modellano la dinamica degli spike utilizzando un meccanismo Integrate-and-Fire (IF) privo di perdite (leaks), dove lo stato di attivazione di un neurone al tempo $t$ dipende ricorsivamente dal suo stato precedente e dalla somma pesata degli spike in entrata.

• Quantizzazione dei Pesi: Lo studio si concentra su reti con pesi quantizzati in insiemi binari $\{0, 1\}$ o ternari $\{-1, 0, 1\}$.
• Codifica degli Spike: Gli esperimenti utilizzano la codifica del tasso di Poisson (Poisson rate coding) e schemi di binarizzazione della soglia. Gli autori evitano esplicitamente codifiche temporali complesse per gestire la complessità computazionale della generazione delle spiegazioni.

2. Mappatura in Modelli Causali Binari (BCM)

Un nucleo del contributo metodologico è la mappatura della dinamica di spiking delle BSNN in un Modello Causale Binario (BCM).

• Variabili: Ogni neurone $X$ ad ogni istante temporale $t$ è assegnato a una variabile booleana $p_{X,t}$. I neuroni di input corrispondono a variabili esogene, mentre i neuroni non di input corrispondono a variabili endogene.
• Dipendenze Causali: La logica di attivazione viene tradotta in un insieme di equazioni booleane (equazioni strutturali). Affinché un neurone si attivi, una specifica combinazione di spike precedenti deve soddisfare la condizione di soglia.
• Equivalenza: Gli autori dimostrano (Teorema 5.2) che le funzioni di attivazione delle BSNN sono compatibili con il BCM se e solo se l'interpretazione booleana soddisfa tutte le equazioni del modello.

3. Generazione di Spiegazioni Abduttive (AXp)

Il documento impiega le Spiegazioni Abduttive (AXp), definite come insiemi minimamente sufficienti di caratteristiche di input (letterali) che garantiscono una specifica classificazione di output.

• Definizione: Un AXp $\lambda$ per un output $\omega_0$ deve soddisfare: (i) $\lambda$ è vero dato l'input; (ii) $\lambda$ implica logicamente $\omega_0$ sotto i vincoli del BCM; e (iii) $\lambda$ è minimo (nessun sottoinsieme proprio implica $\omega_0$).
• Algoritmi: Due approcci basati su solver sono implementati per trovare gli AXp:
  1. Basato su SAT: Codifica il BCM e le condizioni di spiegazione in Logica Proposizionale.
  2. Basato su SMT: Codifica il modello utilizzando la Satisfiability Modulo Theories (specificamente l'Aritmetica Intera Lineare), il che evita la quantificazione universale sugli insiemi di variabili, offrendo miglioramenti significativi nella velocità di ricerca.
• Strategia di Ricerca: L'algoritmo parte da un termine completo che rappresenta l'input totale e rimuove iterativamente i letterali verificando che l'implicazione verso l'output rimanga valida.

4. Configurazione Sperimentale

La metodologia è stata testata sul dataset MNIST per il riconoscimento di cifre scritte a mano.

• Architetture: Reti completamente connesse con dimensioni dello strato nascosto variabili ($k \in \{8, 16, 32, 64, 128\}$) e quantizzazione dei pesi (binaria e ternaria).
• Task: Classificazione di sottoinsiemi di 3 cifre e dell'intero set di 10 cifre.
• Validazione: Ha raggiunto un'elevata accuratezza (fino a circa il 95% per i task a 3 cifre) utilizzando reti quantizzate binarie e ternarie.

Contributi Chiave

1. Prima Mappatura Causale delle BSNN: Il documento presenta la prima mappatura formale di una Rete Neurale Spiking Binaria su un Modello Causale Binario, catturando le dipendenze causali temporali tra le unità neurali.
2. Framework di Spiegazione Basato sulla Logica: Dimostra che la natura booleana delle BSNN permette l'uso di solver SAT e SMT per calcolare spiegazioni abduttive direttamente dal modello causale.
3. Garanzia di Rilevanza Causale: Un contributo teorico critico è la Proposizione 6.2, che dimostra che qualsiasi caratteristica inclusa in una spiegazione abduttiva derivata da questo framework deve avere una connessione a peso non nullo con lo strato nascosto della rete. Ciò garantisce che la spiegazione non contenga caratteristiche completamente irrilevanti.
4. Analisi Comparativa con SHAP: Il documento fornisce un confronto rigoroso con SHAP (SHapley Additive exPlanations), evidenziando la tendenza di SHAP ad assegnare rilevanza a caratteristiche con connessioni a peso zero a causa della sua natura agnostica rispetto al modello.

Risultati

• Efficienza Computazionale: L'approccio basato su SMT ha superato significativamente l'approccio basato su SAT. Per le reti con pesi binari ($S^{bin}_k$), l'SMT ha ridotto i tempi di ricerca da ore (SAT) a secondi (ad esempio, da ~11 ore a ~12 secondi per $k=32$). Per le reti con pesi ternari ($S^{tern}_k$), i tempi di ricerca SMT sono variati da 0,27 a 1,0 ore.
• Qualità della Spiegazione: Le spiegazioni generate erano insiemi minimi di pixel attivi o inattivi sufficienti per innescare la classificazione.
• Confronto con SHAP:
  • SHAP ha identificato erroneamente le caratteristiche con connessioni a peso zero come rilevanti in circa il 47% dei casi (media tra i campioni).
  • L'aumento della dimensione del campione per SHAP ha ridotto questo tasso di errore ma ha aumentato drasticamente il tempo di calcolo (ad esempio, 173 secondi per 1M di campioni).
  • Al contrario, il metodo proposto basato sulla logica garantisce matematicamente che nessuna caratteristica a peso zero venga inclusa nella spiegazione.

Significato e Rivendicazioni

Gli autori posizionano questo lavoro come un passo fondamentale per rendere le BSNN interpretabili attraverso la logica formale. Affermano che, sfruttando la struttura causale inerente alle BSNN, è possibile generare spiegazioni che siano non solo efficienti ma anche formalmente garantite come prive di caratteristiche irrilevanti — una proprietà che i metodi statistici o agnostici rispetto al modello come SHAP non possono fornire.

Il documento nota con modestia che l'attuale lavoro si concentra esclusivamente sulle spiegazioni abduttive (AXp) e sulle architetture completamente connesse. Gli autori suggeriscono che il framework sia estendibile a concetti causali più complessi (come la causa effettiva e le cause NESS) e ad altre architetture, come le BSNN convoluzionali (C-BSNN) e le reti addestrate su dataset linguistici, sebbene questi siano identificati come direzioni per la ricerca futura piuttosto che successi attuali.