Beyond But-for Test: Counterfactual Explanation in Abstract Argumentation via Actual Causality (Extended Version)

Sintesi Tecnica: Oltre il Test del "But-for": Spiegazione Controfattuale nell'Argomentazione Astratta tramite la Causalità Reale

Definizione del Problema
Nel campo della XAI (Explainable AI), l'argomentazione astratta (AA) fornisce spiegazioni strutturate sul perché determinati argomenti siano accettati sotto specifiche semantiche. Sebbene i metodi esistenti rispondano a domande post-hoc identificando insiemi di argomenti che soddisfano proprietà come Rilevanza, Monotonicità o Necessità, essi si basano spesso su liste statiche di ragioni. Il ragionamento umano, tuttavia, impiega frequentemente il pensiero controfattuale ("cosa succederebbe se") per indagare le dipendenze causali.

Le attuali metodologie di spiegazione controfattuale nell'AA sono limitate al test del "but-for" (BFT). Questo test primitivo chiede se lo stato di accettazione di un argomento oggetto di analisi cambierebbe se una singola causa sospetta venisse alterata (ad esempio, eliminando un attacco o aggiungendo un nuovo attaccante). Il documento identifica un difetto critico in questo approccio: esso non riesce a mantenere fissi gli altri argomenti come "testimoni" (witnesses). Di conseguenza, il test del but-for produce risultati controintuitivi in strutture di argomentazione complesse, specificamente nella Preemption (dove una causa blocca un'altra) e nell'Overdetermination (dove più cause sono congiuntamente sufficienti). In questi casi, l'alterazione di una singola causa può non cambiare l'esito perché si attivano percorsi alternativi, portando il BFT a identificare erroneamente o a mancare le cause reali.

Metodologia
Per superare i limiti del test del but-for, gli autori introducono un framework di ragionamento controfattuale basato su interventi fondato sui Modelli di Equazioni Strutturali (SEM) e sulla definizione di causalità reale di Halpern–Pearl (HP).

1. Modello di Accettabilità: Il framework codifica le condizioni di accettabilità degli argomenti come un insieme di equazioni. L'etichetta di un argomento $\alpha$ (in, out, o und) è determinata dalle etichette dei suoi attaccanti. Ciò trasforma il framework di argomentazione (AF) in un modello $M_F$ di funzioni.
2. Operatore di Intervento: Gli autori definiscono un operatore di intervento $[\psi]$ che modifica il modello $M_F$ secondo un'ipotesi $\psi$ (una congiunzione di proposizioni atomiche). A differenza delle semplici modifiche ai grafi, questo operatore:
   • Sostituisce l'equazione di accettabilità dell'argomento (o degli argomenti) intervenuto con una funzione costante che restituisce l'etichetta stipulata.
   • Permette di utilizzare ipotesi composte, consentendo la modifica simultanea di più argomenti.
   • Fondamentalmente, supporta il fissaggio degli argomenti testimone ai loro etichette reali, impedendo a percorsi alternativi di distorcere la valutazione controfattuale.
3. Condizione Controfattuale Raffinata (AC2m): Andando oltre il BFT, il documento adotta una condizione controfattuale modificata, AC2m. Un'ipotesi $\psi$ è una causa reale se:
   • Attualità (AC1): $\psi$ ed l'effetto valgono nella etichettatura originale.
   • Controfattuale Modificato (AC2m): Esiste una modifica $\psi'$ di $\psi$ e un insieme di testimoni fissi $\chi$ (argomenti mantenuti alle loro etichette reali) tali che l'intervento con $\psi' \land \chi$ cambi lo stato dell'argomento oggetto di analisi.
   • Minimalità (AC3): La causa non contiene parti ridondanti.

Contributi Chiave

