Algorytmy wyłożyły się na zadaniach od matematyków. Nasz mózg wciąż wygrywa

Sztuczna inteligencja miała zrewolucjonizować matematykę. Miała rozwiązywać problemy, pisać dowody i przyspieszać badania naukowe. Najnowszy, bardzo wymagający test pokazał, że modele AI rzeczywiście robią postępy, jednak do poziomu najlepszych matematyków wciąż sporo im brakuje.

W projekcie First Proof sprawdzono 4 systemy AI na 10 niepublikowanych dotąd problemach z matematyki badawczej. To nie były szkolne zadania ani łamigłówki z Kangura Matematycznego, które można rozwiązać sprytnym trikiem. Chodziło o małe, techniczne twierdzenia wynikające z rzeczywistej pracy matematyków. Takie, które mogą być częścią większego dowodu albo przyszłej publikacji. I właśnie na takim gruncie maszyny zaczęły się potykać.

Większość popularnych benchmarków matematycznych sprawdza zadania konkursowe, końcowe odpowiedzi albo problemy, które łatwo ocenić automatycznie. First Proof działa zgoła inaczej. Matematycy z różnych dziedzin przygotowali problemy, które wcześniej nie były publicznie dostępne, nie trafiły do internetu i miały znane, ludzkie rozwiązania.

Modele AI uczą się na gigantycznych zbiorach tekstu. Jeśli zadanie albo podobny dowód krążył wcześniej w sieci, trudno powiedzieć, czy model naprawdę rozumuje, czy po prostu odtwarza coś, co wcześniej widział. W First Proof ten problem ograniczono bardzo mocno, bo zadania pochodziły z rzeczywistej pracy badawczej, a ich rozwiązania były nieopublikowane.

W drugiej turze testu było 10 zadań z takich obszarów jak teoria obliczalności, geometria dyskretna, prawdopodobieństwo, geometria metryczna, równania stochastyczne, teoria krat, topologia kombinatoryczna, matroidy, kombinatoryka algebraiczna i algebry von Neumanna. Wśród autorów jednego z problemów znalazł się również Dariusz Kalociński z Polskiej Akademii Nauk.

Najciekawsze jest jednak to, jak przeprowadzono cały eksperyment. Testowane systemy dostawały 10 problemów i musiały poradzić sobie z nimi za jednym podejściem, bez dodatkowych wskazówek, pytań pomocniczych czy rozmowy z człowiekiem. Każdy model otrzymywał zadania zapisane w LaTeX-ie i miał 24 godziny na przygotowanie pełnych rozwiązań.

Sprawdzano cztery podejścia. Wśród nich był samodzielny model ChatGPT 5.5 Pro oraz 3 akademickie systemy, które korzystały z publicznie dostępnych modeli przez API i próbowały poprawiać ich pracę za pomocą dodatkowego oprogramowania. Test nie dotyczył więc wyłącznie czystego chatbota, lecz także bardziej rozbudowanych zaprzęgów AI, które mają imitować pracę badawczą.

Potem przyszła część najważniejsza: ocena. 30 matematyków sprawdzało rozwiązania w trybie podobnym do recenzji naukowej. Każda odpowiedź była oceniana przez co najmniej dwóch ekspertów, a rozwiązania anonimizowano, żeby recenzenci nie wiedzieli, który system je wygenerował.

Modele wbrew pozorom wcale nie wypadły aż tak fatalnie. W całym teście 7 z 10 problemów doczekało się przynajmniej jednego rozwiązania ocenionego jako zasadniczo poprawne albo wymagające jedynie drobnych poprawek. Co więcej, w zadaniu dotyczącym równań stochastycznych jeden z systemów zaproponował poprawne rozwiązanie oparte na innym podejściu niż to, które zastosowali matematycy.

To brzmi imponująco. Tyle że po zajrzeniu w szczegóły entuzjazm trochę opada. Były zadania, przy których modele praktycznie utknęły w miejscu. Najlepiej widać to na problemie z geometrii metrycznej, gdzie nie udało się osiągnąć żadnego istotnego postępu. Zdarzały się też odpowiedzi, które na pierwszy rzut oka wyglądały bardzo profesjonalnie, ale po dokładniejszej analizie okazywało się, że omijają właśnie ten krok, który decydował o powodzeniu całego dowodu.

To właśnie było w tych wynikach najbardziej charakterystyczne. Modele bardzo dobrze radziły sobie z rutynową częścią pracy: rozpisywały definicje, budowały kolejne lemmy, wypełniały strony formalnymi wyprowadzeniami i sprawiały wrażenie, że wszystko jest pod kontrolą. Problemy zaczynały się wtedy, gdy trzeba było zrobić ten jeden naprawdę ważny krok i wpaść na właściwy pomysł. W takich momentach AI bardzo często uciekała po prostu w ogólniki, powoływała się na standardowy argument albo odsyłała do prac, które w rzeczywistości nie zawierały potrzebnego rozwiązania.

Matematyka nie działa na zasadzie brzmi sensownie, więc pewnie jest dobrze. Dowód albo jest poprawny, albo nie. Jeśli pojawi się w nim luka, błędne odwołanie czy nieuzasadniony przeskok, cały wywód może się posypać. Dlatego właśnie AI w matematyce jest jednocześnie tak fascynująca i tak problematyczna.

Modele potrafią pisać tak, jakby były pewne wyniku. Dla niespecjalisty, a czasem nawet dla matematyka z innej dziedziny, może to wyglądaj przekonująco. Problem zaczyna się wtedy, gdy ekspert zaczyna sprawdzać każde przejście. W First Proof recenzenci wielokrotnie widzieli odpowiedzi szczegółowe w miejscach łatwych i zadziwiająco mgliste tam, gdzie znajdował się rzeczywisty ciężar zadania.

W niektórych rozwiązaniach AI nawiązywała do istniejących prac, zapożyczyła sformułowania albo terminologię, ale nie podawała właściwych źródeł. Gdyby podobnie zrobił człowiek, to recenzenci mogliby potraktować to jako poważny problem akademicki. AI nie tylko rozwiązuje lub nie rozwiązuje zadania. Ona może też wytwarzać tekst, który wygląda naukowo, ale jest trudny do zaufania.

First Proof nie kończy się na tej edycji. Jeszcze w czerwcu rusza otwarty eksperyment dla społeczności, a na późniejsze miesiące zaplanowano kolejną formalną serię problemów. To pokazuje, że ten wyścig dopiero nabiera tempa. Modele będą coraz lepsze, a poprzeczka w kolejnych testach prawdopodobnie pójdzie jeszcze wyżej.

Przeczytaj także:

AI potrafi zrobić wrażenie, ale matematycy wciąż są lepsi tam, gdzie nie wystarczy dojść do odpowiedzi. Liczy się też rygor, intuicja i wyczucie tego, gdzie w dowodzie kryje się najtrudniejszy problem. Maszyna może wygenerować 12 stron eleganckiego LaTeX-a, ale ktoś nadal musi sprawdzić, czy te 12 stron faktycznie coś udowadnia.

*Grafika wprowadzająca wygenerowana przez AI