Kontrastiiviset selitykset: Tekoälyn selitettävyyttä logiikan avulla

Abstract

Tässä työssä tarkastellaan kontrastiivisia selityksiä matemaattisen logiikan näkökulmasta. Tarkoituksena on esitellä menetelmä luokittelijoiden selitysten ja kontrastien esittämiseen. Lisäksi esiteltävästä menetelmästä osoitetaan useita ominaisuuksia, ja sitä tarkastellaan tarkemmin esimerkkien avulla. Aluksi työssä määritellään logiikat joukkojen ja symbolien avulla. Yleisimmässä tapauksessa logiikat ovat pikemminkin algebrallisia objekteja. Lisäksi esitellään, millaisia ehtoja logiikoiden tulisi toteuttaa, jotta ne toimisivat luonnollisesti päättelytehtävissä. Yleisen logiikan määritelmän jälkeen keskitytään lauselogiikkaan, jossa haluttu semantiikka määritellään totuusfunktioiden avulla. Lauselogiikalle määritellään tarvittavia rakenteita, kuten CNF-kaavat ja kaavan koko. Perusmääritelmien jälkeen kuvataan, mitä tarkoitetaan luokituksilla, selityksillä ja kontrasteilla logiikan näkökulmasta. Näiden pohjalta määritellään globaali kontrastiivinen selitysongelma. Ongelmasta esitetään esimerkkejä, joiden ratkaisujen optimaalisuus osoitetaan aputulosten avulla. Lopuksi tarkastellaan ongelman vaihtoehtoisia muotoiluja ja määritellään globaalien selitysongelmien perhe. Tälle perheelle määritetään ratkaisujen ylä- ja alarajat käytettävän aakkoston koon suhteen. Työstä voidaan päätellä, että logiikoiden avulla voidaan kuvata luokittelijoita, selityksiä ja kontrasteja mielekkäästi. Lauselogiikan tapauksessa ratkaisuja voidaan löytää myös käsin pienemmissä tapauksissa. Toisaalta havaitaan, että rajoittamalla käytettäviä kaavoja voidaan löytää yleisiä ratkaisuja.

In this master’s thesis, a framework for discovering contrastive explanations is defined using mathematical logic. Classifiers, explanations, and contrasts are defined abstractly within logics. The framework is also shown to possess several useful semantic properties. The definitions are illustrated through several examples. First, the basic definitions of logics are presented in an abstract manner. Without additional restrictions, logics are better understood as algebraic objects. Several properties are then introduced to constrain logics so that they behave naturally in deductive tasks. Next, propositional logic is defined using truth functions, which also satisfy the aforementioned properties. Finally, several useful concepts are introduced for propositional logic, such as CNF formulas and the size function. After establishing the basic definitions, the necessary concepts are introduced, including classifiers, explanations, and contrasts. Based on these, a global contrastive explanation problem is defined. In addition, several example problems are solved using properties of the size function. Finally, alternative formulations of the problem are studied. A family of global contrastive explanation problems is also defined, for which upper and lower bounds on the size of the solutions are established. Based on the results, it can be concluded that logics can be used to describe classifiers, explanations, and contrasts in a meaningful way. The results also show that, in propositional logic, small instances of the global contrastive explanation problem can be solved manually. Furthermore, they indicate that by restricting the class of formulas used, general solutions can be found even in larger cases.