Tehokkaiden päättelyjärjestelmien ansiosta vaikeita laskennallisia ongelmia voidaan ratkaista eksaktisti. Palkitussa väitöskirjassa kehitetään automatisoidun päättelyn menetelmiä laskennallisen argumentaation viitekehyksessä.

Tekoälytutkimuksen tavoitteena on kehittää järjestelmiä, jotka toimivat rationaalisesti eli valitsevat tilanteen valossa parhaan mahdollisen vaihtoehdon toimia tavoitteiden saavuttamiseksi. Erityisesti automatisoidussa päättelyssä tutkimuksen kohteena on järjestelmät, jotka tuottavat eksakteja ratkaisuja tietyllä kielellä kuvattuun ongelmaan tai todistuksia siitä, että ratkaisua ei löydy. Sovelluskohteita automatisoiduille päättelyjärjestelmille löytyy sekä akatemian että teollisuuden puolelta: matemaattisia konjektuureja voidaan todistaa hakemalla vastaesimerkkiä kyseiselle väitteelle, ja laitteiston tai ohjelmiston oikeellinen toiminta voidaan verifioida etsimällä virheellistä suoritusta. Rajoiteoptimoinnista taas puhutaan, kun lisäksi halutaan jossakin mielessä paras mahdollinen ratkaisu. Sovelluksissa voidaan tällöin esimerkiksi säästää resursseja kuten aikaa, raaka-aineita tai energiaa.

Päättely tekoälyssä

Kuvitellaan, että ollaan ratkaisemassa päivän sudokua. Tiedetään, että sudokun ratkaisu on 9×9-ruudukko, jossa on numeroita yhdestä yhdeksään. Kaikki tällaiset ruudukot muodostavat sudokun hakuavaruuden. Tiedetään myös sudokun säännöt, nimittäin jokaisen numeron pitää esiintyä joka rivillä, sarakkeella, sekä pienemmässä ruudussa tasan kerran. Tiedetään myös, mitä numeroita on päivän sudokussa valmiiksi täytettynä. Nämä voidaan nähdä rajoitteina hakuavaruuden yli. Automatisoidut päättelyjärjestelmät toimivat erilaisilla matemaattisilla rajoitekielillä, joilla implisiittisesti esitetään ongelman kaikki ratkaisut. Sudokuun voidaan soveltaa automatisoitua päättelyä, kunhan esitetään sudokuun liittyvä tieto valitun järjestelmän kielellä. Kun sudoku on käännetty järjestelmälle sopivaksi syötteeksi, järjestelmän tulosteesta pitää lisäksi tulkita sudokun ratkaisu. Tätä prosessia kutsutaan deklaratiiviseksi lähestymistavaksi ongelmanratkaisuun. Kyseisen lähestymistavan ansiosta yhdellä päättelyjärjestelmällä voidaan ratkaista monia erilaisia laskennallisia ongelmia.

Ratkaisun löytäminen automatisoidussa päättelyssä on laskennallisesti usein hyvin vaativaa. Tämä tarkoittaa sitä, että pahimmassa tapauksessa joudutaan haravoimaan ongelman koko eksponentiaalinen hakuavaruus. Tästä huolimatta automatisoidut päättelyjärjestelmät ovat kehittyneet viime vuosikymmeninä huimaa tahtia, ja pystyvät ratkaisemaan teollisuudestakin kumpuavia suuria ongelmainstansseja tehokkaasti ja luotettavasti. Tämän vuoksi automatisoitua päättelyä pidetään yhtenä tietojenkäsittelytieteen ja tekoälyn suurista menestystarinoista. Palkittu väitöskirja rakentuu osittain tälle menestystarinalle hyödyntämällä niin kutsuttuja toteutuvuustarkastimia, joissa rajoitekielenä toimii lause- eli propositiologiikka, sekä niiden optimointilaajennoksia. Toisaalta väitöskirja myös vie tätä tarinaa eteenpäin kehittämällä uusia päättelymenetelmiä laskennallisen argumentaation ongelmille.

Laskennallinen argumentaatio

