Voimmeko luottaa tietokoneen olevan oikeassa?
Tiesitkö, että käytät todennäköisesti jatkuvasti tietokonetta optimointiongelmien ratkaisemiseen? Näin teet esimerkiksi tarkistaessasi nopeinta reittiä keskustaan puhelimellasi. Mutta voitko luottaa siihen, että ehdotus on paras mahdollinen? Tämä artikkeli kuvaa tutkimusprosessia, jossa kehitettiin tulostensa laadun todistava algoritmi.
Johdanto
Onko suoratoistopalvelu joskus suositellut sinulle kiinnostavaa elokuvaa? Entä oletko tarkastanut nopeimman reitin keskustaan puhelimellasi? Silloin olet käyttänyt tietokonetta optimointiongelman ratkaisemiseen. Optimointiongelmia esiintyy monella alalla. Kyky ratkaista optimointiongelmia tehokkaasti voi monessa tilanteessa säästää aikaa, rahaa tai muita resursseja, mikä motivoi tutkijoita kehittämään tehokkaita optimointialgoritmeja. Suurin haaste optimointialgoritmien tutkimuksessa on se, että suurin osa meitä kiinnostavista optimointiongelmista on todella vaikeasti ratkaistavia. Kaikkien mahdollisuuksien tarkastamiseen menisi miltä tahansa tietokoneelta miljoonia vuosia. Suurin osa käytännön sovelluksissa käytettävistä optimointialgoritmeista koostuukin lukuisista monimutkaisista osista.
Tutkimuksessamme meitä motivoivat käytännön optimointialgoritmien monimutkaisuus ja niiden antamien tulosten mahdolliset merkittävät vaikutukset yksilöiden elämään. Moni yritys käyttää optimointialgoritmeja valitessaan palkattavat työntekijät työnhakijoiden joukosta. Myös monet pankit käyttävät optimointialgoritmeja päättäessään, kenelle myönnetään asuntolaina. Yhdysvalloissa optimointialgoritmeja käytetään valitsemaan, ketkä vangeista pääsevät ehdonalaiseen vapauteen1, ja monissa maissa (ml. Pohjoismaat) niillä etsitään sopivia pareja elinluovutuksille2.
Työmme tärkein tutkimuskysymys on: Kuinka voimme varmistaa, että optimointiongelmia ratkova tietokoneohjelma oikeasti löytää parhaan mahdollisen ratkaisun? Tietokoneisiin epäröimättä luottaminen voi tuntua houkuttelevalta. On kuitenkin tärkeää sisäistää, että jokainen optimointialgoritmista kehitetty tietokoneohjelma on ihmisen toteuttama, eli implementoima. Vaikka algoritmi itsessään olisi todistettu oikein toimivaksi, eli aina parhaan mahdollisen ratkaisun antavaksi, voi sen monimutkainen rakenne johtaa käytännön toteutuksessa virheisiin, joiden seurauksena ohjelmassa on bugeja eli toimintavirheitä. Nämä bugit voivat esimerkiksi saada tietokoneohjelman väittämään, että työnhakijaa ei kannata palkata, vaikka hän oikeasti olisikin täydellinen työhön. Useimmissa tapauksissa tällaiset bugit ovat vaikeita, jopa mahdottomia, havaita jälkikäteen. Erityisen haastavaa niiden havaitseminen on käyttäjälle, joka ei tunne optimointialgoritmeja ja niiden toimintaa.
Tutkimuksessa on kehitetty kolme pääasiallista menetelmää optimointiongelmia ratkaisevien tietokoneohjelmien luotettavuuden parantamiseksi. Ensimmäinen niistä on testaaminen. Jos tiedämme jonkun henkilön olevan hyvä ehdokas työhön, voimme kokeilla mitä ohjelmamme sanoo tämän henkilön tiedoista. Jos ohjelmakin pitää ehdokasta työhön sopivana, voimme olla hieman varmempia siitä, että ohjelma on implementoitu oikein. Emme kuitenkaan voi koskaan olla täysin varmoja; vaikka ohjelma antaa oikean vastauksen henkilöstä A, ei se välttämättä vastaa oikein henkilön B kohdalla. Toinen menetelmä on formaali verifiointi, jossa todistetaan matemaattisesti, ettei ohjelma sisällä bugeja. Tämä menetelmä on erittäin tehokas, mutta valitettavasti käytettävissä ainoastaan hyvin yksinkertaisiin ohjelmiin. Tutkijat eivät toistaiseksi tiedä, miten formaalia verifiointia voitaisiin käyttää optimointiongelmia tosielämässä ratkaiseviin, monimutkaisiin tietokoneohjelmiin.
Kolmas menetelmä optimointiongelmia ratkaisevien tietokoneohjelmien luotettavuuden parantamiseksi on laajentaa ohjelman käyttämää algoritmia. Tähän menetelmään keskityimme tutkimuksessamme. Algoritmia laajennetaan niin, että se tuottaa tuloksen lisäksi myös matemaattisen todistuksen antamansa tuloksen parhaudesta. Tämä todistus voidaan tarkistaa erillisellä verifiointialgoritmilla, joka on rakenteeltaan tarpeeksi yksinkertainen formaalia verifiointia varten. On huomioitava, että tämä menetelmä ei todista, etteikö ohjelmassa silti voisi olla bugeja. Vaikka todistus jonkun ehdokkaan sopivuudesta olisi oikein, voi algoritmi toimia väärin muiden ehdokkaiden kohdalla. Ideana on, että jos optimointialgoritmi toimiii väärin on myös todistus virheellinen. Yksinkertainen verifiointialgoritmi puolestaan huomaa tämän virheellisen todistuksen.
Miten tutkimus tehtiin?
Työssämme laajensimme jo olemassa olevaa optimointialgoritmia kyvyllä tuottaa todistuksia laskelmilleen. Työmme koostui sekä teoriasta että käytännöstä. Ensin meidän piti keksiä, miten algoritmia voisi teoriassa laajentaa todistuksilla. Tämä osio muistutti matematiikan tehtävien ratkaisemista koulussa, sillä erolla, ettemme voineet tarkistaa ratkaisuja mistään. Keskustelimme ryhmässä, kunnes keksimme yhdessä mahdollisen tavan.
Teoriaosuuden jälkeen aloitimme käytännön työn. Implementoimme todistuksia tuottavan algoritmimme ja testasimme, kuinka paljon todistusten tuottaminen hidasti ohjelmaa. Todistuksia tuottava algoritmi on hitaampi kuin todistuksia tuottamaton, joutuuhan se tekemään enemmän työtä. Tällä hetkellä ei ole olemassa teoriaa, joka kertoisi, kuinka paljon hitaampi todistuksia tuottava algoritmi on. Meidän täytyi yksinkertaisesti testata kokeellisesti. Käytimme ohjelmaamme erilaisten optimointiongelmien ratkaisemiseksi ja mittasimme, kuinka paljon todistusten tuottaminen hidasti suoritusta. Testasimme myös, kuinka pitkään verifiointialgoritmilla kestää tuottamiemme todistusten tarkistamisessa.
Mitä tutkimuksessa löydettiin?
Onnistuimme kehittämään teorian, jota tarvitaan olemassa olevan optimointialgoritmin laajentamiseksi todistuksia tuottavaksi. Uuden todistustuotantomme avulla onnistuimme myös löytämään ja korjaamaan bugin eräässä algoritmin ennestään olemassa olevassa, monin paikoin käytetyssä ohjelmassa.
Kokeemme osoittavat, että optimointialgoritmin laajentaminen todistuksen tuottavaksi hidastaa algoritmia keskimäärin 8,5 prosenttia. Jos optimointiongelman ratkaisemiseen ilman todistusta kuluu 100 sekuntia, voimme tuottaa ratkaisun sekä todistuksen sen oikeellisuudesta 108 sekunnissa. Todistusten tarkastaminen kesti keskimäärin kolme kertaa pidempään kuin niiden tuottaminen. Jos ohjelmalla kestää 108 sekuntia tuottaa todistus, kestää sen tarkastaminen 324 sekuntia. On tärkeä huomioida, että todistusten tuottaminen on tarkoitettu ainoastaan sellaisiin optimointiongelmiin, joiden ratkaisuilla on merkittäviä seurauksia. Suoratoistopalvelu, joka haluaa nopeasti luoda elokuvaehdotuksia käyttäjälleen, ei voi odottaa kolminkertaista aikaa saadakseen todistuksia siitä, että suositukset ovat parhaita mahdollisia. Työnantajan voi toisaalta olla kannattavaa odottaa kolminkertainen aika saadakseen varmuus siitä, että palkattava henkilö on hakijoista paras – uudelleenrekrytointi myöhemmin tulisi nimittäin paljon kalliimmaksi.
Lopuksi
Tietokoneita ja muita älylaitteita käytetään nykyään yhä useampiin eri käyttötarkoituksiin. Usein on helppo kyseenalaistamatta uskoa niiden tuottamien tulosten olevan oikein, vaikka nykyaikaisten tietokonejärjestelmien käyttämät algoritmit ovat erittäin monimutkaisia ja niiden implementoinnissa voi tulla virheitä. Artikkelissamme tutkimme optimointialgoritmeja, jotka osaavat tuottaa sekä ratkaisun että todistuksen ratkaisulle. Tutkimuksemme vaati sekä teoreettista että käytännöllistä tutkimusta. Alkuun meidän oli keksittävä, miten optimointialgoritmeja ylipäätään voidaan laajentaa tuottamaan todistuksia. Tämän jälkeen tutkimme todistustuotannon vaikutusta tietokoneohjelman tehokkuuteen. Vaikka tutkimuksemme ei vielä johtanut yleiseen käyttöön sopivan järjestelmän syntyyn, on tärkeä huomata meidän mallimme olevan yksi ensimmäisistä keinoista saada optimointialgoritmi tuottamaan todistuksia – edes teoriassa. Siksi toivommekin, että esittelemiämme tekniikoita kehitettäisiin edelleen, jotta niistä tulisi nopeampia ja toivon mukaan tulevaisuudessa yhä yleisemmin käytettyjä.