🤖 AI

Rethinking Explanations: Formalizing Contrast in Description Logics

Dit artikel stelt een gebruikersgericht raamwerk voor voor contrastieve verklaringen in beschrijvingslogica dat de beperkingen van bestaande methoden voor rechtvaardiging en abductief redeneren aanpakt door formeel te definiëren en te evalueren hoe verklaard kan worden waarom een feit waar is in plaats van een alternatief tegenbeeld.

Oorspronkelijke auteurs: Yasir Mahmood, Arnab Sharma, Axel-Cyrille Ngonga Ngomo, Balram Tiwari

Gepubliceerd 2026-05-06

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Yasir Mahmood, Arnab Sharma, Axel-Cyrille Ngonga Ngomo, Balram Tiwari

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je door een gigantische, magische bibliotheek loopt waar elk boek een regel vertegenwoordigt over hoe de wereld werkt. Deze bibliotheek is gebouwd op een zeer strikte, logische taal genaamd Beschrijvingslogica (DL). In deze bibliotheek kan een computer een persoon bekijken (laten we hem Alice noemen) en een reeks regels, en kan hij je zeggen: "Ja, Alice is aangenomen!"

De Oude Manier: "Waarom?"

Normaal gesproken, als je de computer vraagt: "Waarom is Alice aangenomen?", geeft hij je een Redenering. Hij pakt de specifieke pagina's uit de bibliotheek die bewijzen dat Alice is aangenomen.

Analogie: Het is alsof een leraar je de exacte stappen in een wiskundeprobleem toont om te bewijzen dat het antwoord 5 is. Het is accuraat, maar het vertelt je alleen over de "winnaar".

Het Nieuwe Probleem: "Waarom Alice en niet Bob?"

De auteurs van dit artikel merkten iets op dat mensen van nature doen: we willen niet alleen weten waarom iets gebeurde; we willen weten waarom het gebeurde in plaats van iets anders.

Stel je voor dat Alice de baan krijgt, maar haar vriend Bob niet.

Als je vraagt: "Waarom Alice?", somt de computer Alice's geweldige vaardigheden op.
Als je vraagt: "Waarom niet Bob?", somt de computer Bob's ontbrekende vaardigheden op.
Maar Bob is verward. Hij wil geen twee aparte lijsten. Hij wil weten: "Waarom Alice en niet ik?" Hij wil het verschil tussen hen zien.

Het artikel stelt dat het geven van twee aparte antwoorden onbevredigend is. Je hebt een Contrastieve Verklaring (CV) nodig die de specifieke kloof tussen de twee benadrukt.

De Oplossing: De "Verschilzoeker"

De onderzoekers bedachten een nieuwe manier om deze "Waarom P in plaats van Q?"-vraag te formaliseren. Ze noemen het ding dat gebeurde het Feit (Alice) en het ding dat niet gebeurde de Contrast (Bob).

Om het verschil uit te leggen, kijken ze naar drie dingen:

Wat Alice had en Bob niet: (bijv. Alice publiceerde in AI).
Wat Bob had en Alice niet: (bijv. Bob publiceerde in zuivere wiskunde).
Wat Bob mistte en wat hem zou hebben aangenomen: (bijv. Bob moest publiceren in AI).

De Creatieve Analogie: De Race
Stel je een race voor tussen Alice en Bob.

Feit: Alice won.
Contrast: Bob verloor.
Oude Verklaring: "Alice rende snel." (Waar, maar legt niet uit waarom Bob verloor).
Nieuwe Contrastieve Verklaring: "Alice rende snel omdat ze trainde op heuvels, terwijl Bob trainde op vlakke grond. Als Bob op heuvels had getraind (het ontbrekende stukje), had hij gewonnen, maar dat deed hij niet."

