OpenAI publikuje 372 dowody matematyczne wygenerowane przez AI

OpenAI opublikowało na GitHubie zbiór 372 wyników matematycznych wygenerowanych przez wewnętrzny model AI, stawiając akademicki świat matematyki przed faktem dokonanym. Jak opisuje the-decoder.com, firma zamiast publikować wyniki w recenzowanych czasopismach, zdecydowała się udostępnić je w repozytorium na GitHubie wraz z logami zmian i cytowaniami, licząc na formalną weryfikację jako alternatywę dla tradycyjnej recenzji naukowej.

Kluczowe wnioski

• OpenAI opublikowało 372 nowe wyniki matematyczne wygenerowane przez wewnętrzny model frontierowy, mające rozwiązywać lub posuwać do przodu otwarte problemy matematyczne.
• Zbiór obejmuje m.in. usprawnienia dużych algorytmów komputerowych oraz postępy związane z hipotezą Riemanna.
• Niemal każdy wynik powstał z jednego promptu skierowanego do jednego agenta AI, choć niektóre wymagały kilku prób – to kontrast wobec wcześniejszego rozwiązania problemu Navier-Stokesa, które wymagało roju 10 000 agentów i milionów dolarów na obliczenia.
• Średnio każdy wynik „kosztował” około trzech godzin obliczeń na poziomie ChatGPT Pro Thinking.
• Grupa doradcza złożona z matematyków, w tym zdobywców Medalu Fieldsa, miała wpływ tylko na sposób komunikowania wyników – nie na to, czy i jak szybko są produkowane.

Weryfikacja formalna jako odpowiedź na skalę problemu

Wiele z opublikowanych dowodów zawiera formalizacje w języku Lean – systemie programistycznym zaprojektowanym do matematycznie sprawdzalnych maszynowo dowodów. OpenAI planuje kolejne formalizacje. Powód jest praktyczny: sama liczba wyników generowanych przez AI mogłaby łatwo przekroczyć zdolność środowiska matematycznego do ręcznej weryfikacji każdego z nich.

Firma opublikowała także szczegóły swojej metodologii, w tym podsumowania procesu rozumowania modelu, statystyki dotyczące liczby podjętych przez model problemów oraz szacunki kosztów obliczeniowych. Według OpenAI ten sam model wygenerował już wcześniej rozwiązanie problemu Navier-Stokesa, które od tygodni przechodzi formalną weryfikację.

GitHub zamiast czasopism naukowych

Decyzja o umieszczeniu wyników na GitHubie, a nie w recenzowanych czasopismach, jest odczytywana jako symboliczny gest – OpenAI daje do zrozumienia, że tradycyjny, powolny proces nauki nie jest w stanie nadążyć za tempem generowania potencjalnie nowej wiedzy.

OpenAI konsultowało się z Advisory Group on Mathematics and Artificial Intelligence działającą przy Institute for Advanced Study i w ogólnych zarysach uwzględniło jej publiczne rekomendacje – choć firma nie opublikowała żadnych promptów i podała tylko średnie, a nie jednostkowe koszty obliczeniowe dla poszczególnych problemów. W skład grupy wchodzi m.in. laureat Medalu Fieldsa Timothy Gowers oraz inni uznani matematycy.

Firma zadeklarowała również, że sfinansuje warsztaty i konferencje poświęcone zrozumieniu wyników generowanych przez AI. OpenAI przyznało, że chce poprawić jakość cytowań i sposobu prezentacji wyników, i twierdzi, że pracuje nad odpowiedzialnym udostępnieniem modelu, by „bezpośrednio wyposażyć naukowców w najnowocześniejsze możliwości”. Jednocześnie firma z góry wyznaczyła granicę dla grupy doradczej: matematycy mogą wpływać na to, jak komunikowane są wyniki, ale nie na to, czy i jak szybko są one produkowane.

Środowisko matematyczne podzielone wobec masowej produkcji dowodów

Formalizacje w Lean potwierdzają logiczną poprawność dowodu, ale nie są w stanie ocenić, czy dany wynik jest matematycznie istotny czy oryginalny. OpenAI stawia na to, że jego wyniki przesuwają granice ludzkiej wiedzy – czy środowisko matematyczne się z tym zgodzi, pozostaje otwartym pytaniem. Reakcje są mieszane, od entuzjazmu do frustracji.

W niedawnym otwartym liście pod tytułem „A Severe Misalignment of AI in Mathematics” 25 laureatów Medalu Fieldsa ostrzegło przed głębokim rozdźwiękiem między celami branży AI a celami matematyki. Rozwiązywanie problemów, jak napisali, jest jedynie narzędziem i miarą prawdziwego celu, którym jest konceptualne zrozumienie i wgląd. Masowe produkowanie prawdziwych stwierdzeń mogłoby zniszczyć podatny na rozwój gruntu, zamiast tworzyć nowe idee – a efekt ten mógłby rozlać się na inne dziedziny nauki.

Gowers ostrzegł, że w ciągu jednej lub dwóch dekad literatura matematyczna może rozrosnąć się ogromnie, podczas gdy nie będzie istniała żadna ludzka społeczność, która ją naprawdę rozumie. Laureat Medalu Fieldsa Terence Tao dodał, że kształcenie młodych matematyków musi kładzić nacisk na ludzki element nauki i ściśle ograniczać korzystanie z narzędzi AI, by prawdziwe uczenie się i rozumienie przetrwały.

Co dalej z masową produkcją dowodów przez AI

Spór wokół publikacji OpenAI pokazuje, że technologiczna zdolność do generowania setek matematycznych wyników wyprzedziła instytucjonalne i społeczne mechanizmy ich oceny. Pozostaje otwartą kwestią, czy formalna weryfikacja w Lean i konsultacje z doradcami wystarczą, by uspokoić obawy części środowiska naukowego, czy raczej tempo zmian narzuconych przez AI będzie dalej przyspieszać niezależnie od stanowiska matematyków.