Tekoäly ratkaisi 56 vuotta auki olleen pulman

Google DeepMind kertoi, että sen AlphaProof Nexus -niminen tekoälyjärjestelmä on ratkaissut yhdeksän avointa matematiikan ongelmaa unkarilaisen Paul Erdősin kuuluisasta kokoelmasta. Kaksi ongelmista oli esitetty vuonna 1970 ja odottanut vastausta 56 vuotta. Uutinen tulee Tanskan Aarhusin yliopistosta, jonka tutkija työskenteli järjestelmän kanssa.

Mikä AlphaProof Nexus on

AlphaProof Nexus on ohjelma, joka kirjoittaa matemaattisia todistuksia Lean-nimisellä kielellä. Lean ei ole tavallinen ohjelmointikieli vaan niin sanottu todistusassistentti: jokainen looginen askel pitää kirjoittaa niin täsmällisesti, että tietokone pystyy tarkistamaan sen oikeellisuuden.

Ero perinteiseen matematiikkaan on juuri tässä. Kun matemaatikko julkaisee todistuksen paperilla, muut alan asiantuntijat lukevat sen läpi ja etsivät virheitä. Työ voi kestää kuukausia, ja virheitä livahtaa silti ohi. Lean-todistuksessa kone käy jokaisen päättelyaskeleen kohta kohdalta ja hylkää työn, jos yksikin kohta ei pidä. Jos todistus menee läpi, se on varmasti pätevä.

Tässä on tekoälylle luontainen etu. Malli voi tuottaa suuren määrän ehdotuksia, ja Lean toimii armottomana tuomarina, joka päästää läpi vain aukottomat. Yhden ongelman ratkaiseminen maksoi DeepMindin mukaan muutamia satoja dollareita laskenta-aikaa.

Yhdeksän ongelmaa ja 44 konjektuuria

Luvut kannattaa erottaa toisistaan. Erdősin kokoelmasta oli muunnettu Lean-muotoon 353 avointa ongelmaa, ja näistä AlphaProof Nexus ratkaisi yhdeksän. Erdős, joka kuoli vuonna 1996, jätti jälkeensä satoja pulmia, joista osa on edelleen auki ja jotkut jopa palkintorahan arvoisia.

Tämän lisäksi järjestelmä todisti 44 avointa konjektuuria, jotka olivat peräisin kokonaislukujonojen tietokannasta OEIS:stä. Konjektuuri tarkoittaa arvausta, jonka moni uskoo todeksi mutta jota kukaan ei ole ehtinyt todistaa. Ratkaistut Erdős-ongelmat ja todistetut konjektuurit ovat siis kaksi eri saavutusta, ei sama asia laskettuna kahteen kertaan.

Miksi 56 vuotta merkitsee

Matematiikassa ongelman ikä kertoo sen vaikeudesta. Jos kysymys on ollut auki puoli vuosisataa, sitä ovat yrittäneet ratkaista lukuisat huippumatemaatikot ilman tulosta. Kaksi vuonna 1970 esitettyä Erdős-ongelmaa kuuluvat juuri tähän joukkoon.

Ratkaisu ei tarkoita, että kone olisi ollut ihmisiä älykkäämpi. Se tarkoittaa, että oikeanlainen todistus löytyi järjestelmällisen haun ja koneellisen tarkistuksen yhdistelmällä. Ihmiselle sama työ olisi ollut hidasta ja virhealtista.

Pohjoismainen kytkös

Uutisen pohjoismainen kärki löytyy Tanskasta. Aarhusin yliopiston matematiikan apulaisprofessori Gergely Bérczi oli ensimmäinen tutkijamatemaatikko, joka työskenteli järjestelmän kanssa. Hän valitsi sopivia ongelmia, tarkisti koneen tuottamat ratkaisut ja kirjoitti niistä ihmisen luettavat versiot.

Bérczi on testannut myös DeepMindin toista järjestelmää nimeltä Co-Mathematician ja ollut mukana kehittämässä ProofCouncil-työkalua, joka ratkaisi riippumattomassa vertailussa kuusi kymmenestä ongelmasta. Tutkijan rooli kertoo, ettei kone toimi yksin: joku päättää, mitä sen kannattaa yrittää, ja varmistaa lopputuloksen.

Tavalliselle lukijalle uutinen ei näy huomenna missään. Pidemmällä aikavälillä koneellinen todistuksen tarkistus voi kuitenkin muuttaa sitä, kuinka luotettavaa ohjelmistoa rakennetaan. Samaa Lean-tekniikkaa käytetään jo nyt varmistamaan, että esimerkiksi lentokoneiden ja sirujen ohjelmakoodi toimii täsmälleen kuten pitää. Jos tekoäly oppii tuottamaan aukottomia todistuksia halvalla, hyöty valuu lopulta arkisiin järjestelmiin, joiden pitää yksinkertaisesti toimia oikein.

Matemaatikolle tämä tarkoittaa työkalua, ei kilpailijaa. Kone hoitaa raskaan varmistustyön, ihminen keskittyy siihen mitä kone ei osaa: kysymään, mikä ongelma ylipäätään kannattaa ratkaista.