DeepMindin yhdeksän todistusta uutuustestissä

Matemaattinen todistus voi näyttää elegantilta ja silti sisältää aukon, joka jää vuosiksi huomaamatta. Google DeepMindin tekoälyagentti AlphaProof Nexus laati todistukset yhdeksään Paul Erdősin esittämään ongelmaan, ja ohjelmisto tarkisti jokaisen päättelyaskeleen. Tutkimus ilmestyi ensin toukokuussa esijulkaisuna (arXiv) ja vertaisarvioinnin jälkeen Science-lehdessä 8. lokakuuta (Science). Ohjelmisto pystyi varmistamaan päättelyn oikeellisuuden. Sen arvioiminen, sisälsikö tulos jotakin uutta, jäi matemaatikoille.

Todistuksen tarkistaja ei vaikutu tyylistä

Kielimallit osaavat tuottaa uskottavan kuuloista matematiikkaa. Varmalta kuulostava teksti voi peittää puuttuvan perustelun, jonka huomaa vain huolellinen lukija. AlphaProof Nexus välttää tämän ongelman käyttämällä Lean-ohjelmointikieltä. Siinä määritelmät, väitteet ja todistukset kirjoitetaan niin täsmällisesti, että tietokone voi tarkistaa ne.

Lean toimii kuin tarkastaja, joka käy valmiin todistuksen läpi rivi riviltä ja soveltaa samoja sääntöjä joka kerta. Tyyli ei vaikuta arvioon. Jos yksikin päättelyaskel ei seuraa edellisistä, todistus hylätään, vaikka muu teksti olisi kuinka sujuvaa.

Tutkimusryhmän mukaan agentti etsi Leanillä kirjoitettuja todistuksia. Tutkijat antoivat sille myös käyttöön AlphaProofin, DeepMindin aiemman, nimenomaan todistamiseen kehitetyn järjestelmän. Kokeissa samaan tulokseen päästiin yksinkertaisemmalla kokoonpanolla: kielimalli ja Lean tuottivat todistukset kaikkiin yhdeksään Erdős-ongelmaan ilman AlphaProofia (The Decoder). Näissä ongelmissa erikoistunutta järjestelmää ei siis tarvittu.

Tutkimuksessa raportoidaan hyväksytyt todistukset yhdeksälle Erdősin väitteelle ja 44:lle Online Encyclopedia of Integer Sequences -tietokannan otaksumalle. Otaksuma on väite, jota pidetään totena mutta jota ei ole todistettu; tietokanta puolestaan kokoaa lukujonoja (Science). Erdős-tulosten joukossa on kokonaislukuja koskeva kaksiosainen ongelma, jonka Erdős ja András Sárközy esittivät vuonna 1970. Se pysyi ratkaisematta yli puoli vuosisataa (ABC).

Mitä tarkistaja ei näe

Lean varmistaa, että todistus osoittaa täsmälleen sen väitteen, joka on kirjoitettu koodiin. Se ei vastaa kolmeen muuhun kysymykseen: vastaako koodi sitä, mitä Erdős tarkoitti, oliko joku ratkaissut ongelman jo aiemmin ja tuoko ratkaisu matematiikkaan jotakin uutta.

Vuoden 1970 ongelma näyttää, miksi kaksi viimeistä kysymystä ovat tärkeitä. Ongelman toinen osa seuraa ensimmäisestä, joten yksi todistus ratkaisee molemmat. Kun agentin todistukset tulivat julki, kävi ilmi, että alkuperäisen vuoden 1970 artikkelin rakennelmaa hieman muokkaamalla saadaan vastaus kumpaankin osaan (arXiv). Agentin todistukset olivat oikein. Ongelma oli vain ollut lähempänä ratkaisua kuin sen avoimeksi luokittelu antoi ymmärtää.

Tällaisen asian huomaaminen vaatii alan tuntemusta. Tanskan Aarhusin yliopiston matemaatikko Gergely Bérczi, yksi tutkimuksen kirjoittajista, auttoi sopivien ongelmien valinnassa ja ratkaisujen arvioinnissa (Aarhus University). Hän osallistui myös sellaisten todistusversioiden kirjoittamiseen, joita ihmisen on helpompi seurata. Lean varmisti jokaisen päättelyaskeleen, kun taas Bérczi kollegoineen arvioi, mitä todistukset kokonaisuutena toivat.

Työnjako erottaa tutkimuksen viime kuussa esitellystä saavutuksesta. Silloin Anthropicin Claude muunsi Fermat’n suuren lauseen jo tunnetun todistuksen Lean-muotoon (To Brief). Tunnetun todistuksen muuntaminen ei herätä epäilyksiä uutuudesta. Avoimina pidettyjen väitteiden etsiminen herättää, joten uutuuden arviointi nousee keskeiseksi.

Tutkimusryhmä on julkaissut todistustiedostot, jotta muutkin voivat tarkistaa ne samalla ohjelmistolla (GitHub). Tutkimuksen osoittama edistysaskel on rajattu: tekoälyagentti tuotti koneellisesti tarkistettavat todistukset joillekin väitteille, joita matemaatikot olivat pitäneet avoimina. Tarkistus takaa, että todistukset pätevät Leanissä kirjoitettuihin väitteisiin. Sen arvioiminen, mitä kukin todistus lisäsi matematiikkaan, jäi niitä lukeneille matemaatikoille.