10 000 agentów AI i 90 lat czekania. OpenAI twierdzi, że rozwiązało Problem Milenijny Naviera-Stokesa
Przez niemal wiek matematycy i fizycy spierali się o to, czy równania opisujące dynamikę płynów zawsze gwarantują gładki, przewidywalny przepływ, czy też potrafią załamać się w skończonym czasie.
OpenAI opublikowało 165-stronicowy preprint dowodu, który wywołał potężne poruszenie w środowisku naukowym: wewnętrzny model firmy, sterując armią 10 tysięcy równoległych agentów, skonstruował matematyczny wir prowadzący do powstania osobliwości. Co najważniejsze, formalny szkielet dowodu został sprawdzony w systemie Lean 4, a w tle całego odkrycia rozgrywa się technologiczny wyścig napędzany pracami badaczy z Anthropic i NYU.
Wir kurczący się jak spaghetti: co tak naprawdę udowodniono?
Równania Naviera-Stokesa, sformułowane w XIX wieku, traktują płyn jako ośrodek ciągły, pomijając ruch pojedynczych cząsteczek. W 2000 roku Instytut Matematyczny Claya umieścił zagadnienie istnienia i gładkości rozwiązań tych równań na liście siedmiu Problemów Milenijnych. W oficjalnym manifeście Charles Fefferman przewidział cztery równorzędne drogi do rozwiązania problemu: warianty A i B (dowód wiecznej gładkości w przestrzeni R3 lub na torusie) oraz warianty C i D (wykazanie załamania gładkości, przy obecności gładkiej siły zewnętrznej).
OpenAI uderzyło w wariant C oraz D. Twierdzenie 1.1 w opublikowanym dokumencie dowodzi, że dla dowolnej dodatniej lepkości istnieje gładka, przestrzennie ograniczona siła zewnętrzna, przy której początkowo spokojny płyn w skończonym czasie rozwija nieograniczoną prędkość w jednym punkcie, zachowując przy tym ściśle ograniczoną energię kinetyczną.
Konstrukcja opiera się na samopodobnym wirze o niezwykle specyficznej geometrii. Rdzeń wiru kurczy się promieniowo szybciej, niż rozciąga się w pionie, przypominając gwałtownie wydłużające się spaghetti. Płyn spiralnie zapada się do środka i wystrzeliwuje wzdłuż osi. W miarę zbliżania się do krytycznego momentu prędkość dąży do nieskończoności, ale objętość wirującego obszaru maleje tak szybko, że energia kinetyczna samego rdzenia dąży do zera.
To nie jest proste wtłoczenie nieskończonej siły z zewnątrz. Istotą 165-stronicowego dowodu jest dodanie oscylacyjnych zaburzeń (fal), których nieliniowy transport pędu samoczynnie kompensuje osobliwe składowe równania. W efekcie siła zewnętrzna pozostaje gładka, podczas gdy sam model continuum załamuje się matematycznie.
Dla fizyki nie oznacza to, że woda w szklance nagle wybuchnie do prędkości światła. Oznacza to dowód, że w skrajnych warunkach klasyczne równania Naviera-Stokesa przestają poprawnie modelować rzeczywistość i wymuszają zejście do opisu na poziomie pojedynczych cząstek.
130 miliardów tokenów w 88 godzin
Skala operacji analitycznej, którą opisuje OpenAI, pokazuje zupełnie nowy paradygmat pracy naukowej. Do zbadania problemu wykorzystano niewydany publicznie model wewnętrzny (bardziej zaawansowany od GPT-6 Astra). System podzielono na zespoły koordynujących agentów wyposażonych w dostęp do interpretera kodu i pamięci podręcznej sieci.
Nad samym problemem Naviera-Stokesa pracowało równolegle około 10 000 agentów. W ciągu zaledwie 88 godzin maszyny wymieniły między sobą 2,7 miliona wiadomości i wygenerowały 130 miliardów tokenów wyjściowych.
Co istotne, nie mamy tu do czynienia z bezmyślnym losowaniem formuł. Brutalna siła obliczeniowa posłużyła do przeszukania gigantycznego drzewa podejść analitycznych, ale wygenerowany dowód posiada rygorystyczną, wieloetapową architekturę: od budowy profilu bazowego, przez teorię naprężeń w pierścieniach, aż po zaawansowane całkowanie wypukłe i przestrzenne wygaszanie zaburzeń.
Lean 4 i koniec z halucynacjami
Największą przeszkodą przy wykorzystaniu LLM-ów w matematyce wyższej było dotąd ryzyko subtelnych halucynacji – błędów logicznych, które człowiek musiałby mozolnie tropić tygodniami. W tym przypadku OpenAI zastosowało inną strategię: pełną formalizację weryfikacyjną.
Dowód został w całości przetłumaczony na język Lean 4, a jego poprawność logiczna została potwierdzona. Proces ten zajął modelowi GPT-6 Astra kolejne 17 godzin. Weryfikacja w Lean nie jest prostym kalkulatorem sprawdzającym rachunki – to rygorystyczne sprawdzenie, czy każdy krok rozumowania wynika bezwzględnie z przyjętych aksjomatów.
Co kluczowe, repozytorium projektu zawiera niezależną warstwę sprawdzającą (Comparator). Rozwiązuje to fundamentalny problem zaufania: potwierdza, że model rzeczywiście udowodnił tezę postawioną przez Feffermana w manifeście Instytutu Claya, a nie jej uproszczony, wygodny dla siebie wariant.
Wyścig w cieniu Anthropic i zagadkowy zapis o danych
Kulisy powstania publikacji rzucają unikalne światło na tempo rywalizacji w Dolinie Krzemowej. OpenAI przyznaje wprost: impuls do badań pojawił się 1 września, gdy do laboratorium dotarła plotka, że dwaj naukowcy – Tristan Buckmaster (matematyk z New York University) oraz Levent Alpöge (zatrudniony w Anthropic) – rozwiązali dwa Problemy Milenijne.
OpenAI natychmiast przekierowało moce obliczeniowe na wszystkie otwarte problemy z listy Claya, a po wstępnym sukcesie na prostszych równaniach Eulera skoncentrowało całą flotę 10 tysięcy agentów na Navierze-Stokesie. Kiedy 6 września przedstawiciele OpenAI odezwali się do Buckmastera i Alpöge z propozycją wspólnego ogłoszenia wyników, okazało się, że tamci pracowali nad innym zagadnieniem – wymuszonymi równaniami Eulera (co odnotował m.in. magazyn Nature).
W oficjalnym komunikacie OpenAI znalazł się jednak niezwykle intrygujący dopisek natury etycznej. Firma zaznacza, że jej badacze nie mieli wglądu w prace konkurentów przed publikacją, ale dodaje:
„Choć to mało prawdopodobne, nie możemy wykluczyć, że zanonimizowane dane pochodzące z korzystania z naszych produktów przez tych badaczy pomogły ulepszyć nasze modele”.
To zdanie z pewnością wywoła gorącą debatę w środowisku akademickim na temat granic prywatności i wykorzystywania danych z promptów czołowych naukowców korzystających z komercyjnych narzędzi AI.
Zwieńczeniem historii jest deklaracja finansowa: OpenAI ogłosiło, że nie zamierza ubiegać się o milion dolarów nagrody od Instytutu Claya. W grze o prestiż technologiczny i potwierdzenie dominacji w sektorze sztucznej inteligencji milion dolarów to zaledwie ułamek kosztu prądu zużytego na te 88 godzin obliczeń.
