Astra od OpenAI: 10 problemów matematycznych, formalne dowody i wiele pytań

Jakich problemów dotyczyły wyniki Astry?

Lista obejmuje bardzo różne dziedziny: geometrię wielowymiarową, teorię kodowania, złożoność obwodów arytmetycznych, teorię grup, algebry operatorowe, złożoność kwantową, kryptografię kratową oraz kombinatorykę ekstremalną .

1. Upakowanie sfer w dużych wymiarach — nowe górne ograniczenia gęstości upakowania, sięgające progu Cohn–Elkiesa .
2. Kody binarne i sferyczne — wykładniczo lepsze ograniczenia maksymalnego rozmiaru kodu przy zadanej minimalnej odległości .
3. Grupy niesoficzne — jawna konstrukcja pokazująca istnienie grup niesoficznych, co było jednym z istotnych otwartych pytań teorii grup .
4. Hipoteza sztywności Connesa — obalenie wieloletniej hipotezy dotyczącej algebr von Neumanna .
5. Złożoność obwodów arytmetycznych — nowe dolne ograniczenia dla obliczania wyznacznika macierzy, w tym ograniczenie dla formuł arytmetycznych rzędu (n^4/\log n) .
6. Kwantowa wielokrotna równoległość — wykładnicze twierdzenie o powtarzaniu równoległym dla ogólnych dwuosobowych gier kwantowych .
7. Problem najbliższego wektora — trudność aproksymacji w czynniku wielomianowym; problem ma znaczenie dla kryptografii postkwantowej .
8. Hipoteza objętości Ehrharta — ustalenie maksymalnej objętości ciała wypukłego, którego środek ciężkości jest jedynym wewnętrznym punktem kratowym .
9. Wielokolorowe liczby Ramseya — superwykładnicze dolne ograniczenie, rozwiązujące problem 183 Erdősa .
10. Hipotezy dotyczące liczb ekstremalnych — wyniki dotyczące hipotez zwartości i degeneracji, rozwiązujące problemy 146 i 180 Erdősa .

Lean 4 jako mechaniczny test dowodów

OpenAI nie udostępniło samej Astry. Zamiast tego opublikowało na GitHubie certyfikaty dowodów w Lean 4 na licencji Apache 2.0. Repozytorium ma według firmy zerową liczbę elementów oznaczonych jako „sorry”, co oznacza, że każdy krok wszystkich dziesięciu sformalizowanych dowodów został zweryfikowany przez system .

To ważne rozróżnienie. Lean nie ocenia, czy pomysł matematyczny jest interesujący ani kto go stworzył, ale mechanicznie sprawdza, czy zapisany dowód wynika z przyjętych założeń. Taki proces ogranicza typowy problem z rozumowaniem generowanym przez AI: przekonujący tekst może zawierać błąd, którego na pierwszy rzut oka nie widać.

Entuzjazm i sceptycyzm środowiska naukowego

Część badaczy, w tym Noam Brown, uznała ogłoszenie za ważny krok w kierunku wykorzystania AI do rozumowania naukowego . Jednocześnie pojawiło się kilka poważnych zastrzeżeń.

To nie są problemy milenijne

Żaden z dziesięciu problemów nie znajduje się na liście problemów milenijnych Instytutu Claya, takich jak P kontra NP czy hipoteza Riemanna . Nie oznacza to, że są błahe — przeciwnie, dotyczą realnych, trudnych pytań badawczych. Jednak ich rozwiązanie nie ma takiej samej rozpoznawalności medialnej jak zdobycie jednej z nagród milenijnych.

Jednym z najgłośniejszych rezultatów jest pierwsza jawna konstrukcja grupy niesoficznej. Pytanie to pozostawało otwarte od czasu wprowadzenia pojęcia soficzności przez Michaiła Gromowa w 1999 r.

Brak wcześniejszej recenzji naukowej

Wyniki ogłoszono bez wcześniejszej publikacji w recenzowanym czasopiśmie matematycznym lub materiałach konferencyjnych . Krytycy podkreślają, że formalna weryfikacja w Lean sprawdza poprawność konkretnego zapisu, ale nie rozstrzyga jeszcze, czy interpretacja rezultatu i jego znaczenie są przedstawione właściwie.

Niejasna pozostaje także granica między odkryciem dokonanym przez model a pracą ludzi, którzy kierowali procesem, wybierali problemy i przygotowali finalne manuskrypty. Samo OpenAI odniosło się do tego napięcia, przywołując deklarację z Lejdy dotyczącą AI i matematyki .

Czy sukces w matematyce przełoży się na inne dziedziny?

Kognitywista Gary Marcus argumentował, że sukces w formalnej matematyce może być „szczególnym przypadkiem” i nie musi oznaczać przełomu w ogólnym rozumowaniu naukowym . Matematyka ma wyjątkową cechę: wiele wyników można zapisać w sposób formalny i jednoznacznie zweryfikować za pomocą narzędzi symbolicznych. Ponadto łatwiej tworzyć dla niej syntetyczne dane z gwarantowaną poprawnością niż dla większości nauk empirycznych.

Problem powtarzalności

Niezależne odtworzenie procesu generowania rozwiązań jest obecnie niemożliwe. Astra nie została udostępniona publicznie, a szczegółowa metodologia promptowania nie została w pełni ujawniona . Badacze mogą analizować opublikowane dowody, ale nie mogą sprawdzić, czy uzyskaliby taki sam rezultat, korzystając z identycznego modelu i procedury.

Pojawiły się też pytania o moment ogłoszenia. OpenAI jednocześnie pozycjonuje Astrę jako swoją kolejną dużą rodzinę modeli, co skłoniło część obserwatorów do zastanawiania się, czy publikacja nie została zaplanowana również z myślą o efekcie marketingowym .

Co naprawdę oznacza ogłoszenie OpenAI?

Jeśli niezależni eksperci potwierdzą poprawność i znaczenie przedstawionych argumentów, kilka z nich może zamknąć problemy otwarte od dziesięcioleci. Szczególnie istotna byłaby konstrukcja grupy niesoficznej, która rozstrzyga pytanie pozostające bez odpowiedzi przez ponad 25 lat . Nawet ostrożni komentatorzy przyznają, że OpenAI przedstawiło znacznie więcej materiału możliwego do zbadania niż typowe korporacyjne ogłoszenie .

Na ostateczny werdykt jest jednak za wcześnie. Najważniejsze pytanie nie brzmi dziś, czy Astra „potrafi matematykę”, lecz czy skuteczne rozwiązywanie formalnych i maszynowo sprawdzalnych problemów w wąskiej dziedzinie przekłada się na uniwersalne badania naukowe. Tego ogłoszenie OpenAI jeszcze nie dowodzi.