Sztuczna inteligencja niezależnie zweryfikowała dowód jednego z najtrudniejszych problemów matematyki – problemu najgęstszego upakowania kul w przestrzeni wielowymiarowej – wyczyn ten przyniósł ukraińskiej matematyk Marinie Wiazowskiej Medal Fieldsa w 2022 r. Ten kamień milowy oznacza zasadniczą zmianę w sposobie prowadzenia badań matematycznych, przechodząc od sztucznej inteligencji jako zwykłego narzędzia obliczeniowego do współpracującego partnera w rozumowaniu.
Ewoluująca rola sztucznej inteligencji w matematyce
Przez stulecia matematycy korzystali z takich narzędzi, jak liczydła, kalkulatory i komputery, które pomagały w obliczeniach. Jednakże narzędzia te pozostały przedłużeniem ludzkiej inteligencji i nigdy nie zastąpiły podstawowego procesu rozumowania. Współczesne pojawienie się sztucznej inteligencji w matematyce jest zasadniczo odmienne: systemy te pomagają obecnie nie tylko w obliczeniach, ale także w samym wnioskowaniu, automatyzując wiele kroków leżących u podstaw argumentów matematycznych.
Ta zmiana następowała stopniowo. Współczesna matematyka opiera się już na złożonych strukturach i ogromnych katalogach wyników, których nikt nie jest w stanie w pełni zrozumieć. Komputery pomagały już w dużych dowodach, takich jak twierdzenie o czterech kolorach i hipoteza Keplera, ale dzisiejsze systemy sztucznej inteligencji oferują nowy poziom autonomii i niezawodności, zwłaszcza w połączeniu z formalnymi asystentami dowodu.
Siła formalnej weryfikacji
Języki weryfikacji formalnej, takie jak Lean, wyrażają argumenty matematyczne w sposób umożliwiający komputerom weryfikację każdego kroku, zapewniając logiczną ważność. W przeciwieństwie do tradycyjnego pisania matematycznego, Lean wymaga wyraźnych definicji i wniosków, dokładnie testując każdy krok. Choć jest to proces bezwzględny, eliminuje ukryte założenia i skoki wiary. Wynik jest wyznaczany matematycznie, pod warunkiem, że dowód przejdzie test Lean.
W ciągu ostatnich kilku lat matematycy zbudowali ogromne biblioteki w tych językach, gromadząc definicje i sprawdzone twierdzenia, aby rozwiązywać coraz bardziej złożone problemy. Wcześniej wąskim gardłem był pracochłonny proces przekształcania najnowocześniejszych dowodów w formę możliwą do sprawdzenia maszynowego, co mogło zająć miesiące lub lata.
Przełom: dowód Wiazowskiej, zweryfikowany przez sztuczną inteligencję
Niedawna weryfikacja dowodu problemu najgęstszego upakowania kul w wielowymiarowej przestrzeni Wiazowskiej pokazuje szybki postęp w tej dziedzinie. Problem najgęstszego upakowania kul dotyczy tego, jak gęsto identyczne kule mogą być upakowane w przestrzeniach o dowolnym wymiarze. Wiazowska rozwiązała ten problem dla ośmiu i 24 wymiarów, opierając się na pracy, która została wcześniej wykonana tylko dla jednego, dwóch i trzech wymiarów.
Startup AI Math, Inc., korzystając ze swojego agenta wnioskowania Gaussa, odegrał kluczową rolę w przetłumaczeniu argumentów Wiazowskiej na kod Lean i walidacji każdego kroku. System sztucznej inteligencji nie działał w izolacji: matematycy zapewnili wstępny projekt i strukturę. Jednak po skonfigurowaniu Gauss wykonał zadanie w ciągu kilku dni – zadanie, które według szacunków badaczy zajęłoby miesiące.
Przyszłość badań matematycznych
To coś więcej niż osiągnięcie techniczne; sygnalizuje to zasadniczą zmianę w sposobie pracy matematyków. Medalista Fieldsa, Terence Tao, sugeruje, że bezpośrednia wartość sztucznej inteligencji polega na automatyzacji żmudnych, ale koncepcyjnie prostych zadań, dzięki czemu matematycy mogą skupić się na strategii, a nie na rachunkowości. Kluczowe znaczenie ma oddzielenie generowania kreatywnych pomysłów od rygorystycznych testów.
Kevin Buzzard z Imperial College London przestrzega przed poleganiem na nieprzetestowanych dużych modelach językowych, twierdzi jednak, że rozwiązaniem są języki weryfikacji formalnej, takie jak Lean. Jeśli dowód przejdzie program, ma gwarancję ważności. Głównym wyzwaniem jest obecnie przełożenie dużej części współczesnej matematyki na te formalne biblioteki, co zapewni systemom AI niezbędne koncepcje do pracy.
Wniosek
Sztuczna inteligencja nie zastępuje matematyków, ale na nowo definiuje ich rolę. Przyszłość matematyki będzie prawdopodobnie polegać na tworzeniu i dostrajaniu narzędzi przesuwających granice poznawcze człowieka, łączących intuicję z dyscypliną maszynową. W miarę rozwoju sprawdzalnej matematyki będzie większe zapotrzebowanie na ludzi, którzy potrafią zadawać właściwe pytania, tworzyć nowe definicje i rozpoznawać prawdziwe pomysły. Partnerstwo między ludzką inteligencją a sztuczną inteligencją pobudzi nową erę odkryć matematycznych.