Het artikel formaliseert dit door het "bewijs" voor Alice en het "bewijs" voor Bob (hoewel Bob's bewijs hypothetisch is) te nemen en het symmetrische verschil te vinden. Ze halen de dingen weg die ze beiden delen (zoals "beiden zijn gekwalificeerd") en focussen alleen op de unieke factoren die de uitkomst bepaalden.

Het "Wat als"-Scenario (Abductie)

Soms moet de computer raden wat er zou moeten gelden om het Contrast waar te maken. Dit heet Abductie.

Analogie: Als Bob niet werd aangenomen, vraagt de computer: "Wat zou waar moeten zijn voor Bob om aangenomen te worden?" Het zou kunnen zeggen: "Als Bob in AI had gepubliceerd."
De methode van het artikel combineert het echte bewijs voor Alice met dit "wat als"-scenario voor Bob om precies te laten zien waar de paden uit elkaar gingen.

Omgaan met Glitches (Inconsistenties)

Soms zijn de regels in de bibliotheek lastig. Wat als de regels zeggen: "Je kunt niet tegelijkertijd een AI-expert en een theoreticus zijn"?

Als Bob een theoreticus is, en de computer zegt: "Als Bob een AI-expert was, zou hij zijn aangenomen", is er een conflict.
Het artikel voegt een veiligheidsnet toe: het identificeert deze conflicten. Het vertelt je: "Bob zou zijn aangenomen als hij een AI-expert was, MAAR dat staat in strijd met zijn aard als theoreticus." Dit voorkomt dat de verklaring de logica van de bibliotheek breekt.

Wat Ze Eigenlijk Dedden

De auteurs schreven niet alleen theorie; ze bouwden een prototype (een werkend computerprogramma) om dit te testen.

Ze testten het op ongeveer 40 verschillende real-world kennisbasissen (zoals medische of technische databases).
Ze ontdekten dat hun methode snel werkt (in minder dan een seconde voor de meeste gevallen) en zeer korte, makkelijk te lezen verklaringen produceert (meestal slechts 1 of 2 zinnen logica).
Ze bewezen wiskundig dat voor bepaalde soorten logica (genaamd EL) dit proces efficiënt is en niet vastloopt in een eindeloze lus.

Samenvatting

Dit artikel gaat over het upgraden van hoe computers beslissingen uitleggen. In plaats van alleen te zeggen "Hier is waarom X gebeurde", zeggen ze nu: "Hier is waarom X gebeurde in plaats van Y". Ze doen dit door het "winnende" bewijs wiskundig te vergelijken met het "verliezende" (of hypothetische) bewijs, de gemeenschappelijke delen weg te halen, en je precies te laten zien wat het verschil maakte. Ze bouwden een tool om dit te doen, en het werkt snel en accuraat op complexe data.

Technische Samenvatting: Het Heroverwegen van Verklaringen: Het Formaliseren van Contrast in Beschrijvingslogica's

Probleemstelling
Bestaande verklaringsformaliseringen voor kennisbanken (KB's) in Beschrijvingslogica (DL) richten zich voornamelijk op justificaties (uitleggen waarom een axioma $P$ waar is) en abductief redeneren (uitleggen waarom een ontbrekend axioma $P$ waar zou kunnen zijn). Deze benaderingen missen echter een gebruikersgerichte perspectief. Ze slagen er niet in om in te spelen op de specifieke cognitieve behoeften van een vraagsteller die vaak verrast is door een feit $P$ , omdat deze een alternatief gebeurtenis $Q$ had verwacht. Het bieden van afzonderlijke verklaringen voor "waarom $P$ " en "waarom niet $Q$ " is vaak onbevredigend, aangezien gebruikers de specifieke verschil tussen het feitelijke resultaat en het verwachte alternatief willen begrijpen. Hoewel contrastieve verklaringen (CV's) goed bestudeerd zijn in machine learning en argumentatiekaders, blijven ze grotendeels onontgonnen in de context van DL's, ondanks dat DL's de basis vormen voor ontologieën zoals OWL die worden gebruikt in kritieke domeinen zoals de gezondheidszorg (bijv. SNOMED CT).

Methodologie
De auteurs stellen een formeel kader voor het genereren van contrastieve verklaringen binnen DL KB's voor, waarbij het filosofische model van contrastieve verklaring van Peter Lipton wordt aangepast aan de logische setting van DL's.

Formalisatie van Contrastvragen (CV's):
Een CV wordt gedefinieerd als een paar $(P, Q)$ waarbij $P$ een feit is (een afgeleide ABox-assertie, bijv. $C(x)$ ) en $Q$ een tegenhanger is (een niet-afgeleide assertie). Het artikel richt zich op twee specifieke typen tegenhangers:
- Entiteitscontrasten: $Q$ is $C(y)$ , waarbij hetzelfde concept wordt gecontrasteerd tegen een ander individu.
- Conceptcontrasten: $Q$ is $D(x)$ , waarbij een ander concept wordt gecontrasteerd voor hetzelfde individu.
Definiëren van de Contrastieve Verklaring (CV):
De auteurs gaan voorbij aan een eenvoudige symmetrische verschil tussen de justificatie van $P$ en de abductieve hypothese voor $Q$ . Ze introduceren een tuple-gebaseerde definitie $E = \langle E_{fact}, E_{foil+}, E_{foil-} \rangle$ (en optioneel een conflictset $C$ ) gebaseerd op drie principes:
- Verschilvoorwaarde: De verklaring moet het verschil noemen tussen de redenen voor $P$ en de ontbrekende feiten voor $Q$ .
- Bekende versus Aangenomen Kennis: De verklaring moet onderscheid maken tussen axioma's die waar zijn in de KB met betrekking tot de tegenhanger ( $E_{foil+}$ ) en de ontbrekende axioma's die nodig zijn om de tegenhanger af te leiden ( $E_{foil-}$ ).
- Rekening houden met Gelijkaardige Axioma's: Het kader introduceert een "hernoemde setverschil"-operator ( $\ddagger$ ). Deze operator verwijdert axioma's die structureel vergelijkbaar zijn tussen het feit en de tegenhanger (bijv. $C(x)$ en $C(y)$ , of $E \sqsubseteq C$ en $E \sqsubseteq D$ ) om ervoor te zorgen dat de verklaring alleen de onderscheidende factoren benadrukt.
Omgaan met Inconsistenties:
Als het toevoegen van de ontbrekende axioma's voor de tegenhanger ( $E_{foil-}$ ) een conflict creëert met de bestaande KB, bevat het kader een conflictset $C$ . Deze set vertegenwoordigt het minimale deel van bestaande ABox-asserties dat moet worden verwijderd om de tegenhanger af te leiden, wat effectief een contrafactual scenario modelleert.
Voorkeurscriteria:
Om te kiezen tussen meerdere mogelijke CV's, stellen de auteurs een syntactische divergentie-maatstaf ( $\sigma_{div}$ ) voor. Deze maatstaf meet het symmetrische verschil tussen de axioma's relevant voor het feit en die relevant voor de tegenhanger. Een voorkeurs-CV is er een die deze divergentie minimaliseert, waardoor de redeneerstructuren van het feit en de tegenhanger zo dicht mogelijk bij elkaar worden gebracht om vergelijking te faciliteren.

Belangrijkste Bijdragen

Formele Definities: Het artikel biedt de eerste formele definities van contrastieve verklaringen voor DL KB's, specifiek gericht op zowel entiteits- als conceptcontrasten.
Algemeen Kader: Het presenteert een algemeen kader voor CV's dat justificaties en abductieve hypothesen integreert, terwijl het onderscheid maakt tussen waar en ontbrekende asserties.
Complexiteitsanalyse: De auteurs analyseren de computationele complexiteit van CV's in twee DL's:
- $\mathcal{EL}$ : Ze bewijzen dat het beslissen van het bestaan van een CV van een gegeven grootte NP-volledig is voor conceptcontrasten. Voor entiteitscontrasten kan echter een $\sigma_{div}$ -voorkeurs-CV (met divergentie 0) in polynomiale tijd worden berekend.
- $\mathcal{ALC}$ : Het probleem van het beslissen van het bestaan van een CV van een gegeven grootte blijkt ExpTime-volledig te zijn.
Implementatie en Evaluatie: Een prototype-implementatie in Java (met behulp van OWL API en ELK-reasoner) is ontwikkeld. Experimenten zijn uitgevoerd op ongeveer 41 real-world OWL KB's.

Resultaten
De experimentele evaluatie leverde de volgende bevindingen op:

Efficiëntie: Het prototype berekent CV's efficiënt, met een gemiddelde runtime van ongeveer 392 ms.
Grootte van Verklaringen: De gegenereerde verklaringen zijn compact, typisch beslaand tot vier ABox-axioma's.
Gemeenschappelijkheid: De "ratio van gemeenschappelijke axioma's" (de overlap tussen justificaties van feit en tegenhanger) bleek laag te zijn (gemiddeld 13,5%), wat suggereert dat in veel gevallen het feit en de tegenhanger steunen op verschillende sets van asserties.
Consistentie: Het conflictratio was laag (4,00%), wat aangeeft dat in de meeste gevallen de ontbrekende axioma's voor de tegenhanger niet in strijd zijn met de bestaande KB.

Betekenis en Beweringen
Het artikel claimt een significante kloof in de literatuur te dichten door contrastieve verklaringen in te voeren in het domein van Beschrijvingslogica's. De auteurs betogen dat deze benadering een meer intuïtieve en gebruikersgerichte manier biedt om redeneeruitkomsten te verklaren door expliciet de verwachtingen van de vraagsteller (de tegenhanger) te modelleren.

Het werk wordt gepresenteerd als een voorlopige stap in dit gebied. De auteurs merken bescheiden op dat hoewel hun definities uitbreiden naar elke DL die abductieve hypothesen ondersteunt, er verder werk nodig is om expressievere DL's te behandelen (bijv. met kardinaliteitsbeperkingen) en om algoritmen te ontwikkelen die efficiënt schalen naar grote datasets. Ze identificeren ook de behoefte aan toekomstige gebruikersstudies om te valideren of deze contrastieve verklaringen inderdaad worden verkiest boven standaardjustificaties door eindgebruikers. Het artikel concludeert dat hun kader een rigoureus, formeel mechanisme biedt voor het combineren van justificaties om het verschil tussen een feit en een tegenhanger te verklaren, en zo de basis legt voor beter onderbouwde besluitvorming in semantische webtoepassingen.