OpenAI opublikowało 722 rękopisy matematyczne. Wąskim gardłem stała się weryfikacja

OpenAI opublikowało 722 rękopisy matematyczne pogrupowane w 372 rodziny wyników. Powstały podczas ewaluacji około 4 000 otwartych problemów, a firma podaje średni budżet obliczeniowy odpowiadający mniej więcej 3 godzinom trybu ChatGPT Pro na wynik. Dla matematyki liczy się zarówno liczba tekstów, jak i tempo, w jakim wewnętrzny model je przygotował.

Jedna ewaluacja przyniosła pakiet 722 rękopisów

Publiczne repozytorium zawiera prace, pomocnicze materiały dowodowe oraz formalizacje w Lean. Źródłowy przegląd Zvi Mowshowitza przedstawia wydarzenie jako rozwiązanie 90 z 500 ważnych otwartych problemów. Samo repozytorium stosuje dokładniejszy podział na 722 rękopisy w 372 powiązanych rodzinach, a nie jeden ranking trudności.

OpenAI udostępniło też 10 skróconych opisów rozumowania modelu. Sam model pozostaje wewnętrzny. Badacze mogą analizować teksty i część formalnych artefaktów, lecz nie mogą odtworzyć całego procesu na tym samym systemie.

Produkcja dowodów wyprzedziła możliwości ich czytania

Badania matematyczne ograniczała dotąd zarówno zdolność znalezienia dowodu, jak i czas potrzebny na jego zrozumienie, sprawdzenie oraz osadzenie w literaturze. Zbiór 722 rękopisów zmienia proporcję między liczbą potencjalnych wyników a liczbą ekspertów, którzy mogą je odpowiedzialnie ocenić.

Skutek praktyczny wykracza więc poza pytanie, czy przetrwa jeden konkretny dowód. Laboratoria będą musiały finansować formalizację, niezależną kontrolę i jasne objaśnienia równie poważnie jak samo generowanie. W przeciwnym razie szybsze odkrywanie stworzy jedynie dłuższą kolejkę nierozstrzygniętych twierdzeń.

Lean obejmuje tylko część opublikowanego zbioru

Według publicznego katalogu 162 z 722 rękopisów ma sformalizowany główny wynik. Jakikolwiek materiał Lean dołączono do 235 z 372 rodzin, co nie oznacza pełnej formalnej weryfikacji każdej pracy. Lean sprawdza też podane twierdzenie formalne. Sam nie ustala, czy dokładnie odpowiada ono tekstowi nieformalnemu, czy wynik jest nowy ani jak duże ma znaczenie.

Część niesformalizowanych wyników może zawierać błędy, a cały zbiór nie przeszedł zwykłego procesu recenzji. Opowieść o natychmiastowym przełomie historycznym jest przedwczesna, choć skali publikacji i liczby sprawdzalnych artefaktów nie da się sprowadzić do produktowego pokazu.

O znaczeniu przesądzą niezależne poprawki i ponowne użycie

Najważniejszym sygnałem będzie publiczna historia rewizji: ile głównych twierdzeń potwierdzą niezależni matematycy, ile trzeba będzie poprawić i ile znajdzie zastosowanie w kolejnych pracach. Równie ważne będzie uzupełnienie formalizacji, pełniejszych zapisów procesu oraz dostępu do modelu, który pozwoli oddzielić możliwości systemu od selekcji udanych wyników.

Jeżeli w najbliższych miesiącach rezultaty staną się cytowanymi dowodami i nowymi narzędziami, zmieni to organizację badań. Jeżeli większość zbioru pozostanie nieprzeczytana, publikacja pokaże przede wszystkim, że matematyka potrafi już produkować twierdzenia szybciej, niż potrafi je przyswajać.

Werdykt Lilith

OpenAI wysłało matematykom 722 zapieczętowane paczki, a skaner dołączyło tylko do części z nich. Historyczny moment zacznie się wtedy, gdy niezależni badacze naprawdę je otworzą, sprawdzą i wykorzystają.