OpenAI: 722 prace z matematyki. Problemy za milion dolarów otwarte

6 października OpenAI opublikowało 722 prace matematyczne napisane przez swój niewydany model. Część z nich dotyka trzech problemów, za które amerykański Instytut Matematyczny Claya wyznaczył po milion dolarów nagrody: hipotezy Riemanna, hipotezy Hodge'a i hipotezy Bircha i Swinnertona-Dyera. Żadnego z trzech nie rozwiązano w całości.

Tak wynika z opisu każdej rodziny wyników w spisie repozytorium OpenAI na GitHubie i z opisów problemów na stronie Instytutu Claya. Tam wszystkie trzy mają nadal status »Unsolved«. Rodzina to główny dowód z pracami towarzyszącymi. Model dostał w trakcie prac około 4000 problemów. Przeciętny wynik zużył według firmy tyle mocy obliczeniowej, co trzy godziny myślenia modelu w płatnym planie ChatGPT Pro.

Najgłośniejsza praca dotyczy hipotezy Riemanna, czyli pytania o rozmieszczenie liczb pierwszych. W uproszczeniu hipoteza mówi, że pewna funkcja, zwana dzetą Riemanna, nie ma miejsc zerowych na prawo od pionowej linii 1/2. Model OpenAI udowodnił, że nie ma ich na prawo od linii 7/8. Pas między 1/2 a 7/8 zostaje otwarty. Matematycy nazywają taki słabszy wynik quasi-hipotezą Riemanna. To jedyny z trzech wyników z dowodem w Lean.

Dwa pozostałe przypadki są węższe. Hipoteza Hodge'a dotyczy kształtów opisanych równaniami algebraicznymi, a prace OpenAI obejmują wybrane klasy takich kształtów. Instytut Claya sam zaznacza, że hipoteza była już znana w niektórych przypadkach szczególnych. Przy hipotezie Bircha i Swinnertona-Dyera, o rozwiązaniach równań krzywych eliptycznych, dowód obejmuje tylko krzywe spełniające jeden techniczny warunek. Obie rodziny wyników nie mają w spisie odnośnika do dowodu w Lean. OpenAI zaznacza w repozytorium, że prace przy Riemannie i Hodge'u powstały poza zwykłą procedurą. Opis jednego z dowodów przy Riemannie redagował człowiek.

Lean to program, w którym dowód zapisuje się tak, żeby komputer skontrolował każde przejście od zdania do zdania. Odnośnik do takiego dowodu ma 235 z 372 rodzin wyników, około dwóch trzecich. Reszta ma sam tekst. OpenAI samo pisze w repozytorium, że część prac bez formalizacji może zawierać błędy.

Katalog dowodów w Lean opisuje zakres jako »Partial progress«, czyli postęp częściowy. Pole przeglądu ma wartość »unchecked«. Lean potwierdza, że dowód pasuje do zapisanego twierdzenia, ale zgodność zapisu z pytaniem matematyków musi ocenić człowiek. W nowej publikacji Navier-Stokes ma jedną rodzinę, o przepływach sterowanych siłą z zewnątrz.

Levent Alpöge, matematyk z Anthropic, konkurenta OpenAI, napisał, że to najważniejszy moment w historii matematyki, i wyróżnił właśnie quasi-hipotezę Riemanna. Spór dotyczy trybu. Andrew Sutherland z Massachusetts Institute of Technology (MIT) chce traktować zapewnienie OpenAI, że wyniki dał jeden agent za jednym podejściem, jako niepotwierdzone, dopóki model nie będzie dostępny, a wyników nie da się odtworzyć. OpenAI dołączyło skrócone zapisy rozumowania modelu dla 10 rodzin z 372.

11 września laureaci Medalu Fieldsa, najważniejszej nagrody w matematyce, zarzucili w deklaracji firmom AI ogłaszanie wyników w pośpiechu, bez porządnego opracowania i cytowania cudzych prac. Przed obecną publikacją OpenAI radziło się grupy doradczej matematyków przy Instytucie Studiów Zaawansowanych, ośrodku badawczym w USA. Publikacja wyszła 25 dni po deklaracji.

Regulamin nagród Claya stawia trzy warunki. Rozwiązanie musi wyjść w uznanym piśmie, zdobyć powszechną akceptację matematyków i przeczekać co najmniej dwa lata od publikacji, zanim instytut w ogóle je rozpatrzy.