Anthropicin matemaatikko Levent Alpöge julkaisi 19. heinäkuuta lyhyen viestin X:ssä. Hän oli löytänyt vastaesimerkin Jacobin otaksumaan, yhteen algebrallisen geometrian tunnetuimmista avoimista ongelmista. Löytö syntyi yhtiön Claude Fable 5 -mallin avulla, joka julkaistiin yleiseen käyttöön vain muutamaa viikkoa aiemmin.
Vastaesimerkki kaataa otaksuman, jota matemaatikot olivat yrittäneet ratkaista vuodesta 1939. The Conversationin mukaan tulos poikkeaa aiemmista tekoälyn matemaattisista läpimurroista, koska se kumoaa pitkään uskotun väitteen sen sijaan että todistaisi sen. Stanfordin yliopiston matemaatikko vahvisti tuloksen alle vuorokaudessa.
Mistä Jacobin otaksumassa on kyse
Otaksuma koskee funktioita, jotka rakentuvat polynomeista. Funktio ottaa sisään lukuja ja tuottaa niistä uusia lukuja tietyn säännön mukaan. Kun luvut tulkitaan avaruuden pisteiksi, funktio siirtää pisteitä paikasta toiseen.
Funktion käyttäytymistä mitataan niin sanotulla Jacobin determinantilla. Jos determinantti on nollasta poikkeava vakio, funktio ei taita eikä litistä avaruutta minkään pisteen ympärillä. Otaksuma väittää, että tällaisella funktiolla on aina käänteisfunktio, joka palauttaa pisteet alkuperäisille paikoilleen.
Kaikki funktiot eivät ole käännettävissä. Jos funktio siirtää kaksi pistettä samaan kohtaan, niitä ei voi enää erottaa toisistaan eikä palauttaa oikeille paikoilleen. Juuri tästä syystä determinantin ehto on niin keskeinen.
Väite kuulostaa yksinkertaiselta, mutta sen todistaminen tai kumoaminen on osoittautunut poikkeuksellisen vaikeaksi. Kaksiulotteisen version esitti tšekkiläinen matemaatikko jo 1800-luvulla, ja saksalainen Ott-Heinrich Keller yleisti sen mihin tahansa ulottuvuuteen vuonna 1939. Fields-mitalisti Stephen Smale otti ongelman vuoden 1998 listalleen tulevan vuosisadan matemaattisista haasteista.
Näin vastaesimerkki löytyi
Alpöge käytti Claude Fable 5:tä työkaluna tutkiakseen matemaattisia rakenteita, joita ihmiset olivat etsineet lähes yhdeksän vuosikymmentä tuloksetta. Lopputulos on hämmästyttävän pieni: vain 216 merkin mittainen polynomikuvaus kolmessa muuttujassa.
Alpöge kertoi löytäneensä tuloksen jalkapallon MM-finaalin aikaan ja julkaisi sen mutkattomasti sosiaalisessa mediassa. Viesti oli tyyliltään arkinen, mutta sen sisältö ravisteli matematiikan yhteisöä välittömästi.
Kyse ei ollut sattumasta. Malli ohjattiin etsimään juuri niitä rakenteita, joissa vastaesimerkin pitäisi teoriassa piillä. Vastaesimerkki oli aina ollut olemassa, mutta se oli piilossa alueella, jota ihmismatemaatikot olivat tutkineet perusteellisesti onnistumatta.
Miksi tulos on merkittävä
Tuloksen painoarvoa lisää sen nopea ja riippumaton varmistus. Stanfordin yliopiston Jared Duker Lichtman tarkisti vastaesimerkin noin vuorokaudessa sekä käsin että Lean-todistusavustimella. Lean varmentaa matemaattiset todistukset koneellisella tarkkuudella, mikä poistaa inhimillisen virheen mahdollisuuden.
Varmistus on olennaista, sillä Jacobin otaksuman historia on täynnä virheellisiä todistuksia. Jopa tunnetut 1900-luvun matemaatikot esittivät ratkaisuja, joista löytyi myöhemmin hienovaraisia virheitä. Koneellinen tarkistus erottaa tämän tuloksen aiemmista yrityksistä.
Löytö liittyy laajempaan ilmiöön. Viime kuukausina kielimallit ovat olleet mukana useissa merkittävissä matemaattisissa läpimurroissa, kuten OpenAI:n yksikköetäisyysotaksuman kumoamisessa. Tekoäly ei korvaa matemaatikkoa vaan toimii työkaluna, joka laajentaa tutkittavan ongelma-avaruuden rajoja.
Yhteenveto
Jacobin otaksuman kaatuminen osoittaa, että kielimallit voivat tuottaa aitoja matemaattisia tuloksia korkeimmalla tasolla. Ratkaiseva ei ollut pelkkä laskentateho vaan mallin kyky navigoida abstrakteissa rakenteissa ihmisen ohjauksessa.
Samalla tapaus muistuttaa varmistuksen merkityksestä. Koneellinen todistustarkistus antoi yhteisölle luottamuksen tulokseen alle vuorokaudessa. Yhdistelmä tekoälyavusteista löytämistä ja formaalia varmennusta voi nopeuttaa matematiikan edistystä tavalla, joka olisi ollut mahdoton vielä muutama vuosi sitten.