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

Technische Samenvatting: Voorbij de But-for Test: Counterfactual Verklaring in Abstract Argumentatie via Actuele Causaliteit

Probleemstelling
In het vakgebied van Explainable AI (XAI) biedt abstracte argumentatie (AA) gestructureerde verklaringen voor waarom argumenten worden geaccepteerd onder specifieke semantiek. Hoewel bestaande methoden post-hoc vragen beantwoorden door sets argumenten te identificeren die voldoen aan eigenschappen zoals Relevantie, Monotoniciteit of Noodzakelijkheid, vertrouwen zij vaak op statische lijsten van redenen. Menselijk redeneren maakt echter frequent gebruik van counterfactual denken ("wat als"-scenario's) om causale afhankelijkheden te onderzoeken.

Huidige benaderingen van counterfactual verklaring in AA zijn beperkt tot de but-for test (BFT). Deze primitieve test vraagt of de acceptatiestatus van een onderwerp-argument zou veranderen als één vermoedelijke oorzaak zou worden gewijkt (bijvoorbeeld door een aanval te verwijderen of een nieuwe aanvaller toe te voegen). Het artikel identificeert een kritiek gebrek in deze benadering: het faalt om andere argumenten vast te houden als "getuigen" (witnesses). Bijgevolg levert de but-for test contra-intuïtieve resultaten op in complexe argumentatiestructuren, specifiek bij Preemption (waarbij één oorzaak een andere blokkeert) en Overdetermination (waarbij meerdere oorzaken gezamenlijk voldoende zijn). In deze gevallen kan het wijzigen van een enkele oorzaak de uitkomst niet veranderen omdat alternatieve paden worden geactiveerd, wat leidt ertoe dat de BFT onjuist oorzaken identificeert of mist.

Methodologie
Om de beperkingen van de but-for test te overwinnen, introduceren de auteurs een interventie-gebaseerd counterfactual redeneerframework dat geworteld is in Structurele Vergelijkingen Modellen (SEMs) en de Halpern–Pearl (HP) definitie van actuele causaliteit.

1. Acceptabiliteitsmodel: Het framework codeert de acceptatievoorwaarden van argumenten als een set vergelijkingen. Het label van een argument $\alpha$ ($in$, $out$, of $und$) wordt bepaald door de labels van de aanvallers van $\alpha$. Dit transformeert het argumentatieframework (AF) naar een model $M_F$ van functies.
2. Interventie Operator: De auteurs definiëren een interventie operator $[\psi]$ die het model $M_F$ wijzigt volgens een hypothese $\psi$ (een conjunctie van atomaire proposities). In tegenstelling tot eenvoudige graafmodificaties, doet deze operator het volgende:
   • Vervangt de acceptatievergelijking van het geïntervenieerde argument(en) door een constante functie die de gestipuleerde label teruggeeft.
   • Maakt samengestelde hypothesen mogelijk, wat de gelijktijdige modificatie van meerdere argumenten mogelijk maakt.
   • Ondersteunt cruciaal het vastzetten van getuige-argumenten op hun werkelijke labels, waardoor alternatieve paden de counterfactual evaluatie niet verstoren.
3. Verfijnde Counterfactual Conditie (AC2m): Voorbijgaand aan de BFT, adopteert het artikel een gemodificeerde counterfactual conditie, AC2m. Een hypothese $\psi$ is een actuele oorzaak als:
   • Actualiteit (AC1): $\psi$ en het effect standhouden in de oorspronkelijke labeling.
   • Gemodificeerde Counterfactual (AC2m): Er bestaat een modificatie $\psi'$ van $\psi$ en een set vaste getuigen $\chi$ (argumenten die op hun werkelijke labels worden gehouden) zodanig dat interveniëren met $\psi' \land \chi$ de status van het onderwerp-argument verandert.
   • Minimaliteit (AC3): De oorzaak bevat geen redundante delen.

Belangrijkste Bijdragen

• Formeel Framework voor Actuele Causaliteit in AA: Het artikel legt de eerste formele link tussen HP actuele causaliteit en abstracte argumentatie, bewegend voorbij de primitieve but-for test.
• Afhandeling van Preemption en Overdetermination: Door getuigen vast te zetten, identificeert de methode correct oorzaken in scenario's waar de but-for test faalt.
  • Preemption: In een scenario waarin $\alpha$ $\beta$ verhindert om $\eta$ te verdedigen, faalt de but-for test om $\alpha$ als oorzaak te identificeren omdat het verwijderen van $\alpha$ $\beta$ heractiveert. De voorgestelde methode zet $\beta$ (of het pad dat het gebruikt) vast naar de werkelijke staat, waardoor $\alpha$ als de ware oorzaak wordt onthuld.
  • Overdetermination: In scenario's waar zowel $\alpha$ als $\beta$ voldoende zijn om $\eta$ te verdedigen, faalt de but-for test om één van beide als oorzaak te identificeren (omdat het verwijderen van de een de ander achterlaat). De voorgestelde methode identificeert de conjunctie $in(\alpha) \land in(\beta)$ als de actuele oorzaak.
• Visualisatie van Graaf-Mutilatie: De auteurs mappen de logische interventie naar grafische operaties op AF's (het toevoegen van aanvallers, het verwijderen van aanvallen, of het toevoegen van zelf-loops), wat een visueel tegenovergestelde vormt voor de algebraïsche interventie.
• Vergelijkende Analyse: Het artikel vergelijkt de nieuwe methode met bestaande argument-gebaseerde verklaringen (Root Reasons, Sufficient/Necessary sets) en closest-world counterfactuals. Het demonstreert dat de voorgestelde methode selectiever en betrouwbaarder is, met name door het vermijden van het "lege verklaring"-probleem dat voorkomt bij closest-world benaderingen wanneer unieke etiketteringen bestaan.

Resultaten en Eigenschappen

• Expressiviteit: De methode ondersteunt samengestelde hypothesen, waardoor de verklaring van gezamenlijke oorzaken mogelijk wordt, wat de but-for test (beperkt tot atomaire wijzigingen) niet kan vatten.
• Relevantie: De methode voldoet aan de Relevantie-eigenschap; alle argumenten in een verklaring zijn relevant voor het onderwerp.
• Niet-monotoniciteit: In tegenstelling tot sommige traditionele verklaringmethoden is de counterfactual verklaring niet monotoon. Het toevoegen van argumenten aan een geldige verklaring kan de Minimaliteit conditie schenden.
• Superieur in Specifieke Structuren:
  • In Preemption identificeert de methode het preëmptende argument als de oorzaak, terwijl Root Reasons irrelevante verdedigers kan bevatten, en Closest-World benaderingen mogelijk geen verklaring opleveren.
  • In Overdetermination identificeert de methode de gezamenlijke noodzakelijkheid van meerdere argumenten, terwijl Root Reasons en Sufficient verklaringen vaak falen om de symmetrische verdedigers te onderscheiden of triviale sets teruggeven.
  • De methode garandeert de Bestaan van een verklaring voor geaccepteerde sink nodes, een eigenschap waarbij Closest-World benaderingen falen wanneer het AF slechts een unieke labeling toelaat.

Significantie en Claims
Het artikel claimt dat door de Halpern–Pearl definitie van actuele causaliteit te integreren in abstracte argumentatie, het voorgestelde framework een verfijndere en meer mens-gealigneerde benadering van counterfactual verklaring biedt. Het stelt dat het vermogen om getuigen vast te houden essentieel is voor het correct identificeren van oorzaken in complexe afhankelijkheidsstructuren, en daarmee de "but-for" beperking overwint die huidige AA verklaringmethoden teistert. De auteurs positioneren dit werk als een stap naar robuustere XAI in argumentatie, waarbij een logische taal wordt geboden die expressief genoeg is om cyclische afhankelijkheden en complexe causale patronen zoals preemption en overdetermination te hanteren, terwijl het geworteld blijft in de structurele eigenschappen van argumentatieframeworks. Er wordt opgemerkt dat toekomstig werk noodzakelijk is om de computationele complexiteit aan te pakken, naar andere semantieken (grounded, preferred, stable) te worden uitgebreid, en het framework toe te passen op uitgebreide argumentatieformalismen (PAF, ADF, ASPIC+).