• Framework Formale per la Causalità Reale nell'AA: Il documento stabilisce il primo legame formale tra la causalità reale di HP e l'argomentazione astratta, andando oltre il primitivo test del but-for.
• Gestione di Preemption e Overdetermination: Fissando i testimoni, il metodo identifica correttamente le cause in scenari in cui il test del but-for fallisce.
  • Preemption: In uno scenario in cui $\alpha$ blocca $\beta$ dal difendere $\eta$, il test del but-for non riesce a identificare $\alpha$ come causa perché la rimozione di $\alpha$ riattiva $\beta$. Il metodo proposto fissa $\beta$ (o il percorso che utilizza) al suo stato attuale, rivelando $\alpha$ come la vera causa.
  • Overdetermination: In scenari in cui $\alpha$ e $\beta$ sono entrambi sufficienti per difendere $\eta$, il test del but-for non riesce a identificare nessuno dei due come causa (poiché la rimozione di uno lascia l'altro attivo). Il metodo proposto identifica la congiunzione $in(\alpha) \land in(\beta)$ come la causa reale.
• Visualizzazione della Mutilazione del Grafo: Gli autori mappano l'intervento logico su operazioni grafiche sugli AF (aggiunta di attaccanti, rimozione di attacchi o aggiunta di auto-anelli), fornendo un contrappunto visivo all'intervento algebrico.
• Analisi Comparativa: Il documento confronta il nuovo metodo con le spiegazioni basate su argomenti esistenti (Root Reasons, insiemi Sufficienti/Necessari) e con i controfattuali del mondo più vicino (closest-world). Dimostra che il metodo proposto è più selettivo e affidabile, in particolare nell'evitare il problema della "spiegazione vuota" riscontrato negli approcci di mondo più vicino quando esistono etichettature uniche.

Risultati e Proprietà

• Espressività: Il metodo supporta ipotesi composte, permettendo la spiegazione di cause congiunte, cosa che il test del but-for (limitato a cambiamenti atomici) non può catturare.
• Rilevanza: Il metodo soddisfa la proprietà di Rilevanza; tutti gli argomenti in una spiegazione sono rilevanti per l'argomento oggetto di analisi.
• Non-Monotonicità: A differenza di alcuni metodi di spiegazione tradizionali, la spiegazione controfattuale non è monotona. L'aggiunta di argomenti a una spiegazione valida può violare la condizione di Minimalità.
• Superiorità in Strutture Specifiche:
  • Nella Preemption, il metodo identifica l'argomento che previene come la causa, mentre le Root Reasons possono includere difensori irrilevanti, e gli approcci Closest-World possono non fornire alcuna spiegazione.
  • Nell'Overdetermination, il metodo identifica la necessità congiunta di più argomenti, mentre le Root Reasons e le spiegazioni Sufficienti spesso non riescono a distinguere tra i difensori simmetrici o restituiscono insiemi triviali.
  • Il metodo garantisce l'Esistenza di una spiegazione per i nodi sink accettati, una proprietà in cui gli approcci Closest-World falliscono quando l'AF ammette solo un'etichettatura unica.

Significatività e Rivendicazioni
Il documento sostiene che, integrando la definizione di causalità reale di Halpern–Pearl nell'argomentazione astratta, il framework proposto fornisce un approccio alla spiegazione controfattuale più raffinato e allineato al ragionamento umano. Si afferma che la capacità di mantenere fissi i testimoni è essenziale per identificare correttamente le cause in strutture di dipendenza complesse, superando così il limite del "but-for" che affligge gli attuali metodi di spiegazione nell'AA. Gli autori pongono questo lavoro come un passo verso una XAI più robusta nell'argomentazione, offrendo un linguaggio logico abbastanza espressivo da gestire dipendenze cicliche e pattern causali complessi come la preemption e l'overdetermination, pur rimanendo ancorato alle proprietà strutturali dei framework di argomentazione. Si nota che futuri lavori saranno necessari per affrontare la complessità computazionale, estendere il metodo ad altre semantiche (grounded, preferred, stable) e applicarlo a estensioni del formalismo dell'argomentazione (PAF, ADF, ASPIC+).