Tungkol sa Problema ng Premyong Milenyo sa Navier–Stokes

Ibinabahagi namin ang isang solusyon sa problema ng pag-iral at pagkamakinis ng Navier–Stokes, isa sa mga Problema sa Premyong Milenyo. Ang patunay na ito, na ginawa ng isang panloob na sistema ng OpenAI, ay nagpapakita na ang dinamika ng mga ekwasyong Navier-Stokes para sa paggalaw ng likido ay maaaring magkaroon ng singularidad sa may hangganang oras. Ibinabahagi namin ang parehong nakasulat na paglalahad ng patunay at ang pormalisasyon nito sa Lean.

Ang Problema sa Premyong Milenyo⁠(magbubukas sa bagong window) ay kumakatawan sa ilan sa pinakamalalalim na tanong sa frontier ng matematika. Ang tanong kung maaaring pumalya ang makinis na tatlong-dimensyong paggalaw ng likido ay nananatiling hindi pa nalulutas sa loob ng humigit-kumulang 90 taon.

Ang isang pangunahing layunin ng aming trabaho ay bigyang-kakayahan ang mga siyentipiko na isulong ang pananaliksik at teknolohiyang pakikinabangan ng buong sangkatauhan. Para malutas ang problema ng Navier–Stokes, gumamit kami ng panloob na modelo na mas makabuluhang may kakayahan kaysa sa GPT‑6 Astra. Naniniwala kaming mahalagang ipaalam sa mundo ang bilis ng pag-unlad ng AI at kung ano ang aasahan mula sa mga susunod na modelo.

Ginagamit ng mga ekwasyong Navier–Stokes ang ikalawang batas ng paggalaw ni Newton (“F=ma”) para ilarawan kung paano gumagalaw ang mga likido. Mahalaga, itinuturing ng mga ito ang likido bilang isang tuloy-tuloy na medium sa halip na subaybayan ang mga indibidwal na molekula. Ginagamit ang mga ekwasyong ito sa disenyo ng sasakyang panghimpapawid, pagtataya ng panahon, at pag-aaral ng daloy ng dugo.

Isang pangunahing hindi pa nasasagot na tanong para sa mga ekwasyong ito ng dinamika ay kung maaaring masira ang aproksimasyon sa likido bilang continuum. Sa partikular, maaari bang magkaroon ng “singularidad” ang mga ekwasyon ng Navier–Stokes para sa isang tatlong-dimensiyonal na hindi napipigang likido na may pare-parehong densidad, kahit maayos na nagsisimula ang paggalaw? Dito, ang singularidad ay nangangahulugang humahantong ang dinamika sa mga bilis ng likido na tumataas nang walang hangganan sa loob ng limitadong panahon. Ang pagbuo ng isang singularidad ay kailangang maganap sa kabila ng presensya ng biskosidad, na may tendensiyang pakinisin ang paggalaw. Dahil ang isang tunay na likido ay hindi makakagalaw nang walang hanggang bilis, magpapahiwatig ito ng pagkasira sa paraan ng pagmomodelo ng mga ekwasyon sa likido. Para maipagpatuloy ang pagmomodelo sa sistema, kakailanganing subaybayan ang pag-uugali ng bawat partikulo nang paisa-isa.

Nagsimula ang mga ekwasyon noong ikalabinsyam na siglo sa gawa nina Claude-Louis Navier at George Gabriel Stokes. Noong 1934, pinatunayan ni Jean Leray na umiiral ang mga solusyon sa pangkalahatang diwa, ngunit kung palagi bang nananatiling makinis ang mga ito ay naging isang mahalagang tanong na hindi pa nasasagot. Noong 2000, itinuring ng Clay Mathematics Institute ang problema ng pag-iral at kakinisan ng Navier–Stokes bilang isa sa pitong Problema sa Premyong Milenyo.

Nakagawa ang aming sistema ng isang analitikal na patunay at isang pormalisasyon sa Lean na nagpapakitang ang isang likido na sa simula ay makinis at nakapahinga ay maaaring magkaroon ng singularidad sa loob ng panahong may hangganan. May makinis na puwersang inilapat sa likido, at nananatiling may hangganan ang enerhiya nito sa buong dinamika, mula sa pagkakapahinga hanggang sa pagbuo ng singularidad. Nalulutas nito ang problema sa Premyong Milenyo ng Navier–Stokes sa pamamagitan ng pagpapatunay sa pahayag na “C” (at pati na rin sa “D”) sa opisyal na pormulasyon ng Premyong Milenyo⁠(magbubukas sa bagong window).

