OpenAI ogłasza trzy „odkrycia” modeli AI i prosi zewnętrznych ekspertów o ich sprawdzenie

OpenAI opublikowało wpis o trzech wynikach, które według firmy wygenerowały jej wewnętrzne modele: z analizy harmonicznej, teorii złożoności obliczeniowej i fizyki matematycznej. Sama firma nazywa manuskrypty „surowymi danymi badawczymi”, które dopiero trzeba zamienić w zrozumienie naukowe. W tym celu poprosiła zewnętrznych ekspertów, by objęli rolę „pasterzy” (shepherds) i zorganizowali grupy do ich analizy.

Trzy wyniki, trzy strategie publikacji

Matematyka. Modele OpenAI miały udowodnić hipotezę lokalnego wygładzania (zaproponowaną przez Sogge’a w 1991 roku) we wszystkich wymiarach. Wcześniej, w 2019 roku, Guth, Wang i Zhang udowodnili ją dla dwóch wymiarów przestrzennych. Hipoteza ta pociąga za sobą m.in. hipotezę Kakeyi i hipotezę restrykcyjną Steina, więc według OpenAI wynik rozwiązuje je również we wszystkich wymiarach. Wang i Zahl udowodnili hipotezę Kakeyi w trzech wymiarach dopiero w 2025 roku. Dowód ma się opierać na nowym pomocniczym równaniu różniczkowym cząstkowym. Wynik pochodzi z 18 października, a dzień później został sformalizowany w Lean. Na zalecenie konsultowanego eksperta OpenAI opublikowało na GitHubie zarówno opis w języku naturalnym, jak i dowód w Lean, a badacze mogą sami zorganizować jego analizę.

Informatyka. Najgłośniejsze jest twierdzenie, że Exponential Time Hypothesis (ETH) jest fałszywa. To hipoteza o złożoności problemu spełnialności formuł logicznych, blisko związanego z problemem P vs NP. Według OpenAI ETH była powszechnie uznawana za prawdziwą i posłużyła w setkach prac do wyprowadzania warunkowych wyników o trudności problemów, m.in. w teorii grafów, biologii obliczeniowej, bazach danych i geometrii obliczeniowej. Obalenie ma pochodzić z 16 października, a formalizacja w Lean z 17 października. Firma zastrzega, że przełożenie tego na praktyczne algorytmy będzie wymagało „znacznych dalszych badań”.

Weryfikację poprowadzą Russell Impagliazzo i Ramamohan Paturi z UC San Diego oraz Ryan Williams z MIT. Impagliazzo i Paturi razem z Francisem Zane’em sformułowali ETH, a Williams obalał jej mocne warianty. Grupa zażądała, by OpenAI upubliczniło wszystkie surowe dane i sfinansowało konferencję o skutkach wyniku dla dziedziny. Firma się zgodziła.

Fizyka. OpenAI twierdzi, że ma matematycznie ścisły dowód istnienia pewnych oddziałujących kwantowych teorii pola z polami cechowania i fermionami w czterech wymiarach. Obejmują one chromodynamikę kwantową (QCD) oraz zunifikowane uzupełnienie Modelu Standardowego. Praca rozwija podejście Balabana, a jako podproblem zawiera istnienie czystej teorii Yanga–Millsa, czyli część jednego z problemów milenijnych Clay Mathematics Institute. Grupę poprowadzi David Gross, laureat Nobla z 2004 roku, a w jej skład wejdą Michael Douglas, Arthur Jaffe, Igor Klebanov i Nikita Nekrasov. Tu strategia jest najbardziej zachowawcza: grupa postanowiła na razie nie ujawniać artefaktów wygenerowanych przez AI i samodzielnie przygotować opis wyniku.

Zasady współpracy i ich ograniczenia

OpenAI deklaruje cztery zasady: przejrzystość (brak umów o poufności, badacze mogą swobodnie publikować wnioski), rezygnację z akademickiego uznania za odkrycia modeli, uznanie dla grup za wypracowane zrozumienie i teksty oraz niezależność. Udział jest dobrowolny i nieodpłatny, a członkowie grup nie mówią w imieniu OpenAI. Firma przyznaje też, że wybór pierwszych „pasterzy” kształtuje, kto zaangażuje się jako pierwszy, i tworzy asymetrię informacji. Nie wie jeszcze, które z trzech podejść okaże się najlepsze.

Ostrożność wobec wyniku jest uzasadniona. The Decoder przypomina, że Lean sprawdza tylko, czy dowód ustanawia twierdzenie w tej postaci, w jakiej zapisano je w Lean. To, czy zapis oddaje zamierzony problem, muszą ocenić eksperci. Z kolei Impagliazzo, Paturi i Williams podkreślają w liście otwartym, że ich udział nie jest poparciem tego wyniku, bo tak duży wynik „wymaga starannej, niezależnej weryfikacji”. Williams na X przyznał, że nie wiadomo, co ten wynik zmieni w praktycznym rozwiązywaniu SAT. Williams uznał poważny postęp w ciągu 12 miesięcy za możliwy, ale dodał, że równie dobrze może nie nastąpić żaden.

Problem formalizacji nie jest teoretyczny. New Scientist opisał zarzut, że w dowodzie dla równań Naviera–Stokesa mogło dojść do błędnego przełożenia matematyki na Lean. W połowie października pisaliśmy też, że matematycy kwestionują opis dowodu OpenAI. Nowa procedura, z zewnętrznymi grupami i publicznymi danymi, wygląda jak odpowiedź na te zastrzeżenia. Czy wyniki wytrzymają kontrolę, okaże się dopiero po pracy grup, a w przypadku fizyki także po ujawnieniu przez nie materiałów.