OpenAI wymusza osobliwość Naviera-Stokesa

Równania Naviera–Stokesa opisują ruch płynów: od prądów oceanicznych i smug dymu po strumień wody z ogrodowego węża. Matematycy wciąż nie wiedzieli, czy ich trójwymiarowe rozwiązania zawsze pozostają gładkie i skończone, czy też mogą osiągnąć osobliwość, czyli stan, w którym przestają dawać skończony wynik. To jeden z siedmiu problemów milenijnych Clay Mathematics Institute. 8 września OpenAI opublikowało 166-stronicowy manuskrypt oraz formalny dowód możliwy do sprawdzenia maszynowego, twierdząc, że znalazło rozwiązanie. Trzy dni później Clay odpowiedział, że problem „najwyraźniej został rozstrzygnięty”. To ocena wyjątkowo przychylna, ale nadal wyraźnie warunkowa.

Zakres tej deklaracji jest węższy, niż wynikałoby z wielu publikacji. Rezultat OpenAI dotyczy płynu poddanego działaniu siły zewnętrznej: odpowiednio zaprojektowany, gładki impuls ma doprowadzać początkowo nieruchomy płyn do osobliwości w skończonym czasie. Nie rozstrzyga natomiast, czy podobne załamanie może nastąpić samoistnie w zwykłym płynie, na który nie działa taka siła. Bez tego rozróżnienia łatwo przecenić znaczenie przedstawionego dowodu.

Dlaczego siła zewnętrzna ma znaczenie

W oficjalnym sformułowaniu problemu Clay wskazał cztery dopuszczalne drogi do rozwiązania. Dwie polegają na wykazaniu, że gładki przepływ zawsze zachowuje regularność. Dwie pozostałe, oznaczone jako warianty C i D, wymagają skonstruowania sytuacji, w której początkowo gładki przepływ nieuchronnie traci tę właściwość. W obu przypadkach Clay wyraźnie dopuszcza zastosowanie gładkiej siły zewnętrznej.

Tę właśnie drogę wybrało OpenAI. Zgodnie z manuskryptem dla każdego poziomu lepkości, czyli właściwości odpowiadającej za to, że miód płynie wolniej od wody, można skonstruować gładką siłę, która doprowadzi początkowo nieruchomy płyn do osobliwości. Jednocześnie jego całkowita energia kinetyczna pozostanie ograniczona. Jeżeli dowód okaże się poprawny, spełni warunki określone przez Clay.

Punktem wyjścia były wcześniejsze badania. Hiszpańscy matematycy Diego Córdoba i Luis Martínez-Zoroa wraz z Fan Zhengiem wykazali już w preprincie, że wymuszona osobliwość może wystąpić w osłabionej wersji równań, w której sztucznie ograniczono wygładzające działanie lepkości. Deklarowanym osiągnięciem OpenAI jest przeniesienie tej metody na pełne, niezmodyfikowane równania.

Co sprawdza Lean

Nietypowy charakter pracy wynika z dołączonego repozytorium Lean 4. Lean jest programem wspomagającym tworzenie dowodów, który odrzuca każdy krok niewynikający z zakodowanych definicji i przyjętych reguł. Poprawność poszczególnych wnioskowań kontroluje niewielki, uznawany za zaufany rdzeń oprogramowania.

Takie rozwiązanie znacznie ułatwia weryfikację w porównaniu z analizą samego tekstu matematycznego. Lean bada jednak wyłącznie spójność wewnętrzną: sprawdza, czy wnioski rzeczywiście wynikają z zapisanych w systemie definicji. O tym, czy definicje te wiernie obejmują wszystkie warunki sformułowanego po angielsku problemu Clay, muszą rozstrzygnąć specjaliści od dynamiki płynów. Zarówno manuskrypt, jak i repozytorium opublikowała sama firma; nie są to prace po recenzji naukowej. Do 14 września nie udokumentowano publicznie pełnego, niezależnego audytu repozytorium.

Według OpenAI wynik analityczny opracował własnościowy system wielu równolegle działających modeli AI, a następnie model GPT-6 Astra sformalizował dowód w Lean (OpenAI). Podawanych przez firmę danych o skali i szybkości tego procesu nie można niezależnie odtworzyć. Osoby z zewnątrz mogą zbadać rezultat, ale nie są w stanie powtórzyć sposobu jego wygenerowania.

Jak podał Quanta Magazine, około dwunastu godzin przed komunikatem OpenAI Tristan Buckmaster z NYU oraz związany z Anthropic Levent Alpöge przedstawili pokrewne, wspomagane przez AI wyniki dotyczące sąsiednich równań opisujących płyny. Oni również wykorzystali strategię Córdoby i Martíneza-Zoroi. Zbieżność prac dwóch korporacyjnych laboratoriów AI pokazuje zarazem, jak wiele zawdzięczają one wcześniejszym badaniom akademickim.

Co wydarzy się dalej

Zgodnie z regulaminem nagrody rozwiązanie musi zostać opublikowane w uznanym czasopiśmie recenzowanym, przejść co najmniej dwuletnią weryfikację środowiska naukowego i zdobyć powszechną akceptację. Dopiero wtedy specjalna komisja może rozpocząć obrady nad przyznaniem nagrody. Nie zidentyfikowano dotąd czasopisma, do którego OpenAI miałoby przesłać swój manuskrypt.

Jeżeli niezależna ocena potwierdzi poprawność dowodu, będzie to oznaczało, że standardowe trójwymiarowe równania Naviera–Stokesa z gładką siłą zewnętrzną mogą w skończonym czasie doprowadzić do osobliwości. Nadal otwarte pozostanie pytanie o przypadek bez wymuszenia: czy płyn pozostawiony własnej dynamice może samoistnie utracić regularność. Odpowiedź otrzymałaby zatem jedna część wielowiekowego problemu. Druga wciąż czekałaby na rozwiązanie.