Matematycy coraz głośniej pytają, na ile można ufać 719 manuskryptom matematycznym wygenerowanym przez OpenAI, po tym jak nowa publikacja wykazała, że wcześniejszy dowód Naviera-Stokesa przedstawiony przez firmę nie odpowiada swojej wersji formalnie zweryfikowanej w systemie Lean.
Kluczowe ustalenia:
- Katalog OpenAI skurczył się z 722 do 719 manuskryptów po wycofaniu trzech prac z powodu błędu znaku.
- Trzech matematyków z Wielkiej Brytanii opisało dwa miejsca, w których pisemny dowód Naviera-Stokesa i jego kod w Lean się rozchodzą.
- Autorzy nie twierdzą, że dowód jest błędny, ale podkreślają, że weryfikacja maszynowa nie zastępuje recenzji naukowej.
Premiera pakietu dowodów OpenAI
OpenAI opublikowało kolekcję prac 6 października. Raport opublikowany w czwartek wykazał, że projekt odbiega od wytycznych przygotowanych przez niezależny panel matematyków dla laboratoriów zajmujących się AI. Katalog ruszył z 722 manuskryptami. Dzień później OpenAI wycofało trzy z nich, po tym jak błąd znaku unieważnił jedno z rozumowań oraz dwie prace, które się na nim opierały.
Wytyczne te, opublikowane 29 września przez dziewięcioosobową Advisory Group on Mathematics and Artificial Intelligence, zaczynają się od apelu, by laboratoria zaprzestały testowania zaawansowanych problemów matematycznych na zastrzeżonych modelach. Repozytorium OpenAI informuje, że manuskrypty powstały podczas ewaluacji nieopublikowanego wewnętrznego modelu na otwartych problemach badawczych.
Opisy rozumowania modelu dołączono jedynie do 10 wyników, a około 42% najważniejszych rezultatów zostało sformalizowanych w Lean – języku programowania, który pozwala komputerowo sprawdzić poprawność dowodu.
Przeczytaj także: Ile zarabia prezes Anthropic? Prospekt IPO ujawnia szczegóły
Luki w dowodzie Naviera-Stokesa
Alexander Bastounis z King's College London oraz Fabian Circelli i Anders Hansen z University of Cambridge przeanalizowali dowód Naviera-Stokesa, który OpenAI ogłosiło we wrześniu. Udokumentowali dwa miejsca, w których wersja napisana w artykule i wersja w Lean się rozmijają – w tym jedno, gdzie kod dowodzi jedynie słabszego oszacowania, niż deklaruje tekst pracy.
Autorzy podkreślają, że nie przesądzają, czy pisemny dowód jest ostatecznie poprawny. Ich teza jest węższa: Lean potwierdza, że finalne twierdzenie rzeczywiście zachodzi, ale nie jest w stanie wykazać, że wszystkie pośrednie kroki, które czyta człowiek, są logicznie bez zarzutu. Tego typu prace nadal wymagają pełnej recenzji środowiska.
Laureat Medalu Fieldsa Terence Tao napisał 6 października, że kolejne problemy są rozwiązywane przez „propmterów AI”, którzy nie rozumieją wyników na tyle dobrze, by odpowiadać na szczegółowe pytania czy wygłaszać o nich referaty. Profesor Harvardu Melanie Matchett Wood, członkini grupy doradczej, zauważyła, że w momencie publikacji nikt z ludzi w pełni nie rozumie takich rezultatów „i dopiero wtedy zaczyna się prawdziwa praca”.
Spór o dowód OpenAI
Grupa doradcza podkreśla, że jedynie szeroka społeczność matematyków może ocenić, jak ściśle OpenAI zastosowało się do jej zaleceń. Ta wzmożona kontrola przychodzi po napiętym miesiącu. OpenAI ogłosiło wynik dotyczący Naviera-Stokesa 8 września, co natychmiast wywołało spór o autorstwo z matematykiem z New York University, Tristanem Buckmasterem. Trzy dni później 25 laureatów Medalu Fieldsa opublikowało deklarację ostrzegającą, że masowa produkcja wyników generowanych przez AI może zaszkodzić rozwojowi dyscypliny.
Czytaj dalej: OpenAI udostępniło 722 matematyczne prace AI. Teraz matematycy muszą je ocenić
