OpenAI twierdzi, że tajny model AI rozwiązał setki otwartych problemów matematycznych za jednym promptem — matematycy chcą dowodów

OpenAI opublikowało 722 manuskrypty matematyczne na GitHubie we wtorek, wszystkie wygenerowane przez model wewnętrzny, którego firma nie wydała. Rzecznik OpenAI powiedział, że prawie wszystko pochodziło z jednego promptu przekazanego pojedynczemu agentowi AI, choć niektóre mogły wymagać wielu prób.

To śmiałe twierdzenie i potencjalnie przełomowe osiągnięcie w dziedzinie matematyki. Ale nie wszyscy są fanami ani nie kupują tego hype'u.

„Dopóki nie udostępnią modelu i ludzie nie będą mogli odtworzyć ich wyników, uważam, że wszelkie twierdzenia o rozwiązywaniu problemów za jednym razem przy użyciu pojedynczego agenta należy traktować jako niezweryfikowane” – Andrew Sutherland, matematyk z MIT, powiedział Scientific American. „Powinniśmy poprosić o dowody” – stwierdził.

Prace są pogrupowane w 372 „rodziny” powiązanych wyników, a rodzina może łączyć główne twierdzenie z towarzyszącymi argumentami, konsekwencjami lub alternatywnymi dowodami. To sprawia, że 722 to liczba manuskryptów, a nie rozwiązanych problemów. OpenAI twierdzi, że przedstawiło modelowi około 4000 problemów i zachowało wyniki, które uznało za wystarczająco istotne, by je opublikować.

Przeciętny wynik wykorzystywał równowartość około trzech godzin obliczeń myślowych ChatGPT Pro, według OpenAI. Zeszłomiesięczne twierdzenie dotyczące Naviera-Stokesa wyglądało zupełnie inaczej, z 10 000 koordynujących agentów pracujących przez 88 godzin.

OpenAI udostępniło skrócone podsumowania rozumowania dla 10 wyników. Jednak według katalogu formalizacji w repozytorium tylko 162 z 722 prac zawierają główny wynik sprawdzony komputerowo. Stanowi to około 22% kolekcji, przetłumaczonej na Lean, oprogramowanie, które mechanicznie sprawdza każdy krok logiczny.

Sam OpenAI przyznaje, że nie wszystkie manuskrypty mają formalizacje w Lean i że „niektóre nieformalne wyniki mogą mieć problemy”. Innymi słowy, wiele z tego, co opublikowali, może być błędne.

Pozytywna weryfikacja w Lean potwierdza jedynie, że dowód wynika z twierdzenia zapisanego w Lean. To nie oznacza, że twierdzenie odpowiada oryginalnemu problemowi ani że wynik jest nowy lub ważny – to właśnie musi ocenić matematyk.

I tu właśnie badacze podnoszą brwi.

„Mamy teraz do czynienia z sytuacją, w której AI może generować argumenty matematyczne w okolicznościach, gdy człowiek, który je zainicjował, nie jest w stanie ich zrozumieć, zweryfikować ani wziąć za nie odpowiedzialności” – stwierdził w oświadczeniu Instytut Studiów Zaawansowanych w Princeton w New Jersey. „Uważamy, że ludzkie rozumienie matematyki pozostaje sprawą najwyższej wagi. Jak w tej nowej erze możemy pracować na rzecz nowego paradygmatu, który uwzględnia ludzkie rozumienie matematyki jako część odpowiedzialnego dorobku naukowego?”

Inni jednak, jak profesor Abhishek Saha, są całkiem podekscytowani. „To bardzo ważny dzień dla matematyki” – napisał, ale zauważył, że większość problemów mieści się w kategoriach „wyjątkowych postępów w ramach istniejącego programu” lub „zaskakujących przełomów”.

Oznacza to, że większość problemów w zestawie jest interesująca, ale nie niemożliwa ani przełomowa jak problemy milenijne. To miejsce jest zarezerwowane dla dokładnie jednego problemu spośród 722: quasi-hipotezy Riemanna.

Wydanie to również nie spełnia tego, co grupa doradcza w Institute for Advanced Study zaleciła 29 września: nazwy modelu, promptów, podsumowanego łańcucha myśli, czasu potrzebnego oraz kosztu obliczeniowego dla każdego wyniku. OpenAI opublikowało średnie wartości obliczeń i 10 podsumowań rozumowania, ale nie opublikowało promptów, i twierdzi, że wciąż pracuje nad odpowiedzialnym udostępnieniem modelu.

Daniel Litt, matematyk z University of Toronto, zajął przeciwne stanowisko, argumentując, że nie ma powodu, by prosić firmę o utrzymywanie odpowiedzi na te pytania matematyczne w tajemnicy.

Anthropic poszło inną drogą ze swoim zweryfikowanym przez Lean dowodem Wielkiego Twierdzenia Fermata w zeszłym miesiącu, publikując publicznie wszystkie 13 milionów linii na GitHubie. Ten dowód sformalizował twierdzenie opublikowane przez Andrew Wilesa w 1995 roku, a nie roszczenie sobie prawa do nowych wyników.

OpenAI twierdzi, że będzie dodawać formalizacje Lean w miarę ich uzyskiwania; na razie 162 z 722 manuskryptów ma taką formalizację.