Sztuczna inteligencja Google rozwiązała zadania otwarte od 56 lat za kilkaset dolarów

System badawczy Google DeepMind stworzył kompletne, sprawdzone maszynowo dowody dla dziewięciu otwartych zadań postawionych przez matematyka Paula Erdősa, z których dwa pozostawały nierozwiązane od 56 lat. Ten sam system domknął 44 hipotezy zaczerpnięte z Internetowej encyklopedii ciągów liczb całkowitych, zamknął piętnastoletnie pytanie z geometrii algebraicznej i zacieśnił znane ograniczenie w optymalizacji wypukłej. Efektowna liczba znaczy mniej niż metoda. Każdy z tych dowodów został przez maszynę nie tylko postawiony, ale i zweryfikowany.

Erdős, zmarły w 1996 roku, zostawił setki precyzyjnych i upartych pytań, wiele z nich łatwych do sformułowania i potwornie trudnych do domknięcia. Przez dekady stały się rodzajem stałego egzaminu dla dziedziny. Hipotezy o ciągach pochodzą z publicznej bazy danych, którą matematycy przeszukują w poszukiwaniu wzorców i w której zgadnięty wzór potrafi latami leżeć bez dowodu. To nie są sztuczne testy stworzone, by schlebiać modelowi. To realne zaległości otwartej matematyki.

To rozróżnienie jest całą historią. System o nazwie AlphaProof Nexus zapisuje swoje argumenty w Lean, języku formalnym, którego kompilator odrzuca każdy krok, którego nie potrafi potwierdzić. Dowód albo przechodzi, albo nie, bez miejsca na pewny siebie akapit, który później okazuje się błędny. Dla kogoś, kto próbuje ocenić, czy „odkrycie” SI jest prawdziwe, to właśnie tu biegnie granica między komunikatem prasowym a wynikiem.

Pod spodem dowodzący działa na Gemini 3.1 Pro, a lżejszy model zajmuje się szeregowaniem. Pętla jest niemal nudna. Model szkicuje dowód w Lean, kompilator zwraca błędy, a te błędy zasilają kolejną próbę. To, co utrzymuje uczciwość, to sprzężenie symboliczne, nie płynna proza. Zespół zbudował cztery wersje o rosnącej złożoności, w tym jedną zdolną tworzyć i szeregować konkurujące szkice dowodów. A jednak najprostsza wersja, zwykła pętla z modelu i kompilatora, sama rozwiązała wszystkie dziewięć zadań Erdősa.

Cicho zdumiewa ekonomia. Każde rozwiązane zadanie kosztowało kilkaset dolarów czasu obliczeniowego. Pytania, które pochłonęły całe kariery, zamknięto mniej więcej za cenę weekendowego wypadu. To nie wysyła matematyka na emeryturę. Ktoś wciąż musi wybrać, które zadania warto atakować, ująć je w formie, którą system potrafi odczytać, i rozstrzygnąć, co znaczy odpowiedź. Zmienia się rachunek tego, co w ogóle warto spróbować.

Zastrzeżenia ważą więcej niż nagłówek. Dziewięć rozwiązanych z 353 próbowanych zadań Erdősa to skuteczność około 2,5 procent. Liczba z ciągów, 44 na 492, jest poniżej dziewięciu procent. Autorzy wprost przyznają, że większość tych zadań pozostaje poza zasięgiem, tym bardziej te wymagające rozległej nowej teorii, a sukcesy skupiają się tam, gdzie biblioteka matematyczna Lean jest już głęboka. Odbierz to zbudowane przez ludzi rusztowanie i wyselekcjonowaną listę celów, a systemowi zostaje niewiele gruntu.

Ostrożność jest zasłużona. W szeroko wyśmianym epizodzie konkurencyjne laboratorium ogłosiło, że jego model rozwiązał dziesięć zadań Erdősa, dopóki matematycy nie zauważyli, że odpowiedzi już figurowały w opublikowanej literaturze. Model je znalazł, a nie udowodnił. AlphaProof Nexus zbudowano tak, by był odporny na ten błąd. Dowód w Lean znanego wyniku wciąż jest ważnym dowodem, a dowodu w Lean czegoś naprawdę nowego nie da się zmyślić. Demis Hassabis, który kieruje DeepMind, zadbał o to, by powiedzieć, że ta praca nie jest ogólną sztuczną inteligencją, co jest nadzwyczaj ostrożną uwagą jak na firmę rzadko nieśmiałą wobec swoich modeli.

Jest subtelniejszy zysk, który podkreślają badacze. Pożytek przyniosły nawet porażki. Ponieważ każdy częściowy dowód jest sprawdzany formalnie, matematycy mogli dokładnie zobaczyć, które podcele system potrafił domknąć, a których nie, bez ręcznego przeglądania całego rozumowania. Maszyna przestaje być wyrocznią, a staje się niestrudzonym współpracownikiem, który pokazuje swoją pracę i wskazuje, gdzie wciąż kryje się trudna część.

Wynik nie stoi sam. Przypada na ten sam okres co osobne doniesienie o konkurencyjnym modelu rozumującym, który miał obalić około 80-letnią hipotezę Erdősa w geometrii dyskretnej, a ustalenie to czynni matematycy dopracowali i poparli. Dwa laboratoria, dwie metody, jedna oparta na weryfikacji formalnej, druga na surowych łańcuchach rozumowania, dotarły do tej samej granicy w odstępie tygodni. Rywalizacja nie dotyczy już chatbotów, które brzmią mądrze.

Pracę opisano w artykule opublikowanym w tym miesiącu, a metody opierają się na otwartych narzędziach, mianowicie na Lean i jego budowanej przez społeczność bibliotece, dzięki czemu grupy z zewnątrz mogą sprawdzić i ponownie przepuścić dowody, zamiast wierzyć firmowemu blogowi. DeepMind nie powiedział, czy system trafi do badaczy spoza firmy. Liczbą, którą warto śledzić, nie jest dziewięć. Chodzi o to, czy te 2,5 procent zmieni się w dziesięć, a potem w dwadzieścia, bo w dniu, w którym to nastąpi, spór o to, do czego służą te maszyny, będzie musiał zacząć się od nowa.