Matematycy z MIT, David Roe i Andrew Sutherland, zostali laureatami grantów „AI for Math” – pierwszego programu finansowania uruchomionego przez Renaissance Philanthropy i XTX Markets. Jako pracownicy Wydziału Matematyki MIT zamierzają wykorzystać tę okazję do połączenia sztucznej inteligencji z przełomowymi badaniami matematycznymi.
Ta nowa inicjatywa ma na celu przyspieszenie odkryć matematycznych poprzez sfinansowanie 29 pionierskich projektów, z których każdy zakłada wykorzystanie sztucznej inteligencji do przekształcenia dziedziny matematyki. Chodzi przede wszystkim o zapewnienie matematykom narzędzi do opracowywania systemów sztucznej inteligencji, które przyspieszą tempo odkryć i usprawnią rozumowanie formalne w szerokim spektrum dziedzin 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).
Z jednej strony biblioteka mathlib – obszerna biblioteka rozwijana przez ogromną międzynarodową społeczność – wykorzystuje system dowodzenia Lean do weryfikacji poprawności każdego logicznego kroku w dowodzie. Zawierając około 100 000 wyników matematycznych, stanowi ona prawdziwą kopalnię wyników badań matematycznych.
Z drugiej strony mamy LMFDB – ogromną cyfrową encyklopedię poświęconą współczesnej teorii liczb. Zawiera ona ponad miliard twierdzeń matematycznych i punktów danych, stanowiąc nieocenione źródło informacji zarówno dla profesjonalnych matematyków, jak i dla tych, którzy dopiero rozpoczynają swoją karierę w tej dziedzinie. Poradzenie sobie z tą kolosalną górą danych jest zadaniem nie lada wyzwaniem, ale Roe i Sutherland, pełniąc funkcję redaktorów naczelnych LMFDB, są właśnie odpowiednimi osobami do tego zadania.
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 udostępnienie mathlib ogromnej bazy faktów z zakresu teorii liczb zgromadzonych w LMFDB. Integracja ta umożliwiłaby zarówno agentom sztucznej inteligencji, jak i ludzkim matematykom nieograniczone zgłębianie matematycznego wszechświata. Aby to osiągnąć, zespół nie planuje formalizacji całej bazy LMFDB – co byłoby niezwykle pracochłonne – lecz zamierza opracować narzędzia, które w sposób selektywny będą czerpać z jej zawartości. Strategia ta, która ma obniżyć koszty, oznacza, że nie wszystkie informacje niezbędne do sformułowania nowych twierdzeń muszą być formalnie udowodnione.
Współczesne twierdzenia matematyczne, takie jak dowód ostatniego twierdzenia Fermata autorstwa Andrew Wilesa, w znacznym stopniu opierają się na etapach obliczeniowych, których ręczna formalizacja nie jest łatwa. Właśnie dlatego matematyczne bazy danych, takie jak LMFDB, mają nieocenioną wartość i stanowią kluczowe źródło informacji dla matematyków.
Nie da się przecenić znaczenia selekcji danych w matematycznych bazach danych. Na przykład skupienie się bazy LMFDB na przewodniku w krzywych eliptycznych miało kluczowe znaczenie dla niedawnego zidentyfikowania „murmuracji” krzywych eliptycznych – zjawiska odkrytego przy użyciu technik uczenia maszynowego.
Roe i jego zespół zamierzają rozpocząć całe przedsięwzięcie od sformalizowania definicji, które stanowią podstawę sekcji bazy danych LMFDB dotyczących krzywych eliptycznych, pól liczbowych i form modułowych oraz umożliwiają przeprowadzanie wyszukiwań w bazie LMFDB w ramach biblioteki mathlib. Ich plan stwarza studentom MIT możliwość wzięcia udziału w tej wielkiej matematycznej przygodzie.
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.
Ta strona używa plików cookie.