Matematycy z MIT otrzymali grant AI for Math na stworzenie pomostu między bazami danych a weryfikatorami twierdzeń

Matematycy z MIT, David Roe i Andrew Sutherland, zostali laureatami grantów AI for Math, inauguracyjnego programu finansowania uruchomionego przez Renaissance Philanthropy i XTX Markets. Jako członkowie Wydziału Matematyki MIT zamierzają skorzystać z okazji, aby połączyć sztuczną inteligencję z przełomowymi badaniami matematycznymi.

Ta nowa inicjatywa ma na celu napędzanie odkryć matematycznych poprzez finansowanie 29 pionierskich projektów, z których każdy ma na celu przekształcenie dziedziny matematyki. Chodzi o zapewnienie matematykom narzędzi do opracowania systemów sztucznej inteligencji, które zwiększą szybkość odkrywania i poprawią formalne rozumowanie w szerokim zakresie obszarów matematycznych.

W ramach tego imponującego wdrożenia, Roe i Sutherland, współpracując z Chrisem Birkbeckiem z University of East Anglia, planują wykorzystać swój grant do połączenia dwóch głównych zasobów matematycznych: L-Functions and Modular Forms Database (LMFDB) oraz biblioteki matematycznej Lean4 (mathlib).

Łączenie dziedzin matematycznych ze sztuczną inteligencją

Z jednej strony, mathlib, wszechstronna biblioteka prowadzona przez ogromną międzynarodową społeczność, wykorzystuje weryfikator twierdzeń Lean do weryfikacji poprawności każdego logicznego kroku w dowodzie. Z około 100 000 wyników matematycznych, jest to w zasadzie kopalnia złota matematycznych odkryć.

Z drugiej strony jest LMFDB, gigantyczna cyfrowa encyklopedia współczesnej teorii liczb. Zawierająca ponad miliard twierdzeń matematycznych i punktów danych, jest źródłem informacji zarówno dla profesjonalnych, jak i początkujących matematyków. Zrozumienie tej kolosalnej góry danych jest trudnym zadaniem, ale Roe i Sutherland jako redaktorzy zarządzający LMFDB są odpowiednimi ludźmi do tego zadania.

Demistyfikacja matematyki za pomocą sztucznej inteligencji

Jak przyznaje Sutherland, tradycyjna ścieżka nauki do zrozumienia zautomatyzowanych systemów dowodzenia twierdzeń jest stroma. Jednak ze względu na rosnącą dostępność i skuteczność dużych modeli językowych (LLM) i innych narzędzi sztucznej inteligencji, proces uczenia się stał się mniej onieśmielający, zapraszając szersze grono matematyków do korzystania z tych systemów.

Głównym celem jest tutaj wykorzystanie ogromnych faktów z teorii liczb LMFDB w mathlib. Integracja ta otworzyłaby nieograniczoną eksplorację matematycznego wszechświata zarówno dla agentów AI, jak i ludzkich matematyków. Aby to osiągnąć, zespół nie planuje formalizować całej LMFDB - co byłoby niezwykle pracochłonne - a raczej opracować narzędzia, które selektywnie wykorzystują jej zawartość. Taktyka ta, która ma obniżyć koszty, zakłada, że nie wszystkie informacje wymagane do ustalenia nowych twierdzeń muszą być formalnie udowodnione.

Nowoczesne twierdzenia matematyczne, takie jak dowód ostatniego twierdzenia Fermata przeprowadzony przez Andrew Wilesa, opierają się w dużej mierze na krokach obliczeniowych, które nie są tak proste do sformalizowania ręcznie. Właśnie dlatego matematyczne bazy danych, takie jak LMFDB, są nieocenione i służą jako kluczowe zasoby dla matematyków.

Znaczenie kurateli w matematycznych bazach danych jest nie do przecenienia. Na przykład, skupienie się LMFDB na przewodniku w krzywych eliptycznych było kluczowe dla niedawnej identyfikacji szemranych krzywych eliptycznych, zjawiska odkrytego przy użyciu technik uczenia maszynowego.

Budowanie przyszłości matematyki

Roe i jego zespół zamierzają rozpocząć całe przedsięwzięcie od sformalizowania definicji, które stanowią podstawę sekcji krzywej eliptycznej, pola liczbowego i formy modularnej LMFDB oraz umożliwiają wykonywanie wyszukiwań LMFDB w mathlib. Ich plan otwiera możliwości dla studentów MIT, aby stać się częścią tej wielkiej matematycznej przygody.

Oprócz Roe i Sutherlanda, czterech innych pionierów matematyki z MIT - Anshula Gandhi, Viktor Kunčak, Gireeja Ranade i Damiano Testa - otrzymało granty AI for Math w uznaniu ich innowacyjnej pracy w tej dziedzinie.

Więcej informacji na temat grantów AI for Math można znaleźć w pełnym artykule tutaj.