OpenAI opublikowało propozycję dowodu osobliwości Naviera

OpenAI ogłosiło 8 września rozwiązanie jednego z wariantów problemu milenijnego Naviera–Stokesa, znalezione przez wewnętrzny model AI. Firma udostępniła pracę matematyczną i formalizację w Lean. Wynik dotyczy przepływu z odpowiednio dobraną siłą zewnętrzną; nie rozstrzyga analogicznego pytania dla płynu bez wymuszenia.

Publikacji towarzyszy spór z matematykami Tristanem Buckmasterem i Leventem Alpögem, którzy wcześniej uzyskali pokrewne wyniki dla innych równań. Poprawność twierdzenia, udział ludzi w badaniach i pierwszeństwo odkrycia wymagają osobnego sprawdzenia. Na stronie Clay Mathematics Institute problem nadal ma status nierozwiązanego.

Osobliwość przy gładkiej sile zewnętrznej

Równania Naviera–Stokesa opisują ruch lepkiego płynu. W trzech wymiarach nie wiadomo ogólnie, czy początkowo gładki przepływ pozostanie gładki przez dowolnie długi czas. Osobliwość oznacza tu utratę wymaganej regularności rozwiązania, a nie zaobserwowaną eksplozję fizycznej cieczy.

W pracy OpenAI prędkość początkowa wynosi zero, siła zewnętrzna jest gładka i działa w ograniczonym obszarze przestrzeni i czasu, a energia kinetyczna pozostaje ograniczona. Mimo tego największa wartość prędkości ma rosnąć bez ograniczenia przed upływem skończonego czasu. Konstrukcja dotyczy każdej dodatniej lepkości.

Autorzy opisują kurczący się wir oraz dodatkowe, szybko oscylujące zaburzenia przepływu. Samego wiru nie dałoby się podtrzymać gładką siłą: potrzebna siła również stałaby się osobliwa. Zaburzenia dostarczają brakującego transportu pędu, dzięki czemu zewnętrzne wymuszenie może pozostać gładkie. To zasadnicza trudność konstrukcji, której nie rozwiązuje samo znalezienie pola prędkości rosnącego do nieskończoności.

Oficjalna definicja problemu dopuszcza cztery alternatywy. Warianty A i B dotyczą globalnego istnienia gładkich rozwiązań bez siły zewnętrznej. Warianty C i D pozwalają wykazać załamanie regularności przy gładkim wymuszeniu, odpowiednio w całej przestrzeni i przy periodycznych warunkach przestrzennych. OpenAI wskazuje C i D. Taki wynik mieściłby się w warunkach problemu milenijnego, ale nie uzasadnia twierdzenia, że dowiedziono osobliwości w układzie bez wymuszenia.

Co można sprawdzić w formalizacji Lean

Repozytorium NavierStokesAndEuler zawiera formalizacje obu wariantów Naviera–Stokesa oraz osobnego wyniku dla równań Eulera bez wymuszenia. Euler opisuje płyn bez lepkości, więc jego wyniku nie można przenieść wprost na równania Naviera–Stokesa.

Lean sprawdza, czy zapisane twierdzenie wynika z przyjętych definicji, założeń i kroków dowodowych. Publiczne pliki pozwalają innym badaczom odtworzyć sprawdzenie. Repozytorium określa wersję Lean 4.34.0-rc2 i zależności biblioteczne. Udostępnia również procedurę z dodatkowym weryfikatorem, która porównuje wynik z osobno zdefiniowanym zadaniem i sprawdza wyeksportowany dowód.

Nadal trzeba ocenić, czy formalne definicje odpowiadają treści problemu Clay i jak formalizacja wiąże się z argumentem przedstawionym w artykule. Komunikat autora repozytorium o udanej kontroli nie zastępuje publicznego odtworzenia przez niezależnych badaczy. Kontrola logiczna nie ustala też, skąd pochodził pomysł ani jakie dane widział model podczas treningu.

Tysiące agentów i interwencje badaczy

