Viisi ihmistä sadassa vuodessa
Yhdysvaltalainen Axiom ilmoitti maaliskuun alussa, että sen AxiomProver-järjestelmä sai täydelliset 120 pistettä vuoden 2025 Putnam-kokeesta. Putnam on Pohjois-Amerikan arvostetuin yliopistotason matematiikkakilpailu, ja kokeen lähes sadan vuoden historiassa vain viisi ihmistä on yltänyt täysiin pisteisiin.
Kokeen vaikeus on legendaarinen. Vuosittain noin 4 000 matematiikan opiskelijaa yrittää ratkaista 12 tehtävää, jotka vaativat luovaa ongelmanratkaisua lukuteoriasta ryhmäteoriaan. Mediaanipisteet ovat tyypillisesti nolla tai yksi 120:stä. Vuoden 2024 kilpailussa keskiarvo oli kahdeksan pistettä, ja vain prosentti osallistujista ylsi yli puoleen pisteistä.
Vuonna 2025 paras ihmistulos oli 110 pistettä. Axiomin tekoäly päihitti senkin ja ratkaisi kaikki 12 tehtävää virheettömästi.
Todistaminen, ei arvaaminen
Axiomin teknologia eroaa perinteisistä kielimalleista yhdellä ratkaisevalla tavalla: se ei arvaa. Tavallinen kielimalli tuottaa tilastollisesti todennäköisimmän vastauksen, joka voi näyttää oikealta mutta olla täysin väärä. Axiom käyttää Lean-ohjelmointikieltä, joka on suunniteltu matemaattisten todistusten koneelliseen tarkistamiseen.
Jokainen päättelyvaihe on Leanissa formaalisti verifioitavissa. Järjestelmä ei voi tuottaa virheellistä tulosta huomaamatta, koska todistuksen jokainen askel tarkistetaan automaattisesti. Tämä poistaa hallusinaatio-ongelman, joka on suurin yksittäinen este tekoälyn käyttöönotolle kriittisillä aloilla.
Axiomin lähestymistapa luo myös itseään vahvistavan kehän. Kun järjestelmä tuottaa verifioitua dataa, sitä voidaan käyttää mallin jatkokouluttamiseen ilman riskiä siitä, että koulutusdata sisältää virheitä. Perinteisissä kielimalleissa tekoälyn tuottaman datan syöttäminen takaisin koulutukseen johtaa laadun heikkenemiseen.
Erottelu on merkittävä erityisesti ohjelmistokehityksessä. Kun tekoäly tuottaa yhä suuremman osan maailman koodista, kasvaa tarve varmistaa, että koodi tekee sen mitä sen pitää. Axiom tarjoaa matemaattisen takuun: koodi on oikein eikä se sisällä tietoturva-aukkoja.
“Kielimallit ovat luonteeltaan tilastollisia – ne tuottavat uskottavia tuloksia, eivät todistettavasti oikeita tai turvallisia.”
25-vuotias perustaja ja matemaatikko, joka luopui virasta
Axiomin perusti Carina Hong, 25-vuotias MIT:stä valmistunut matemaatikko, joka keskeytti Stanfordin jatko-opintonsa yrityksen takia. Hong on Morgan-palkinnon voittaja ja yhdeksän vertaisarvioidun julkaisun kirjoittaja.
Yhtiön perustajajäsen Ken Ono on yksi maailman tunnetuimmista lukuteoreetikoista ja Ramanujanin matematiikan asiantuntija. Hän jätti vakituisen professorin virkansa ja varaprovostin tehtävän Virginian yliopistossa liittyäkseen Axiomiin kokopäiväisesti. Tekniikkajohtajana toimii Shubho Sengupta, joka johti aiemmin Metan tekoälytutkimusyksikön infrastruktuuria kahdeksan vuoden ajan.
Tiimin osaaminen näkyy tuloksissa. Putnam-kokeen lisäksi Axiomin tekoäly ratkaisi formaalisti 20 vuotta avoinna olleen lukuteoreettisen konjektuurin, johon Ono itse ei ollut koskaan pystynyt. Järjestelmä tuotti todistuksen Lean-kielellä täysin itsenäisesti, ilman ihmisen ohjausta.
