Dowód OpenAI rozwiązuje zadanie za milion dolarów zgodnie z literą. Matematycy pytali o coś innego

Rano 8 września OpenAI ogłosiło rozwiązanie jednego z najsłynniejszych problemów matematyki. Dowód przeszedł kontrolę programu sprawdzającego każdy krok rozumowania. Dziewięć dni później trzech matematyków opublikowało pracę, z której wynika, że ta metoda nigdy nie odpowie na pytanie, o które dziedzina pytała od początku. Oba zdania są prawdziwe naraz.

Chodzi o równania Naviera-Stokesa. Opisują ruch cieczy i gazów: wody w rurze, powietrza nad skrzydłem, krwi w naczyniach. Pytanie brzmi, czy gładki na początku przepływ może sam z siebie dojść do punktu z nieskończoną prędkością. Matematycy nazywają taki punkt osobliwością. W 2000 roku Instytut Matematyczny Claya umieścił to pytanie na liście siedmiu problemów milenijnych i wyznaczył za każdy milion dolarów nagrody.

Według opisu w Quanta Magazine OpenAI uruchomiło około 10 tysięcy agentów, czyli programów AI, które same wykonują kolejne kroki zadania i wymieniają się wynikami. Działały na wewnętrznym modelu, niedostępnym publicznie. Po 88 godzinach miały dowód osobliwości. Po kolejnych 17 godzinach inny model przełożył go na zapis w programie Lean.

Lean to program do sprawdzania dowodów. Nie ocenia, czy rozumowanie jest ładne albo przekonujące, tylko mechanicznie kontroluje każde przejście od jednego zdania do następnego. Jeśli Lean przyjmie dowód, twierdzenie w tej postaci jest prawdziwe. Jednej rzeczy program nie zrobi. Quanta przypomina, że człowiek musi jeszcze sprawdzić, czy udowodnione twierdzenie jest tym samym twierdzeniem, o które chodziło.

Oficjalny opis problemu napisał w 2000 roku Charles Fefferman z Princeton. Przewidział w nim kilka dróg do nagrody, a jedna z nich, oznaczona literą C, dopuszcza siłę działającą na ciecz z zewnątrz. W przyrodzie taką siłą jest na przykład grawitacja. W dowodzie OpenAI jest to siła dobrana z matematyczną precyzją tak, żeby przepływ się rozpadł.

Metodę budowania takiej siły rozwijali od kilku lat Diego Córdoba i Luis Martínez-Zoroa. Na ich pracy oparły się obie drużyny ogłaszające wyniki w odstępie dwunastu godzin. Pierwsi byli Tristan Buckmaster z Uniwersytetu Nowojorskiego i Levent Alpöge z Anthropic. Tuż przed północą 7 września podali rozwiązanie pokrewnego problemu dla cieczy bez tarcia. OpenAI ogłosiło swój wynik następnego ranka. Stąd trwający do dziś spór o pierwszeństwo.

17 września trzech matematyków opublikowało pracę z wnioskiem, że po usunięciu siły zewnętrznej osobliwość znika. Metody OpenAI nie da się więc przenieść na przypadek bez tej siły, a właśnie o nim myśli większość badaczy, gdy mówi o tym problemie. Scientific American opisał to 21 września pod tytułem pytającym, czy OpenAI rozwiązało nie ten problem.

Zasady nagród milenijnych są na stronie Instytutu Claya. Zanim instytut w ogóle zajmie się proponowanym rozwiązaniem, muszą zostać spełnione trzy warunki: publikacja w uznanym miejscu, co najmniej dwa lata od tej publikacji i powszechna akceptacja w światowym środowisku matematycznym. Pierwszy warunek zależy od redakcji czasopisma, drugi od kalendarza, trzeci od ludzi, którzy przez te dwa lata będą wynik czytać, podważać i porządkować.

To zestawienie tłumaczy, skąd bierze się nerwowość wokół całej sprawy. Maszynowe sprawdzenie poprawności zajęło 17 godzin. Rozstrzygnięcie, co ten wynik znaczy i komu należy się za niego zasługa, zajmie lata. Liczby z komunikatu firmy dotyczą wyłącznie tej pierwszej części.

18 września niezależny programista podpisujący się jako prinz ogłosił, że model GPT-6 Astra odczytał niemiecką depeszę radiową z końca listopada 1918 roku. Szyfr ADFGVX był w użyciu armii niemieckiej w ostatnim roku wojny. Depesza figurowała na prowadzonej przez Klausa Schmeha liście pięćdziesięciu najważniejszych nieodczytanych szyfrogramów.

Klucza nie trzeba było łamać. Słowo TRUPPENVERSCHIEBUNG, czyli „przesunięcie wojsk”, jest opisane w monografii J. Rivesa Childsa o niemieckich szyfrach z lat 1914–1918. Badacze przyjmowali jednak, że obowiązywało od 9 grudnia 1918, więc przy depeszy z listopada go nie próbowali. Model sprawdził założenie, że radiotelegrafista użył klucza wcześniej. Wyszła informacja o angielskim krążowniku w Sewastopolu 24. dnia miesiąca i o eskadrze aliantów płynącej 26. Według dzienników Royal Navy HMS Canterbury wszedł do Sewastopola 24 listopada 1918.

Niebezpiecznik zwraca uwagę na to, czego w tej historii brakuje: nie są znane pełne polecenia wydane modelowi, koszt jego pracy ani udział człowieka. Obie sprawy łączy jednak ta sama cecha. Model sprawdził wariant, który ludzie wcześniej odrzucili jako mało prawdopodobny. Przy depeszy odrzucony wariant okazał się prawdziwy i każdy może to potwierdzić w archiwum marynarki. Przy równaniu odrzucony wariant był dozwolony przez treść zadania, ale nie był tym, o co pytano.

21 września OpenAI powołało Grupę Doradczą do spraw Matematyki i Sztucznej Inteligencji przy Instytucie Studiów Zaawansowanych w Princeton. Zasiada w niej dziewięcioro matematyków: François Charles, Camillo De Lellis, Timothy Gowers, Martin Hairer, Nikhil Srivastava, Ulrike Tillmann, Ravi Vakil, Edward Witten i Melanie Matchett Wood. Nie biorą wynagrodzenia, mogą publikować opinie bez pytania firmy o zgodę i sami decydują o składzie grupy. Według AI Times OpenAI zastrzegło jednocześnie, że grupa nie doradza w sprawie tempa jego wewnętrznych prac.

Przy tej samej okazji firma podała, że jej nowy wewnętrzny model rozwiązał, poza problemem Naviera-Stokesa, ponad sto długo otwartych problemów z różnych działów matematyki. Listy tych problemów OpenAI nie opublikowało. Martin Hairer napisał na swoim blogu, jakie jest pierwsze zadanie grupy.

Grupa powstała dziesięć dni po deklaracji dwudziestu pięciu laureatów Medalu Fieldsa, w której zarzucono firmom AI ogłaszanie wyników w pośpiechu, bez opracowania i bez cytowania wcześniejszych prac. Sprawa Córdoby, Martíneza-Zoroi i Buckmastera jest dokładnie takim przypadkiem.