OpenAI kertoi tiistaina ratkaisseensa Navier-Stokes-yhtälöiden olemassaolo- ja sileysongelman. Kyseessä on yksi Clay-instituutin vuosituhannen ongelmista, joista kustakin on luvattu miljoonan dollarin palkinto. Todistuksen tuotti yhtiön sisäinen malli, jota ei ole julkaistu asiakkaille. Tulos on formalisoitu Lean-kielellä ja koneellisesti tarkistettu, joten sen oikeellisuutta ei tarvitse uskoa yhtiön sanaan.
Uutinen kertoo kahdesta asiasta yhtä aikaa. Kone ratkaisi tehtävän, jonka parissa matemaatikot ovat työskennelleet kahden vuosisadan ajan. Samana vuorokautena syntyi kuitenkin kiista siitä, kenelle ansio kuuluu ja miten OpenAI päätyi juuri tälle reitille.
Kymmenentuhatta agenttia ja 88 tuntia
OpenAI:n oman kuvauksen mukaan työ käynnistyi 1. syyskuuta. Yhtiö oli kuullut huhun, jonka mukaan kaksi vuosituhannen ongelmaa oli ratkennut jossain muualla. Se päätti ajaa tuoreen sisäisen mallinsa läpi kaikki avoimet Clay-ongelmat ja muutaman muun vaikean tehtävän. Kyse ei siis ollut pitkästä tutkimusohjelmasta vaan reaktiosta.
Liikkeelle lähti ensin noin sadan agentin ryhmä. Se tuotti runsaassa 50 tunnissa vastatodistuksen kolmiulotteisten Euler-yhtälöiden säännöllisyydelle. Vasta sen jälkeen yhtiö kohdisti varsinaiseen Navier-Stokes-ongelmaan noin 10 000 agenttia. Mittakaavan kasvattaminen oli tietoinen valinta, ei sattuma.
Agenttiparvi löysi singulariteetin 88 tunnissa laskennan aloittamisesta. Lean-formalisointi ja varmennus veivät vielä 17 tuntia, ja sen hoiti GPT-6 Astra. Agentit lähettivät toisilleen matkan varrella lähes viisi miljoonaa viestiä. Sébastien Bubeck, joka johtaa OpenAI:n matematiikkatiimiä, arvioi laskennan hinnaksi useita miljoonia dollareita.
Luvut ovat olennainen osa uutista. Todistus ei syntynyt yhdestä nerokkaasta kehotteesta vaan teollisesta ajosta, jossa raaka laskentateho korvasi vuosien miettimisen. Sama resepti on periaatteessa toistettavissa mihin tahansa riittävän tarkasti muotoiltuun ongelmaan.
Kiista ansioista kärjistyi saman vuorokauden aikana
Noin 12 tuntia ennen OpenAI:n ilmoitusta NYU:n matematiikan professori Tristan Buckmaster julkaisi omat tuloksensa. Ne syntyivät yhteistyössä Levent Alpögen kanssa, joka on Anthropicin työntekijä mutta teki työn omissa nimissään. Pari osoitti, että Euler-yhtälöt voivat räjähtää äärellisessä ajassa. Työkaluina he käyttivät sekä Claudea että OpenAI:n Codexia.
Buckmasterin mukaan tieto heidän edistymisestään kulkeutui OpenAI:lle ennen julkaisua. Hän kertoo kysyneensä, oliko yhtiö nähnyt hänen Codex-kehotteitaan, ja saaneensa kieltävän vastauksen. Kysymykseen siitä, oliko kehotteita käytetty mallin koulutuksessa, ei hänen mukaansa vastattu lainkaan. OpenAI pidättää oikeuden kouluttaa malleja Codex-istunnoilla, ellei käyttäjä erikseen kiellä sitä.
Buckmaster kertoo saaneensa myös ehdotuksen, jossa hän olisi julkaissut Navier-Stokes-tuloksen omissa nimissään ilman Alpögen mainintaa. Hän kieltäytyi ja vei asian julkisuuteen. TechCrunchin mukaan puhelinkeskustelun sävy kiristyi tämän jälkeen selvästi. Buckmaster korostaa julkilausumassaan, ettei hän syytä ketään mistään vaan kertoo, mitä hänelle sanottiin ja milloin.
OpenAI kiistää väitteet. Bubeckin mukaan yhtiön tutkijat tai agentit eivät nähneet parin työtä ennen sen julkistamista. Yhtiö tunnustaa Buckmasterin ja Alpögen ensisijaisuuden Euler-tuloksessa ja onnittelee heitä. Sen mukaan oma todistus on luonteeltaan olennaisesti eri asia.
Ratkesiko Clay-ongelma vai porsaanreikä
Todistus nojaa yhtälöiden pakotustermiin, jonka useimmat tutkijat jättävät kokonaan pois. Clayn virallinen muotoilu kuitenkin sallii sen, ja juuri siihen molemmat tiimit tarttuivat. Menetelmän kehittivät espanjalaiset matemaatikot Diego Córdoba ja Luis Martínez-Zoroa, jotka huomasivat sivuutetussa termissä hyökkäyspinnan. Ilman heidän työtään kumpikaan tulos ei olisi syntynyt.
Charles Fefferman, joka aikanaan kirjoitti Clayn viralliset ongelmanmuotoilut, pitää Córdobaa ja Martínez-Zoroaa tarinan varsinaisina sankareina. Buckmaster on mennyt pidemmälle ja esittänyt Martínez-Zoroalle Fields-mitalia. Näkemys on huomionarvoinen, koska se siirtää painopisteen laskentateholta ideaan.
Osa matemaatikoista katsoo, että ongelma ratkesi teknisen aukon kautta. Pakotustermi on menetelmälle niin keskeinen, ettei todistusta ilmeisesti voi yleistää ilman sitä. Monet asiantuntijat ovat vuosikymmeniä ajatelleet ongelmaa nimenomaan ilman kyseistä termiä. Clay-instituutti joutuu nyt ottamaan kantaa siihen, täyttääkö tulos palkinnon ehdot.
OpenAI on itse ilmoittanut, ettei se hae palkintoa. Yhtiön mukaan julkaisun tarkoitus on raportoida mallien edistymisestä, ei kerätä miljoonaa dollaria. Quanta Magazinen mukaan Lean-varmennus tekee itse todistuksesta kiistattoman riippumatta siitä, miten Clay lopulta linjaa.
Yhteenveto
Navier-Stokes on ensimmäinen vuosituhannen ongelma, jonka ratkaisusta valtaosan teki kone. Todistus on tarkistettu formaalisti, ja sen oikeellisuus on kenen tahansa todennettavissa. Tästä ei kiistele kukaan.
Kiista koskee kaikkea muuta: kuka sai idean, kenen työ kulkeutui kenelle ja mitä käyttäjien omista lokeista päätyi koulutusaineistoon. Nämä kysymykset eivät ratkea Leanilla. Ne toistuvat todennäköisesti aina, kun seuraava malli osuu tutkimuskysymykseen, jonka parissa ihmiset ovat jo pitkällä.