OpenAI twierdzi, że ich najnowszy model sztucznej inteligencji, Astra, rozwiązał zadania matematyczne, które od dziesięcioleci stanowiły wyzwanie dla naukowców. Ale jak znaczący jest ten przełom i co dokładnie udało się osiągnąć temu modelowi? Przyjrzyjmy się bliżej tym twierdzeniom, badaniom, na których się opierają, oraz temu, co mogą one oznaczać dla przyszłości matematyki i sztucznej inteligencji.
TREŚĆ ARTYKUŁU:
Ogłoszenie ukryte w trzecim akapicie
Jest coś symbolicznego zarówno w momencie, jak i w sposobie, w jaki OpenAI zdecydowało się zaprezentować swój prawdopodobnie najbardziej ambitny jak dotąd model sztucznej inteligencji. Zamiast organizować specjalną konferencję prasową czy uruchamiać głośną kampanię zapowiadającą na X, firma przedstawiła Astrę w publikacji naukowej poświęconej wyłącznie wynikom matematycznym. Nazwa modelu pojawia się dopiero w trzecim akapicie. Jak na firmę, która tradycyjnie zamienia każde większe wydanie w wydarzenie medialne, takie podejście wydaje się niemal celowo skromne. Jednak ta powściągliwość, w połączeniu ze skalą deklarowanych osiągnięć, sprawia, że ta historia jest o wiele bardziej fascynująca niż ogłoszenie kolejnej wersji chatbota.
Formalnie ogłoszenie dotyczy wewnętrznej wersji modelu, która nie została jeszcze udostępniona. Według OpenAI model Astra albo całkowicie rozwiązał, albo poczynił znaczne postępy w dziesięciu długotrwałych, nierozwiązanych problemach – zagadnieniach, które od co najmniej dekady, a w niektórych przypadkach nawet od kilkudziesięciu lat, stanowią wyzwanie dla matematyków i teoretyków informatyki.
Przeczytaj też: Wszystko, co musisz wiedzieć o Kimi K3 firmy Moonshot AI: jak chiński startup rzucił wyzwanie gigantom AI
Co kryje się za liczbą „dziesięć”
Zestaw problemów wybranych przez OpenAI był celowo zróżnicowany i obejmował dziedziny, które w dużej mierze nie są ze sobą powiązane. Należą do nich geometria wielowymiarowa, teoria kodowania, teoria grup, algebry operatorów, kryptografia postkwantowa, złożoność obliczeniowa oraz kombinatoryka ekstremalna. Według firmy brano pod uwagę tylko te problemy, których główne kierunki badań praktycznie nie zmieniły się przez co najmniej dekadę. Innymi słowy, nie były to starannie dobrane „prezentacyjne” zadania mające na celu uzyskanie imponujących wyników, ale naprawdę trudne, otwarte problemy, które sama społeczność matematyczna uważa za poważne wyzwania.
Publicznie dostępne informacje opublikowane po ogłoszeniu wyników zawierają więcej szczegółów na temat osiągniętych rezultatów. Wśród nich jest obalenie hipotezy sztywności Connesa dotyczącej algebr von Neumanna, dowód hipotezy Ehrharta o objętości, rozwiązania kilku problemów ze słynnego zbioru Erdősa – w tym problemu wielokolorowych liczb Ramseya – pierwsze od prawie pół wieku ulepszenie górnej granicy gęstości upakowania sfer w przestrzeniach wielowymiarowych oraz nowe postępy w zakresie złożoności obliczeniowej wyznaczania stałej macierzy. Każdy z tych wyników to ważny kamień milowy w dziedzinie, w której znaczący postęp mierzy się zazwyczaj w latach żmudnej pracy małych grup specjalistów.
Przeczytaj też: Wszystko, co musisz wiedzieć o przeglądarkach AI: Głośny debiut, ciche zakończenie
Jak przebiegał ten proces: od wstępnych dowodów do formalnej weryfikacji
Być może najbardziej odkrywczym aspektem tej zapowiedzi jest metodologia stojąca za przedstawionymi wynikami. Według OpenAI model samodzielnie wygenerował argumenty matematyczne – w zasadzie wstępne dowody. Następnie naukowcy współpracowali z systemem, żeby dopracować te argumenty do postaci tradycyjnych artykułów naukowych, które nadają się do recenzji. Ostatnim i najważniejszym krokiem było sformalizowanie każdego dowodu w języku Lean – języku do dowodzenia twierdzeń, który pozwala komputerowi zweryfikować każdy krok logiczny z matematyczną dokładnością.
To kluczowa różnica w porównaniu z wcześniejszymi branżowymi twierdzeniami o „przełomach matematycznych” napędzanych przez AI. Dowód zweryfikowany w języku Lean to nie tylko kwestia zaufania do wyników modelu; to artefakt, który można odtworzyć. Każdy, kto ma dostęp do odpowiedniego oprogramowania, może samodzielnie potwierdzić, że ciąg rozumowania jest kompletny i pozbawiony luk logicznych. Z tego powodu OpenAI podkreśla, że autorstwo dowodów matematycznych nie jest przypisywane ludzkim badaczom, gdy podstawowa argumentacja została wygenerowana przez model. Rola badaczy polega na przygotowaniu pracy do publikacji i przełożeniu dowodów na ich formalną reprezentację w języku Lean.
Przeczytaj też: Planujesz kupić laptopa? Odpowiedz na te trzy pytania
Koszt tego przełomu – i dlaczego może to być najbardziej zaskakująca liczba
Być może najbardziej przełomowym aspektem tej wiadomości nie są same osiągnięcia matematyczne, ale podany koszt ich uzyskania. Według OpenAI łączna liczba tokenów potrzebnych do znalezienia rozwiązań wszystkich dziesięciu problemów kosztowałaby około 2 000 dolarów przy obecnych cenach API. Dla porównania, rozwiązanie problemów tej rangi w ramach tradycyjnych badań naukowych zazwyczaj wymaga lat pracy wyspecjalizowanych zespołów badawczych, wspieranych przez granty, konferencje i recenzje naukowe. Natomiast podany koszt obliczeniowy jest mniej więcej na poziomie tego, co jedna osoba mogłaby wydać na subskrypcje kilku serwisów internetowych w ciągu miesiąca. Jeśli te szacunki wytrzymają niezależną weryfikację, mogą one zasadniczo zmienić dotychczasowe założenia dotyczące ekonomiki badań matematycznych oraz roli sztucznej inteligencji w przyspieszaniu odkryć naukowych.
Ta liczba ma znaczenie nie dlatego, że sama w sobie dowodzi „genialności” modelu, ale dlatego, że może zmienić ekonomię badań naukowych. Jeśli koszt próby rozwiązania nietrywialnego, nierozwiązanego problemu spadnie do zaledwie kilku tysięcy dolarów, bariera dla eksperymentowania znacznie się obniży. To z kolei rodzi intrygujące pytanie: ile jeszcze długotrwałych problemów można by teraz zbadać tylko dlatego, że koszt podjęcia próby stał się stosunkowo niewielki?
Przeczytaj też: Anthropic zagląda do wnętrza sztucznej inteligencji: co tak naprawdę kryje się w przestrzeni J Claude’a
Astra wciąż pozostaje w cieniu
Mimo całego szumu wokół doniesień o jej osiągnięciach, sama Astra pozostaje prawie całkowicie nieprzejrzysta dla osób z zewnątrz. OpenAI nie ujawniło ani specyfikacji technicznych modelu, ani przewidywanego harmonogramu premiery, a jej miejsce w planie rozwoju produktów firmy wciąż nie jest jasne. Nie wiadomo, czy Astra stanie się kolejną wersją flagowego modelu OpenAI, czy pojawi się jako zupełnie nowa rodzina modeli, czy też będzie prekursorem przyszłej generacji flagowych systemów AI.
Ten brak informacji o samym modelu, w kontraście do szczegółowej prezentacji jego osiągnięć matematycznych, tylko potęguje intrygę. Zamiast debatować nad specyfikacjami technicznymi czy funkcjami produktu, dyskusja przesunęła się w stronę bardziej fundamentalnego pytania: co ten system faktycznie jest w stanie osiągnąć.
Przeczytaj też: Passkeys zamiast haseł: czy świat jest gotowy na nowy system uwierzytelniania?
Najważniejsze zastrzeżenie: kto weryfikuje weryfikatora?
Mimo że istnieją formalne dowody dotyczące Lean, warto spojrzeć na te twierdzenia z odpowiedniej perspektywy. Doniesienia o tych przełomach pochodzą od samego OpenAI – organizacji, która nie tylko opracowała ten model, ale też ma oczywisty interes w tym, by zaprezentować swoje osiągnięcia w jak najlepszym świetle. Formalna weryfikacja pokazuje, że dowód jest logicznie spójny, ale nie zastępuje oceny ze strony społeczności matematycznej. Naukowcy nadal muszą ocenić, czy wyniki są naprawdę nowatorskie, istotne z matematycznego punktu widzenia i eleganckie w szerszym kontekście ich dziedzin. Muszą też sprawdzić, czy proces tworzenia dowodów opiera się na założeniach lub uproszczeniach, które mogłyby ograniczyć praktyczną wartość tych wyników.
Z tego powodu kolejnym – i prawdopodobnie najważniejszym – etapem tej historii nie będzie kolejne ogłoszenie od OpenAI, ale niezależna ocena środowiskowa. Specjaliści z poszczególnych dziedzin matematyki ostatecznie zdecydują, czy te dziesięć wyników to prawdziwy postęp, który zasługuje na to, by stać się częścią standardowego dorobku tej dyscypliny, czy też pozostaną one intrygującym, ale ograniczonym do konkretnego kontekstu przykładem badań wspieranych przez sztuczną inteligencję.
Dopóki ten proces się nie zakończy, bardziej trafne będzie opisywanie ich jako rozwiązań, które OpenAI twierdzi, że znalazło, a nie jako ostatecznie rozwiązanych problemów. O ich ostatecznym znaczeniu zadecydują nie ci, którzy je ogłosili, ale naukowcy, którzy spędzili lata – a nawet dziesięciolecia – pracując nad tymi zagadnieniami.
Przeczytaj też: Jak urządzenia do noszenia i okulary z AI zmieniają logikę cywilizacji technologicznej
