Riepilogo Tecnico: L'Impossibilità dell'Attribuzione

1. Enunciato del Problema

Il documento affronta una limitazione fondamentale nell'IA spiegabile (XAI): l'affidabilità delle classifiche di importanza delle caratteristiche quando le caratteristiche di input sono collineari. Sebbene metodi come SHAP (SHapley Additive exPlanations) siano ampiamente utilizzati per spiegare le previsioni dei modelli, gli autori dimostrano che, per caratteristiche collineari, la classifica di importanza non è una proprietà stabile della relazione modello-dati, bensì un artefatto stocastico del processo di addestramento.

Nello specifico, il documento indaga se una classifica delle caratteristiche possa soddisfare simultaneamente tre requisiti:

1. Fedele: La classifica riflette le attribuzioni specifiche apprese da una singola istanza del modello.
2. Stabile: La classifica è riproducibile attraverso diverse esecuzioni di addestramento (ad esempio, diversi semi casuali) della stessa architettura di modello sugli stessi dati.
3. Completa: La classifica fornisce un ordinamento rigoroso per ogni coppia di caratteristiche (nessun pareggio).

La tesi centrale è che, in condizioni di collinearità delle caratteristiche (correlazione $\rho > 0$), è matematicamente impossibile soddisfare simultaneamente tutte e tre le condizioni.

2. Metodologia e Quadro Teorico

La Proprietà di Rashomon e il Teorema di Impossibilità

Il contributo teorico fondamentale è il Teorema di Impossibilità dell'Attribuzione (Teorema 5). La dimostrazione si basa sulla Proprietà di Rashomon, che postula che, per caratteristiche collineari, esistano molteplici modelli quasi ottimali (l'insieme di Rashomon) che classificano caratteristiche simmetriche in ordini opposti.

• Logica della Dimostrazione: Se una classifica è completa, deve scegliere un ordine (ad esempio, $j \succ k$). Se è stabile, questo ordine deve valere per tutti i modelli. Tuttavia, la proprietà di Rashomon garantisce l'esistenza di un modello in cui $k \succ j$. Pertanto, la classifica non può essere sia fedele a quel modello specifico sia stabile attraverso l'insieme.
• Limiti Quantitativi: Il documento deriva limiti quantitativi sulla gravità di questa instabilità per diverse classi di modelli:
  • Gradient Boosting (GBDT): Il rapporto di attribuzione (dominanza della caratteristica "prima mossa") diverge come $1/(1-\rho^2)$ (o $1/(1-\alpha\rho^2)$ con correzioni per la profondità).
  • Lasso: Il rapporto è infinito ($\infty$) per qualsiasi $\rho > 0$ a causa della selezione rigida.
  • Reti Neurali: L'instabilità è condizionata dall'inizializzazione e dalle dinamiche di addestramento, ma segue pattern simili di rottura della simmetria.
  • Random Forest: Mostra una violazione limitata ($1 + O(1/\sqrt{T})$) dovuta all'addestramento indipendente degli alberi, in contrasto con l'instabilità divergente del boosting sequenziale.

La Dicotomia Bayesiana Simmetrica

Gli autori generalizzano questo risultato utilizzando la Dicotomia Bayesiana Simmetrica (Teorema 37), un teorema a due famiglie della teoria decisionale invariante. Dimostrano che per qualsiasi problema decisionale simmetrico (dove la distribuzione dei dati è invariante sotto le permutazioni delle caratteristiche), l'insieme raggiungibile di soluzioni collassa in esattamente due famiglie:

• Famiglia A (Singolo Modello): Fedele e completa, ma instabile (infedeltà $U = 1/2$ per coppie simmetriche).
• Famiglia B (Ensemble): Stabile e fedele alla media della popolazione, ma incompleta (segnala pareggi per caratteristiche simmetriche, $U=0$).
  Non esiste una terza opzione.

Risoluzione Costruttiva: DASH

Per risolvere l'impossibilità, il documento propone DASH (Diversified Aggregation of SHAP). Questo è un metodo di ensemble che media i valori SHAP su $M$ modelli addestrati indipendentemente.

• Meccanismo: Mediando, DASH annulla il bias casuale della "prima mossa" intrinseco nei singoli modelli, convergendo verso l'aspettativa della popolazione.
• Ottimalità: DASH è dimostrato essere Pareto-ottimale tra le aggregazioni non distorte. Raggiunge il limite di varianza di Cramér–Rao ($\sigma^2/M$) per la stabilità della classifica.
• Compromesso: DASH sacrifica la completezza intra-gruppo (segnala pareggi per caratteristiche simmetriche) per guadagnare stabilità e fedeltà inter-gruppo.

Verifica Formale

Una parte significativa della metodologia coinvolge la verifica meccanica utilizzando Lean 4.