Ang solusyon ay isang alimpuyo, isang umiikot na daloy ng likido, na pumupulupot paloob at lalong humahaba, gaya ng espageti. Ang sentral na bahaging ito ay lumiliit habang bumibilis sa paraang nananatiling may hangganan ang enerhiya nito, ayon sa hinihingi ng mga batas ng pisika. Ang teknikal na hamon ay ang mga ekwasyon ang bumuo ng pagkasira sa pamamagitan mismo ng galaw ng likido, sa halip na, halimbawa, maglagay tayo ng walang-hanggang puwersa nang mano-mano. Sa mas matematikal na paliwanag, ang mga termino sa mga ekwasyong Navier–Stokes na naglalarawan sa galaw—pagbilis, mga gradiyente ng presyon, paglipat ng momentum, biskosidad—ay dapat parehong maging malalaki ngunit magkansela sa tiyak na paraan. Iniiwan ng detalyadong balanseng ito ang isang makinis na panlabas na puwersa kahit na lumalaki nang walang hanggan ang bilis ng likido.

Mula noong Agosto 28, nagsasanay kami ng bagong panloob na modelo na nagpakita ng walang kapantay na pagganap sa aming mga pamantaya, kabilang ang matematika. Nagpapatuloy ang pagsasanay ng modelo ito at patuloy na bumubuti ang pagganap nito.

Noong Martes, Setyembre 1, nakarinig kami ng mga usap-usapan na nalutas na ang dalawang problema sa Premyong Milenyo. Dahil sa mga usap-usapang ito at sa malaking pag-angat sa pagganap ng aming panloob na modelo, sinimulan namin ang pagsisikap na suriin ito sa lahat ng hindi pa nalulutas na problema sa Premyong Milenyo at ilang iba pang problema na may mataas na epekto.

Gumamit kami ng sistema ng mga nag-uugnayang agent na pinapagana ng aming panloob na modelo. May access ang mga agent sa mga tool tulad ng kakayahang magbasa mula sa mga pansamantalang nakaimbak na bersyon ng internet at kakayahang magpatakbo ng code. Hinati ang mga agent sa mga grupong may kakayahang makipag-ugnayan sa loob ng grupo. Nagkakaiba ang laki ng mga grupo, at ang grupong nakagawa ng resolusyon sa Navier–Stokes ay kinabibilangan ng humigit-kumulang 10,000 sabay-sabay na mga agent. Sa lahat ng oras, pinanatili namin ang parehong mahihigpit na pananggalang na inilalapat namin sa lahat ng aming pagsusuri sa mga modelo ng frontier, kabilang ang pagsubaybay at paghihiwalay.

Para sa bawat problema, nagbigay kami ng mga prompt sa magkakaibang grupo ng mga agent gamit ang iba’t ibang bersyon ng pahayag ng problema, na sumasaklaw sa lahat ng bersyon ng problema. Para sa problemang Navier–Stokes, iminungkahi namin ang mga bersyong “A” at “B” (mga partikular na anyo ng problemang Navier–Stokes na magreresulta sa isang patunay) at mga bersyong “C” at “D” (na magreresulta sa isang pagpapabulaan) sa magkakahiwalay na grupo ng mga agent.

Bukod sa kumpletong mga problema sa Premyong Milenyo, hiniling namin sa aming sistemang multiagent na subukan ang isang hanay ng mga “mas madaling” problema. Isa sa mga problemang ito ay isang kahalintulad na tanong tungkol sa blowup para sa limitasyon ng problemang Navier–Stokes kung saan inalis ang terminong biskosidad. Kilala ito bilang problema sa regularidad para sa mga ekwasyon ni Euler, at nagulat kami nang malutas ng aming mga agent ang tanong na ito. Ang partikular na bersyon ng tanong na nalutas nila ay ang unforced na bersyon, kung saan walang panlabas na puwersang inilapat sa likido. Halos 100 ahente ang nagtulungan nang humigit-kumulang 50 oras upang gawin ang aming pagpapabulaan sa regularidad ng Euler¹.

Nang makita namin ang solusyon ni Euler, naisip namin na ang Navier–Stokes ang pinakamainam na problemang pagtuunan ng pansin. Kaya naman, nagpasya kaming ilaan ang aming mga mapagkukunan sa Navier–Stokes. Upang magawa ito, inilipat namin ang mga agent mula sa iba pang Problema sa Milenyo at binigyan ang mga agent na ito ng prompt gamit ang resolusyon ni Euler. Nang magkaroon ng mas sinanay na bersyon ng aming panloob na modelo habang isinasagawa ang pagsisikap, in-update namin ang aming mga ahente sa modelo iyon.

