Matematycy sprawdzają nowość dowodów DeepMind

Matematyczny dowód może być elegancki, a mimo to kryć lukę, której nikt nie dostrzeże przez lata. Agent AI AlphaProof Nexus firmy Google DeepMind przygotował dowody dziewięciu problemów postawionych przez Paula Erdősa. Oprogramowanie sprawdziło każdy krok. Wyniki po raz pierwszy opisano w majowym preprincie (arXiv), a po recenzji naukowej opublikowano je 8 października w „Science” (Science). Program mógł potwierdzić poprawność rozumowania, ale o tym, czy dowody wnosiły coś nowego, musieli rozstrzygnąć matematycy.

Weryfikator, którego nie da się oczarować

Chatboty potrafią formułować matematyczne wywody, które brzmią przekonująco. Pewny siebie tekst może ukryć brakujący krok, który wychwyci dopiero uważny czytelnik. AlphaProof Nexus omija tę pułapkę, pracując w Lean — języku programowania pozwalającym precyzyjnie zapisywać definicje, twierdzenia i dowody, tak by komputer mógł sprawdzić ich poprawność.

Lean działa jak recenzent, który czyta gotowy dowód linijka po linijce i stosuje ustalone reguły. Styl nie ma znaczenia. Jeśli jeden krok nie wynika z poprzednich, dowód zostaje odrzucony, choćby reszta była elegancka.

Zespół opisuje agenta jako system wyszukujący dowody zapisane w Lean. Badacze udostępnili mu także AlphaProof, wcześniejszy system DeepMind stworzony specjalnie do dowodzenia twierdzeń. W testach prostszy układ dawał te same wyniki: model językowy połączony z Lean, bez AlphaProof, również uzyskał wszystkie dziewięć dowodów Erdősa (The Decoder). Przy tych problemach specjalistyczny system okazał się zbędny.

W artykule przedstawiono dowody dziewięciu twierdzeń Erdősa oraz 44 hipotez, czyli twierdzeń uznawanych za prawdziwe, ale dotąd nieudowodnionych, z Online Encyclopedia of Integer Sequences — obszernego katalogu ciągów liczb całkowitych (Science). Jeden z wyników dotyczy dwuczęściowego problemu o liczbach całkowitych, który Erdős i András Sárközy postawili w 1970 r. Przez ponad pół wieku pozostawał nierozwiązany (ABC).

Czego weryfikator nie widzi

Gwarancja Lean ma ściśle określony zakres: potwierdza, że dowód wykazuje dokładnie to, co zapisano w kodzie. Nie odpowiada na trzy pytania: czy kod oddaje intencję Erdősa, czy ktoś nie rozwiązał problemu wcześniej i czy wynik wnosi coś do matematyki.

Problem z 1970 r. pokazuje, dlaczego liczą się dwa ostatnie pytania. Jego druga część pociąga za sobą pierwszą, więc jeden dowód rozstrzyga obie. Gdy dowody agenta zaczęły krążyć wśród matematyków, okazało się, że niewielka modyfikacja konstrukcji z oryginalnej pracy z 1970 r. również rozwiązuje obie części (arXiv). Dowody agenta były poprawne. Problem okazał się po prostu bliższy rozwiązania, niż sugerowała etykieta „otwarty”.

Takie rzeczy mogą wychwycić ludzie znający daną dziedzinę. Gergely Bérczi, matematyk z Aarhus University w Danii i jeden z autorów pracy, pomagał dobierać odpowiednie problemy i oceniać rozwiązania (Aarhus University). Pomagał też przygotować wersje dowodów zrozumiałe dla ludzkich czytelników. Lean potwierdzał poprawność każdego kroku, a Bérczi i jego współpracownicy oceniali, co wynika z całości.

Ten podział pracy odróżnia badanie od osiągnięcia ogłoszonego miesiąc wcześniej. Wtedy Claude firmy Anthropic przepisał w Lean znany już dowód Wielkiego Twierdzenia Fermata (To Brief). W przypadku znanego dowodu nie ma wątpliwości co do nowości. Gdy system szuka rozwiązań problemów uznawanych za otwarte, sprawdzenie, czy wynik jest nowy, staje się kluczowym zadaniem.

Zespół udostępnił pliki z dowodami, więc inni mogą sprawdzić je w tym samym systemie (GitHub). Badanie pokazuje konkretną możliwość: agent AI wytworzył dowody sprawdzalne maszynowo dla części problemów uznawanych przez matematyków za otwarte, a gwarancja obejmuje te twierdzenia dokładnie w brzmieniu zapisanym w Lean. Ustalenie, co każdy dowód wniósł do matematyki, nadal należało do matematyków, którzy go czytali.