56 vuotta auki ollut matematiikkapulma ratkesi parilla satasella

Google DeepMindin AlphaProof Nexus on selvittänyt yhdeksän aiemmin avointa Erdősin ongelmaa, joista kaksi on ollut auki 56 vuotta. Järjestelmä yhdistää kielimallin Lean-todistuskoneeseen ja tarkistaa jokaisen päättelyaskeleen koneellisesti. Yksittäisen pulman ratkaisu maksoi muutaman sadan dollarin laskenta-ajan. Tutkimusryhmä julkaisi tulokset arXivissa 21. toukokuuta.

Yhdeksän 353 avoimesta pulmasta

Unkarilainen Paul Erdős (1913–1996) jätti jälkeensä satoja matemaattisia ongelmia, joita hän ei ennättänyt itse ratkaista. Erdős-projektiin on koottu 353 niistä, ja niiden parissa matemaatikot ovat usein viettäneet vuosikymmeniä. AlphaProof Nexus kävi pinon läpi ja palautti yhdeksän formaalisti todistettua ratkaisua. Samalla järjestelmä todisti 44 avointa konjektuuria OEIS-tietokannasta, johon kerätään kokonaislukujonojen avoimia ominaisuuksia.

Paperi nimeää muun muassa ongelman 12(i), joka esitettiin vuonna 1970. Se koski äärettömän joukon rakentamista tietyillä jakautuvuus- ja tiheysominaisuuksilla, ja AlphaProof Nexus käytti kiinalaista jäännöslausetta ratkaisussa. Toinen mainittu pulma, ongelma 125 vuodelta 1996, käsitteli kokonaislukujen summajoukkoja kantajärjestelmien 3 ja 4 numeroesityksissä. Sen todistus nojaa kahden kantaluvun diofantosläheisyyteen.

Lean estää hallusinaatiot

Aiemmat tekoälyt ovat tuottaneet vakuuttavalta näyttäviä matemaattisia todistuksia, jotka eivät ole pitäneet tarkemmassa tarkastelussa. AlphaProof Nexus välttää ongelman rakenteellaan: sen tuotos ei ole vapaata tekstiä vaan Lean-todistuskoneen ymmärtämää formaalia koodia. Lean tarkistaa jokaisen päättelyaskeleen mekaanisesti. Jos jokin kohta ei pidä, kone hylkää todistuksen ja syöttää virheilmoituksen takaisin kielimallille, joka yrittää uudelleen.

Ero on ratkaiseva. Luonnollisella kielellä kirjoitettu todistus vaatii aina asiantuntija-arvioijan, ja prosessi voi kestää kuukausia tai vuosia. Andrew Wilesin Fermat'n suuren lauseen todistus oli vertaisarvioinnissa lähes vuoden, ennen kuin se hyväksyttiin. Lean-koodi joko menee läpi tai ei mene, ja päätös syntyy sekunneissa.

Päivä OpenAI:n jälkeen

Vain päivää aiemmin OpenAI oli ilmoittanut, että GPT-5 olisi ratkaissut yhden Erdősin ongelman. DeepMindin toimitusjohtaja Demis Hassabis huomautti pian, että malli oli löytänyt verkosta viittauksia jo aiemmin ratkaistuun tulokseen, ei todistanut mitään uutta. Googlen vastaus tuli alle vuorokaudessa: kahdeksan uutta todistusta päälle, ja jokainen niistä formaalisti verifioitu.

Tutkimuksen kiinnostava sivulöydös on, että järjestelmän yksinkertaisin variantti, paperissa nimeltä Agent A, onnistui yksinään kaikissa yhdeksässä ratkaisussa. Monimutkaisemmat populaatiopohjaiset variantit eivät tuoneet lisäratkaisuja, vaan ainoastaan laskivat per ratkaisu menevää kustannusta. Tämä viittaa siihen, että pohjalla olevan kielimallin parantuminen ja Lean-kääntäjän palautekierros tekevät varsinaisen työn.

Satasia per pulma muuttaa laskelman

Per pulma -kustannus jäi muutamaan sataan dollariin. Ennen vuotta 2024 vastaavan tason koneellinen todistus vaati erikoistuneen tutkimusryhmän kuukausien työn ja merkittävää rahoitusta. Kustannuksen lasku tarkoittaa, että pienemmilläkin yliopistoilla ja yksittäisillä tutkijoilla on varaa kokeilla järjestelmää omiin avoimiin pulmiinsa.

Sovelluskohteita ovat tutkijoiden mukaan kombinatoriikka, optimointi, graafiteoria, algebrallinen geometria ja kvanttioptiikka. DeepMind on avannut GitHubiin sekä Lean-todistukset että työn proosa-version, jolloin muut matemaatikot voivat tarkistaa tulokset itse.

Suomeen ulottuvat seuraukset

Suomalaiselle matematiikalle uutinen on kahtalainen. Ensiksi: formaali verifiointi nostaa tekoälyn tuottamien todistusten luotettavuutta tasolle, jolla niitä voidaan käyttää lähteinä jatkotutkimuksessa. Toiseksi: muutaman sadan dollarin per pulma -hinta tarkoittaa, että aiheeseen pääsee käsiksi ilman erikoisrahoitusta.

Suomessa Lean-yhteisöjä toimii sekä Aalto-yliopistossa että Helsingin yliopistossa, ja suomalaiset matemaatikot osallistuvat kansainväliseen mathlib-kirjaston rakentamiseen. Siinä olemassa olevia matematiikan teoreemoja käännetään käsin formaaliin muotoon. Pyysin keskiviikkona molemmilta yliopistolta kommenttia AlphaProof Nexuksen merkityksestä Suomen formaalille matematiikalle, ja päivitän juttua heti kun vastaukset saapuvat.

Tavalliselle lukijalle uutinen kertoo, että tekoäly on siirtynyt avustavasta roolista varsinaisen tutkimuksen tekijäksi vähintään matematiikan kentällä. Akateeminen julkaisukäytäntö joutuu pohtimaan uudelleen, kuka saa tekijyyden todistukseen, jonka on löytänyt kone ja verifioinut toinen kone. Lukuteorian kentällä keskustelu on alkanut vasta nyt, mutta seuraavien kuukausien aikana se ulottuu kaikkialle, missä formaaleja todistuksia on saavutettavissa.