Tekoälytutkimuksessa laskennallista argumentaatiota on sovellettu aloilla, joissa päättely on luonteeltaan epämonotonista, kuten lääketieteellisen päätöksenteon tukena ja oikeudellisten sääntöjen mallintamisessa. Epämonotoninen päättely eroaa klassisesta päättelystä siinä mielessä, että seuraukset saatetaan hylätä uuden aineiston pohjalta. Esimerkiksi, jos tiedetään että Tipi on lintu, voidaan oletettavasti päätellä, että Tipi osaa lentää. Jos saadaan lisäksi tietää, että Tipi on tarkkaan ottaen pingviini, lopputuloksena on, että Tipi ei itse asiassa osaakaan lentää. Eräs epämonotonisen päättelyn muoto on abstrakti argumentaatio, jossa tieto esitetään argumentteina ja niiden vasta-argumentteina. Yksi keskeisimmistä laskennallisista ongelmista abstraktissa argumentaatiossa on yksittäisen argumentin hyväksyttävyys. Tämä voidaan taas määrittää ottamalla huomioon kaikkien argumenttien väliset suhteet. Jotta argumenttia voidaan pitää hyväksyttävänä, on löydettävä ristiriidaton näkökulma, joka tukee sitä, eli jokaiselle vasta-argumentille pitää löytyä kyseisestä näkökulmasta vasta-argumentti. Kyseessä on vaativa ongelma, ja tehokkaimmat tunnetut algoritmit pohjautuvat deklaratiiviseen lähestymistapaan sekä automatisoituihin päättelyjärjestelmiin.

Ratkaisun löytäminen automatisoidussa päättelyssä on laskennallisesti usein hyvin vaativaa.

Väitöskirjassa tutkitaan useita abstraktin argumentaation laskennallisia ongelmia, joihin liittyy muutoksia tai epävarmuutta. Esimerkiksi tarkastellaan, kuinka muutetaan argumenttien välisiä suhteita mahdollisimman vähän niin, että annetuista argumenteista tulee hyväksyttäviä, sekä abstraktin argumentaation yleistyksiä, joissa argumentit tai niiden väliset suhteet voivat olla epävarmoja. Ongelmien teoreettista laskennallista vaativuutta analysoidaan tarkasti ottaen huomioon monet erilaiset ongelmien variaatiot. Käytännössä taas kehitetään deklaratiivisia ratkaisualgoritmeja, jotka käyttävät tehokkaita päättely- ja optimointijärjestelmiä. Teoria ja käytäntö ovat kuitenkin vahvasti yhteen punoutuneita, sillä laskennallisella vaativuudella ja automatisoidulla päättelyllä on vahva vuorovaikutus keskenään. Vaativuusanalyysin tuloksesta voidaan esimerkiksi päätellä, että ongelmaa ei voi tehokkaasti kääntää tietyn päättelyjärjestelmän rajoitekielelle, jolloin voidaan käyttää ilmaisuvoimaisempaa rajoitekieltä tai suunnitella algoritmi, jossa päättelyjärjestelmää kutsutaan iteratiivisesti.

Päättelyjärjestelmiä hyödyntämällä voidaan tehokkaasti tuottaa eksakteja sekä verifioitavia tuloksia useissa sovelluskohteissa. Tämän vuoksi automatisoitua päättelyä pidetään modernin tietojenkäsittelytieteen menestystarinana. Väitöskirjassa viedään automatisoidun päättelyn menetelmiä eteenpäin erityisesti laskennallisen argumentaation kontekstissa analysoimalla ongelmien laskennallista vaativuutta sekä suunnittelemalla deklaratiivisia algoritmeja. Kaikki väitöskirjassa esitetyt algoritmit on toteutettu avoimen lähdekoodin järjestelminä.

Andreas Niskasen väitöskirja on luettavissa: https://helda.helsinki.fi/handle/10138/319458

Teksti: Andreas Niskanen

Andreas Niskanen työskentelee tutkijatohtorina Helsingin yliopistolla Constraint Reasoning and Optimization -tutkimusryhmässä.