Według OpenAI grupa pracująca nad Navierem–Stokesem obejmowała około 10 tys. równoległych agentów. Wytworzyła 2,7 mln wiadomości i 130 mld tokenów wyjściowych. Znalezienie rozwiązania zajęło 88 godzin, a jego formalizacja i sprawdzenie kolejne 17 godzin z użyciem GPT-6 Astra. Axios relacjonuje, że firma mówiła na konferencji prasowej o milionach dolarów kosztu obliczeń, bez dokładnej kwoty.

Ludzie wybrali priorytetowy problem, przekazywali wcześniejsze wyniki, aktualizowali model i scalali ustalenia grup za pomocą Codex. Opis dotyczy zatem modelu pracującego w rozbudowanym środowisku agentowym, z narzędziami i wymianą informacji. Model odkrywający dowód nie został udostępniony publicznie. Te liczby nie określają możliwości ani kosztu zwykłej sesji z Astrą.

Pierwszeństwo i niewyjaśnione pochodzenie danych

W oświadczeniu Buckmastera przełom we wspólnej pracy z Alpögem nastąpił 15 sierpnia, a formalne sprawdzenie 22 sierpnia. Badacze opublikowali wyniki dotyczące wymuszonych równań Eulera, Boussinesqa i modelu przepływu w ośrodku porowatym. Korzystali z Claude’a i Codex, rozwijając kierunek zapoczątkowany przez Diega Córdobę i Luisa Martíneza-Zoroę. Buckmaster podkreśla, że znalezienie rozwiązania poprzedzało wielotygodniową pracę nad czytelnym dowodem.

Alpöge pracuje w Anthropic, lecz według oświadczenia była to ich osobista współpraca naukowa, niezwiązana umową z pracodawcami. Buckmaster kwestionuje pomniejszanie wkładu ludzi i opisuje naciski dotyczące publikacji. TechCrunch relacjonuje jego zarzut, że wyścig z OpenAI wymusił pośpieszne ogłoszenie wyników.

Buckmaster pyta też, czy rozmowy prowadzone przez badaczy w produktach OpenAI mogły wpłynąć na model. Wyraźnie zaznacza, że tego nie wie; pisząc oświadczenie, nie widział jeszcze dowodu firmy. Nie jest to ustalony przypadek przejęcia dowodu.

OpenAI odpowiada, że jego badacze i agenci nie widzieli pracy konkurentów przed publikacją ani nie sięgali po ich konkretne dane użytkowania. Firma nie wyklucza jednak wpływu zanonimizowanych danych produktowych na ogólne ulepszanie modeli. Przyznaje wcześniejszą datę wyniku Buckmastera i Alpögego dla wymuszonych równań Eulera.

Udostępnianie kierunków badań przed publikacją

Terence Tao argumentuje, że wybór problemu obiecującego naukowo wymaga wiedzy o całej dziedzinie. Sama możliwość szybkiego uzyskania poprawnego rozwiązania nie mówi jeszcze, czego nauczy ono o problemach sąsiednich. Matematyk obawia się, że uruchamianie ogromnych zasobów AI po usłyszeniu o cudzym projekcie będzie zniechęcać badaczy do dzielenia się pomysłami. Brak publikacji nieudanych prób dodatkowo utrudnia ocenę, które zadania pozostają poza zasięgiem modeli.

Tao postuluje ocenianie automatycznych rozwiązań także według tego, czy objaśniają metody i pomagają wybrać dalsze kierunki pracy. Jego argument nie rozstrzyga zarzutów wobec OpenAI. W tym sporze ocena wkładu zespołów wymaga datowanych zapisów badań i informacji o dostępie do danych, których nie dostarcza samo sprawdzenie dowodu.

Źródła

Źródła pierwotne

Niezależne analizy i relacje

Dyskusje publiczne

Terence Tao: wybór problemów i skutki wyścigu do publikacji

Wykorzystuję treści generowane przez AI jako część mojego codziennego procesu nauki.

OpenAI opublikowało propozycję dowodu osobliwości Naviera–Stokesa