Hinikayat namin ang iba't ibang grupo ng mga agent na tuklasin ang sari-saring pamamaraan. Makalipas ang ilang panahon, pinag-ugnay namin ang mga grupo ng agent sa pamamagitan ng paggamit ng Codex upang pagsama-samahin ang pinakamahahalagang pananaw mula sa bawat grupo ng agent. Kumuha ang mga kasunod na prompt na ito sa sariling mga pansamantalang resulta ng mga agent. Ang grupong nakahanap ng solusyon sa Navier–Stokes ay ginabayan sa ganitong paraan.

Naabot ng mga ahente ang kanilang solusyon noong Sabado, Setyembre 5, humigit-kumulang 88 oras matapos ilunsad ang mga unang ahente. Tumagal ng karagdagang 17 oras ang pormalisasyon at beripikasyon gamit ang Lean sa pamamagitan ng GPT‑6 Astra.

Sa lahat ng problemang sinubukang lutasin, nagpadala ang mga agent ng 4.9 milyong mensahe at gumamit ng humigit-kumulang 300 bilyong mga output token. Sa proseso ng paglutas sa problemang Navier–Stokes, nagpadala ang mga ahente ng 2.7 milyong mensahe at gumamit ng humigit-kumulang 130 bilyong mga output token.

Nagsimula ang aming pagsisikap noong ika-1 ng Setyembre matapos makarinig ng isang usap-usapan na kalaunan ay napagtanto naming may kaugnayan kina Levent Alpöge, isang empleyado ng Anthropic, at Tristan Buckmaster, isang propesor ng matematika sa NYU.² Matapos makumpleto ang aming buong proyekto at ang beripikasyon sa Lean (noong ika-6 ng Setyembre), dahil naniniwala kami batay sa usap-usapan na mayroon din silang solusyon sa Navier–Stokes, nakipag-ugnayan kami sa kanila upang mag-alok ng sabayang paglalabas ng aming resulta at kilalanin ang kanilang pagkauna sa isang magkasanib na anunsyo. Sa puntong iyon nalaman namin na, gamit ang isang panloob na modelo ng Anthropic, nakagawa sila ng resolusyon sa problemang Euler na may panlabas na pwersa. Sa mga talakayang ito, inalok namin silang makita ang lahat ng mga prompt na ginamit namin at kalaunan ay makita ang patunay. Kinikilala namin ang priyoridad ng kanilang gawain sa Euler na may panlabas na pwersa at binabati namin sila sa kanilang kahanga-hangang tagumpay sa matematika.

Kami (ang mga mananaliksik at ang mga agent) ay hindi nakakita ng alinman sa kanilang gawain sa anumang paraan hanggang sa inilabas nila ito sa publiko—lalo na, walang partikular na data ng user ang in-access para malutas ang problemang ito.

Kasunod ng isang imbestigasyon, nakumpirma namin na ang mga prompt ng Codex ni Buckmaster sa loob ng dalawang buwan bago ang anunsyo at papel na ito noong Setyembre 8, 2026, ay hindi maaaring nakaimpluwensya sa sistema sa anumang paraan, kabilang na sa pamamagitan ng pagsasanay. Ang panloob na modelo ng OpenAI na ginamit para sa resultang ito ay binuo sa pamamagitan ng malakihang pagpapatibay ng pag-aaral batay sa isang dati nang sinanay na modelo. Malaki rin ang pagkakaiba ng aming mga patunay. Sa kaso ni Euler, pinatunayan nina Alpöge at Buckmaster ang isang resulta na may panlabas na puwersa, samantalang pinatunayan ng sistema ng OpenAI ang isang resulta na walang panlabas na puwersa.

Layunin namin sa paglalabas ng resultang ito na iulat ang malaking pag-unlad ng aming mga modelo ng AI. Hindi namin nilalayong angkinin ang Premyong Milenyo para sa resultang ito.

Ang mahalagang yugtong ito ay kumakatawan sa malaking pagsisikap ng mga matematiko at mananaliksik ng AI. Gayunpaman, hindi ito ang sukdulan, kundi isang larawan lamang sa isang punto ng panahon ng pag-unlad sa AI.

Naniniwala kami na nasa susunod na yugto na kami ng pag-unlad ng AI⁠, at ang mga resulta ngayon ay nagbibigay ng higit pang katibayan nito. Nakatuon kami sa pag-unawa sa modelong ito at paggamit sa aming natututuhan upang makatulong sa paggabay at pagtatakda ng bilis ng aming paghahangad ng higit pang pagsulong sa kakayahan. Isa sa aming mahahalagang layunin⁠ ay bumuo ng mga sistema ng AI na magagabayan, may pananagutan, at konektado sa mga tao, na maaaring mangailangan ng mas maingat na mga pagpili tungkol sa bilis ng pag-unlad, habang ipinagpapatuloy namin ang aming misyon na tiyaking makikinabang ang buong sangkatauhan sa AGI.