OpenAI pokazał 722 prace matematyczne swojego modelu. Komputer sprawdził główny wynik w 162

OpenAI opublikował 6 października zbiór 722 prac matematycznych, które według firmy napisał jej wewnętrzny, jeszcze niewydany model AI. Zapowiedź jest na blogu OpenAI, a same prace leżą w publicznym repozytorium openai/math na GitHubie. Dla użytkowników ChatGPT nic się dziś nie zmienia: modelu, który to zrobił, nie ma w aplikacji ani w API. OpenAI pisze, że pracuje nad jego odpowiedzialnym udostępnieniem, i nie podaje daty.

Co jest w zbiorze

Prace są podzielone na 372 „rodziny”, czyli grupy tekstów wokół jednego wyniku, z dowodami pomocniczymi i alternatywnymi. Według opisu repozytorium model dostał w czasie testów około 4000 problemów. Przeciętny wynik kosztował tyle obliczeń, ile trzy godziny myślenia modelu w ChatGPT Pro. OpenAI zaczął dawać modelowi otwarte problemy badawcze, bo na dotychczasowych testach matematycznych wyniki doszły do sufitu.

Co	Liczba
Prace w zbiorze	722
Rodziny wyników	372
Problemy postawione modelowi	ok. 4000
Prace z dowodem głównego wyniku sprawdzonym w Lean	162
Streszczenia rozumowania modelu	10
Przeciętny koszt jednego wyniku	ok. 3 godziny myślenia w ChatGPT Pro

Liczbę 162 policzyliśmy z katalogu formalizacji w repozytorium, który wymienia prace z formalnie sprawdzonym głównym wynikiem.

Jakie problemy model miał rozwiązać

Na liście są twierdzenia i hipotezy znane z nazwy. W przeglądzie zbioru OpenAI podaje między innymi dowód, że stała Catalana jest liczbą niewymierną, czyli nie da się jej zapisać jako ułamka. Inna praca rozstrzyga dziesiąty problem Hilberta dla liczb wymiernych: nie ma algorytmu, który dla każdego równania wielomianowego powie, czy ma ono rozwiązanie w ułamkach. Jeszcze inna podaje, że wykładnik niewymierności liczby pi wynosi dokładnie 2. To mówi, jak dobrze pi da się przybliżać ułamkami.

To są deklaracje producenta. Źródło nie podaje recenzji niezależnych matematyków, a opis repozytorium sam ostrzega, że wyniki bez formalizacji mogą mieć błędy.

Co znaczy „sprawdzone w Lean”

Lean to język programowania, w którym dowód zapisuje się tak, żeby komputer mógł sprawdzić każdy krok. Taki dowód ocenia program, a nie recenzent, który w długim wywodzie może coś przeoczyć. W katalogu formalizacji jest na przykład praca o tak zwanej quasi-hipotezie Riemanna, czyli o tym, gdzie nie mogą leżeć zera funkcji dzeta i jej pokrewnych. Trzech przykładów z poprzedniego akapitu w tym katalogu nie ma. Sam katalog ma opis „częściowy postęp”, a OpenAI zapowiada, że będzie dokładać kolejne formalizacje.

Jeśli przeczytasz gdzieś, że AI „udowodniło” któreś z tych twierdzeń, sprawdź w repozytorium, czy praca ma formalizację w Lean. Bez niej wynik czeka na matematyków.

Co dalej

Przy publikacji OpenAI radził się niezależnej grupy doradczej do spraw matematyki i AI przy Institute for Advanced Study. Firma zapowiada też finansowanie warsztatów i konferencji o wynikach uzyskanych przez AI. Poprawki prac mają wychodzić jako nowe wersje, a starsze zostaną dostępne.

Dwa wyniki powstały inną drogą niż reszta: obszar bez zer funkcji dzeta Riemanna i hipoteza Hodge'a dla rozmaitości abelowych typu CM. Opis jednego z wyników o funkcji dzeta zredagował dla czytelności człowiek.

Podobne prace pokazywał ostatnio Anthropic: fizyk Matthew Schwartz napisał z Claude'em 36 prac naukowych, a Claude Fable 5.1 policzył dziewięć pętli w fizyce cząstek. OpenAI nie podał, jak będzie się nazywał model od matematyki ani kiedy trafi do ChatGPT.