Dwa. OpenAI publikuje 722 prace matematyczne wygenerowane przez wewnętrzny model
Drugi fakt dotyczy granicy między modelem a nauką. Szóstego października OpenAI opublikowało na GitHubie, na licencji Apache 2.0, 722 manuskrypty matematyczne zgrupowane w 372 rodziny, którym towarzyszą formalizacje dowodów w Lean, skrócone podsumowania rozumowania oraz szacunki zużytego obliczenia. Jak podaje samo laboratorium w komunikacie „Sharing AI progress in mathematics", materiał powstał w niepublicznym modelu frontier, a średni wynik pochłonął obliczenie odpowiadające około trzem godzinom „myślenia" ChatGPT Pro; laboratorium podało modelowi około czterech tysięcy problemów, z których część trafiła do publikacji. To rozwinięcie wrześniowej deklaracji OpenAI o rozwiązaniu problemu Naviera-Stokesa z milenijnej listy Clay Mathematics Institute. Wśród dziesięciu opublikowanych podsumowań rozumowania są wyniki dotyczące wykładnika niewymierności liczby pi, hipotezy Kaplansky'ego czy formuły Mézarda-Parisiego dla szkła spinowego, a dwa przypadki potraktowano odrębnie: obszar bez zer funkcji dzeta Riemanna, którego manuskrypt lekko zredagowali ludzie, oraz dowód hipotezy Hodge'a dla rozmaitości abelowych o mnożeniu zespolonym.
Krytyczna ocena jest tu absolutnie konieczna i sam OpenAI ją częściowo ułatwia. Formalizacja w Lean sprawdza jedynie, czy zakodowany dowód wynika z przyjętych definicji, aksjomatów i zależności w danym środowisku — nie rozstrzyga, czy formalne twierdzenie odpowiada temu z pracy, czy definicje oddają zamierzone pojęcia, czy założenia są dopuszczalne ani czy wynik jest nowy i istotny. Część wyników nie ma jeszcze formalizacji i wymaga zwykłej recenzji eksperckiej. Sam proces także nie jest w pełni odtwarzalny, bo OpenAI nie podało ustawień próbkowania, sprzętu ani pełnych śladów rozumowania, a wcześniejsza zapowiedź o Navierze-Stokesie spotkała się z publicznym pytaniem matematyka z Uniwersytetu Nowojorskiego Tristana Buckmastera, gdy laboratorium mówiło wówczas o dziesięciu tysiącach agentów pracujących przez osiemdziesiąt osiem godzin. Warto więc traktować to jako otwarcie nowego trybu publikacji naukowej, a nie jako ustalony dorobek: kluczowa jest infrastruktura dowodowa — wersjonowane cytowania, ślad korekt i nadzór niezależnej grupy doradczej do spraw matematyki i sztucznej inteligencji przy Institute for Advanced Study, która powstała po krytyce wokół Naviera-Stokesa. Sygnał społeczny jest przy tym nie do przeoczenia: na czele Hacker News znalazło się tego dnia ogłoszenie OpenAI z ponad sześciuset siedemdziesięcioma punktami i ponad sześciuset komentarzami, co pokazuje, że debata przeniosła się z „czy model umie dowodzić" na „jak weryfikować i przypisywać takie wyniki".
Źródło: hacker-news