• Gli autori hanno formalizzato l'intero quadro teorico, inclusi il teorema di impossibilità, i limiti quantitativi e la dimostrazione di ottimalità di DASH.
• La formalizzazione consiste in 305 teoremi verificati per tipo distribuiti su 54 file con 0 sorry (nessuna assunzione non dimostrata).
• Il processo ha coinvolto 16 assiomi (14 specifici del dominio, 2 per la complessità delle query). Si noti che il teorema centrale di impossibilità richiede zero assiomi comportamentali, basandosi esclusivamente sulla proprietà di Rashomon.
• Il processo di formalizzazione ha identificato due incongruenze logiche e un disallineamento di tipo nel sistema assiomatico informale originale.

3. Risultati Chiave e Validazione Empirica

Risultati Empirici

Il documento convalida la teoria su 77 dataset pubblici e molteplici implementazioni di modelli (XGBoost, LightGBM, CatBoost, Reti Neurali).

• Prevalenza: In un sondaggio su 77 dataset, il 68% ha mostrato instabilità di attribuzione (tasso di inversione > 10%) per coppie di caratteristiche correlate. Per dataset ad alta dimensionalità ($P \ge 20$), questo tasso sale al 93%.
• Tassi di Inversione: Per coppie altamente correlate ($\rho \approx 0.9$) con importanza simile, il tasso di inversione si avvicina al massimo teorico del 50% (un lancio di moneta) attraverso diversi semi di re-addestramento.
• Efficacia di DASH: La media di ensemble con $M \ge 25$ modelli riduce il tasso di inversione al di sotto dell'1%, risolvendo efficacemente l'instabilità.
• Diagnostica: Il documento introduce un Test Z Multi-Modello e un Filtro a Singolo Modello (basato sulle frequenze di divisione) per rilevare coppie instabili. Il Test Z mostra una forte correlazione negativa ($r \approx -0.89$) con i tassi di inversione osservati.

Comportamenti Specifici per Classe di Modello

• GBDT: Mostra instabilità divergente. La caratteristica "prima mossa" assorbe il segnale, lasciando segnale residuo per le altre, creando un ampio divario di attribuzione che si inverte in base a quale caratteristica viene selezionata per prima.
• Lasso: Mostra instabilità infinita poiché seleziona esattamente una caratteristica da un gruppo correlato.
• Reti Neurali: Mostrano alta instabilità (87% delle coppie instabili sui dati sul cancro al seno), guidata dall'insieme di Rashomon più ampio e dalla varianza di KernelSHAP.
• Random Forest: Mostrano un'instabilità significativamente inferiore a causa della mancanza di condivisione sequenziale dei residui.

Estensioni

• Attribuzione Condizionale: Il documento dimostra che passare a SHAP condizionale non sfugge all'impossibilità se gli effetti causali delle caratteristiche sono uguali ($\beta_j = \beta_k$).
• Audit di Equità: Gli autori dimostrano che gli audit di discriminazione tramite proxy basati su SHAP di un singolo modello sono provatamente inaffidabili in presenza di collinearità, poiché la conclusione (quale caratteristica è il proxy) è un lancio di moneta.
• Identificazione Causale: L'instabilità riflette la difficoltà dell'identificazione causale in presenza di collinearità, con una complessità del campione che diverge come $1/(1-\rho)^2$.

4. Significato e Affermazioni

Il documento afferma di fornire il primo risultato di impossibilità formalmente verificato nell'IA spiegabile. Il suo significato è inquadrato in tre dimensioni:

1. Necessità Matematica: L'instabilità non è un fallimento ingegneristico (ad esempio, iperparametri scadenti o bug) ma un'inevitabilità matematica che deriva dalla geometria del paesaggio della perdita e dall'insieme di Rashomon. Il documento riformula il problema da "come correggere SHAP" a "cosa è raggiungibile dati i vincoli".
2. Caratterizzazione dello Spazio di Progettazione: Definendo lo Spazio di Progettazione dell'Attribuzione, il documento stabilisce che i praticanti devono scegliere tra stabilità e completezza. Non esiste un "pranzo gratis" in cui un singolo modello fornisca una classifica stabile, fedele e completa.
3. Impatto Normativo e Pratico:
   • Conformità all'AI Act dell'UE: Il documento sostiene che l'instabilità di attribuzione costituisce una "circostanza nota e prevedibile" ai sensi dell'articolo 13(3)(b)(ii) dell'AI Act dell'UE. I fornitori devono divulgare questa instabilità piuttosto che presentare classifiche arbitrarie come fatti.
   • Equità: Gli audit di equità su singolo modello sono considerati inaffidabili per caratteristiche correlate, portando potenzialmente a falsi positivi o negativi nel rilevamento della discriminazione tramite proxy.
   • Toolkit Azionabile: Il documento fornisce un flusso di lavoro concreto (Filtro $\to$ Test Z $\to$ DASH) e una formula per la dimensione minima dell'ensemble ($M_{min}$) necessaria per raggiungere un livello di stabilità desiderato.

Gli autori concludono che il campo deve allontanarsi dal "paradigma del singolo modello" per le spiegazioni in presenza di collinearità e adottare approcci basati su ensemble come DASH per fornire spiegazioni oneste, stabili e difendibili.