Matematycy coraz głośniej pytają, na ile można ufać 719 matematycznym manuskryptom wygenerowanym przez OpenAI, po tym jak w nowej publikacji wykazano, że wcześniejszy dowód Naviera–Stokesa nie pokrywa się z jego wersją formalnie zweryfikowaną w systemie Lean.
Najważniejsze ustalenia:
- Katalog OpenAI skurczył się z 722 do 719 manuskryptów po wycofaniu trzech prac z powodu błędu znaku.
- Trzech matematyków z brytyjskich uczelni 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.
Publikacja zestawu dowodów OpenAI
OpenAI udostępniło kolekcję 6 października, a raport opublikowany w czwartek wskazał, że projekt odbiega od wytycznych opracowanych dla laboratoriów AI przez niezależny panel matematyków. Katalog startował z 722 manuskryptami. OpenAI wycofało trzy z nich dzień później po tym, jak błąd znaku podważył jedno z rozumowań, a wraz z nim dwie prace na nim oparte.
Wytyczne te, opublikowane 29 września przez dziewięcioosobową Advisory Group on Mathematics and Artificial Intelligence, zaczynają się od apelu, by laboratoria przestały testować zaawansowane problemy matematyczne na zastrzeżonych modelach. Repozytorium OpenAI informuje, że prace powstały w wyniku ewaluacji nieudostępnionego jeszcze wewnętrznego modelu na otwartych problemach badawczych.
Szczegółowe 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 pozwalającym komputerowo sprawdzić poprawność dowodu.
Zobacz także: Ile zarabia prezes Anthropic? Prospekt emisyjny 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. Zidentyfikowali dwa miejsca, w których wersja „papierowa” i kod w Lean się rozchodzą – w tym jedno, gdzie kod dowodzi słabszego oszacowania, niż to zadeklarowane w pracy.
Autorzy podkreślają, że nie wypowiadają się co do prawdziwości samego, spisanego dowodu. Ich teza jest węższa: Lean potwierdza prawdziwość twierdzenia końcowego, ale nie jest w stanie zagwarantować, że każdy pośredni krok, który czyta człowiek, jest poprawny. Takie konstrukcje nadal wymagają klasycznej recenzji naukowej.
Laureat Medalu Fieldsa Terence Tao zwrócił uwagę 6 października, że problemy są dziś rozwiązywane przez „prompterów AI”, którzy nie rozumieją wyników na tyle dobrze, by odpowiadać na pytania czy prezentować je na seminariach. Profesor Harvardu Melanie Matchett Wood, członkini grupy doradczej, zauważyła, że w momencie publikacji „nikt z ludzi tak naprawdę nie rozumie tych rezultatów – i dopiero wtedy zaczyna się prawdziwa praca”.
Spór o dowód OpenAI
Grupa doradcza podkreśla, że jedynie szersza społeczność matematyczna jest w stanie ocenić, jak ściśle OpenAI stosuje się do jej zaleceń. Ta weryfikacja odbywa się po burzliwym miesiącu. OpenAI ogłosiło wynik dotyczący Naviera–Stokesa 8 września, co wywołało spór o autorstwo z matematykiem z New York University, Tristanem Buckmasterem, a trzy dni później 25 laureatów Medalu Fieldsa ogłosiło deklarację ostrzegającą, że masowa produkcja wyników przez AI może zaszkodzić rozwojowi dyscypliny.
Czytaj dalej: OpenAI udostępnia 722 matematyczne prace AI. Teraz matematycy muszą je ocenić
