Matematycy nigdy nie byli tak poszukiwanymi osobami przez najbogatszych ludzi na świecie. Na uniwersytetach na całym świecie akademicy obserwują tajemnicze znikanie ich kolegów, którzy dołączają do prywatnych firm. Niektóre z tych firm to znane nazwy, jak OpenAI i Google, ale inne są nowo powstałe i zaledwie kilku miesięcy stare, mając nadzieję skorzystać z chwili, w której matematyka jest uważana za tajny składnik, który poprawi sztuczną inteligencję – co z kolei może odmienić samą matematykę.
„“W zeszłym roku maja, naprawdę żałowałem mojej tożsamości naukowej” – mówi Ken Ono, który w 2025 roku wystąpił z profesury na Uniwersytecie Wirginii, aby dołączyć do Axiom Math, start-upu mającego na celu budowę sztucznej inteligencji skupionej na matematyce.
Ono został poproszony przez inną firmę, o nazwie Epoch AI, o pomoc w stworzeniu zestawu trudnych do rozwiązania problemów matematycznych, które miałyby testować zdolności rozwiązywania problemów przez SI. Ale gdy poddał te SI próbom, zdał sobie sprawę, że są one o wiele zdolniejsze, niż sobie wyobrażał. „Po kilku miesiącach takiej pracy, zdałem sobie sprawę, że może to być ten moment, kiedy dzierżawca spotyka samochód z silnikiem spalinowym na polu i myśli, że może zrobimy więcej, przyjmując te technologie” – mówi Ono.
Świadomość Ono nie była wyjątkowa: Axiom Math to jedna z serii firm założonych w ciągu ostatnich dwóch lat, które mają na celu budowę SI, która nie tylko potrafi wykonywać matematykę, ale także udowodnić, że robi to poprawnie. W kwietniu odwiedziłem te firmy w Dolinie Krzemowej, Kalifornia, by zrozumieć, dlaczego pokładają tak wielką wiarę w matematykę jako przewodnika w przyszłości z SI.
Biura Axiom Math znajdują się w Palo Alto, rzut beretem od Uniwersytetu Stanforda, gdzie założycielka firmy, Carina Hong, która była także byłym uczniem Ono, wcześniej studiowała. Kilka drzwi dalej znajduje się inny start-up, o nazwie Harmonic, który również ma na celu zbudowanie „matematycznej superinteligencji”, która produkuje weryfikowalne wyniki. Obie firmy zajmują niepozorne budynki, ale zgromadziły ogromne sumy pieniędzy, z inwestorami przelającymi setki milionów dolarów, aby osiągnąć swoje cele.
W jednym z niepozornych biur, z salami nazwanymi imionami słynnych matematyków, takich jak Carl Friedrich Gauss i Ada Lovelace, zapytałem Ono, dlaczego istnieje potrzeba firm takich jak jego, szczególnie w obliczu istnienia tak dobrze sfinansowanych i masowych firm SI, takich jak OpenAI i Google.
„ChatGPT to bibliotekarz; nie znajdziesz czegoś, czego nie przeczytał, ale czy chcesz, żeby twoim neurochirurgiem był bibliotekarz?” – mówi Ono. Ono tłumaczy mi, że pomimo sukcesu dużych modeli językowych, takich jak ChatGPT, nadal nie można na nich polegać pod kątem poprawności bez sprawdzenia przez ludzkich recenzentów, co stwarza możliwość weryfikacji.
Weryfikacja matematyczna to nie nowy koncept. W ostatnich dziesięcioleciach matematycy stworzyli różne systemy, za pomocą których można sprawdzić, czy dowód jest poprawny. Najpopularniejszym z tych systemów jest język programowania o nazwie Lean, którego matematycy mogą używać do przetłumaczenia swoich pisanek na formę, którą można natychmiast sprawdzić za pomocą komputera. Może to pomóc w matematyce na poziomie badawczym, gdzie sprawdzenie poprawności dowodu może zajmować ogromną ilość czasu już obciążonym badaczom.
Zbyt wiele do sprawdzenia
Podobny problem istnieje teraz w programowaniu komputerowym, ponieważ duże modele językowe generują ogromne ilości kodu, które często zawierają małe i trudne do wykrycia błędy, co sprawia, że wielu programistów ludzkich pełni role opiekunów produkowanych przez SI wyników.
To ostatnia kategoria, którą firmy takie jak Axiom Math i Harmonic widzą jako sposób na generowanie dochodów, ponieważ dostępne środki finansowe na rozwiązanie trudnych problemów matematycznych są niewielkie. Tak samo jak dowód matematyczny może zostać sprawdzony pod kątem poprawności za pomocą Lean lub podobnego języka programowania, tak samo można matematycznie udowodnić, że program komputerowy jest poprawny i nie zawiera błędów. „W miarę jak SI zaczyna pisać coraz więcej kodu, wzrasta dodatkowa wartość weryfikacji, ponieważ ludzie stają się wtedy bottlneckiem” – mówi dyrektor generalny Harmonic, Tudor Achim.
Podczas gdy weryfikacja oprogramowania to głównie przewidywane źródło dochodów obu firm, obie posiadają także narzędzia SI, które są niezwykle zdolne do rozwiązywania niektórych problemów matematycznych w aktywnych obszarach badawczych i wygenerowały sprawdzone dowody w dziedzinach takich jak geometria algebraiczna i teoria liczb. Pięć artykułów napisanych wyłącznie za pomocą narzędzi SI Axiom Math zostało zaakceptowanych w czasopismach matematycznych. Ono nie był w stanie powiedzieć mi dokładnej strategii firmy Axiom Math na przyszłe wyzwania, ale powiedział, że mają na celu napisanie kilkudziesięciu artykułów do przyszłego roku, kompresując wiele lat pracy w tygodnie i dni.
Te firmy mają do czynienia z zaciekłą konkurencją, zwłaszcza że giganci technologiczni również coraz bardziej koncentrują się na SI rozwiązujących problemy matematyczne. „Matematyka jest wspaniała dla rozwoju SI, ponieważ jest bardzo mierzalna” – mówi główny naukowiec OpenAI, Jakub Pachocki. „Ponadto, dla początkowych modeli językowych, była to wspaniała rzecz, która sprawiła im trudności. Naprawdę nie były dobre w bardzo wymiernych rzeczach. Ale teraz stały się dość dobre.”
Po wolnym starcie, podczas którego duże modele językowe miały trudności z formułowaniem prostych argumentów matematycznych, najnowsze modele SI osiągnęły szereg zdumiewających osiągnięć, najpierw zdobywając złoto na Międzynarodowej Olimpiadzie Matematycznej, elitarnej olimpiadzie szkolnej, która wcześniej uważana była za poza zasięgiem SI, a teraz obalając dychtatem 80-latia, którego niektórzy matematycy uważali, że nie zobaczą postępu za swojego życia.
“Wady, które widzieliśmy sześć miesięcy temu, były bardzo dobrze widoczne” – mówi Sébastien Bubeck z OpenAI. “Były dziedziny matematyki, gdzie model tylko mówił bzdury. Dzisiaj, to nieco nie wygląda tak.”
W przeciwieństwie do firm takich jak Axiom Math i Harmonic, które zatrudniły matematyków, żeby szkolić swoje modele w szczególnie adeptów matematyki, Bubeck twierdzi, że OpenAI nie optymalizuje swoich systemów SI w celu szczególnie dobrego wykonywania zadań matematycznych, ale próbuje produkować bardziej ogólnie inteligentne systemy, co jest również celem ogólnym w OpenAI. “Przeprowadzamy szkolenie ogólnego SI, i poprzez tę ogólną poprawę wychodzą zdolności, które nas wszystkich szokują pod kątem matematyki” – mówi Bubeck.
Która z tych podejść zwycięży, przyszłość matematyki kontrolowanej przez małą liczbę dobrze sfinansowanych firm technologicznych wywołała pewien niepokój wśród matematyków. Wszystkie te intensywne zainteresowania nadeszły nagle. A co jeśli zniknie równie szybko?
„W tej chwili jest wkładana duża ilość pieniędzy w ten obszar, a będziemy tego tęsknić, gdy zniknie” – mówi Ravi Vakil ze Stanford University. “To poprawia modele SI ogólnie, by stały się lepszymi matematycznymi myślicielami. Ale za pięć lat nie będzie już tak”. Nie ma zbyt wielu pieniędzy do zarobienia na rozwiązaniu hipotezy Riemanna.”
Teorematy z płatnym dostępem
Inną możliwą przyszłością jest to, że sama matematyka stanie się ogródkiem zaporowym, w którym można rozwiązać problem tylko wtedy, gdy ma się wystarczająco dużo pieniędzy lub dostęp do odpowiedniego modelu SI. Podczas gdy wiele narzędzi Axiom Math jest obecnie darmowych w użyciu, firma nie zdołała wykluczyć, że w przyszłości mogą one kosztować pieniądze.
“Dziś trochę matematyki już jest zaporowana” – mówi Shubho Sengupta z Axiom Math. “[Wielkie fundusze hedgingowe] robią wiele modelowania matematycznego. Nikomu innemu to nie jest dostępne, z dobrego powodu, ponieważ to jest ich własność intelektualna; to jest sposób, w jaki zarabiają pieniądze.”
Sengupta dodaje jednak, że „posuwanie granic wiedzy matematycznej do przodu powinno być darmowe.”
Achim z Harmonic ma podobne zdanie. “Narzędzie przydatne dla matematyki kosztuje pieniądze. Chcemy dać ludziom możliwość zapłacenia w zamian za usługę, którą chcą otrzymać.” To nie oznacza jednak, że nie będą wspierać matematyków, mówi. “Jeśli firma uważa, że matematyka jest naprawdę ważna dla przyszłości, zawsze będziemy chcieli wspierać matematyków najlepiej, jak tylko możemy. Nie sądzę, że jakakolwiek firma postrzega matematyków jako sposób na wyciągnięcie całej wartości dla firmy.”
Przewidywanie przyszłości to zadanie niezmiernie trudne, zwłaszcza dla modeli SI, biorąc pod uwagę ich niedawny postęp, ale prawdopodobne jest, że na przewidywalną przyszłość matematycy odegrają w niej wiodącą rolę. Opuszczając Axiom, Ono porównał nadejście systemów SI zdolnych do matematyki do momentu, kiedy Srinivasa Ramanujan po raz pierwszy zaszokował społeczność matematyczną. Ramanujan był samoukiem z Indii, którego odkrycia matematyczne wynikały głównie z intuicji, szokując społeczność matematyczną na początku XX wieku, ponieważ pojawiły się nagle.
Ojciec Ono, japoński matematyk, który przeniósł się do Stanów Zjednoczonych częściowo pod wpływem historii Ramanujana, zmarł w styczniu. Ono wspomina jedną z ich ostatnich rozmów razem: „Może to jest jak twój moment Ramanujana, może inni nie zrozumieją, i jeśli zobaczysz komputer, który wydaje się robić coś magicznego, powinieneś to przyjąć, ponieważ już to stało się nam wszystkim.
