Matematycy z MIT, David Roe i Andrew Sutherland, zostali laureatami grant\u00f3w AI for Math, inauguracyjnego programu finansowania uruchomionego przez Renaissance Philanthropy i XTX Markets. Jako cz\u0142onkowie Wydzia\u0142u Matematyki MIT zamierzaj\u0105 skorzysta\u0107 z okazji, aby po\u0142\u0105czy\u0107 sztuczn\u0105 inteligencj\u0119 z prze\u0142omowymi badaniami matematycznymi.<\/p>\n
Ta nowa inicjatywa ma na celu nap\u0119dzanie odkry\u0107 matematycznych poprzez finansowanie 29 pionierskich projekt\u00f3w, z kt\u00f3rych ka\u017cdy ma na celu przekszta\u0142cenie dziedziny matematyki. Chodzi o zapewnienie matematykom narz\u0119dzi do opracowania system\u00f3w sztucznej inteligencji, kt\u00f3re zwi\u0119ksz\u0105 szybko\u015b\u0107 odkrywania i poprawi\u0105 formalne rozumowanie w szerokim zakresie obszar\u00f3w matematycznych. <\/p>\n
W ramach tego imponuj\u0105cego wdro\u017cenia, Roe i Sutherland, wsp\u00f3\u0142pracuj\u0105c z Chrisem Birkbeckiem z University of East Anglia, planuj\u0105 wykorzysta\u0107 sw\u00f3j grant do po\u0142\u0105czenia dw\u00f3ch g\u0142\u00f3wnych zasob\u00f3w matematycznych: L-Functions and Modular Forms Database (LMFDB) oraz biblioteki matematycznej Lean4 (mathlib).<\/p>\n
Z jednej strony, mathlib, wszechstronna biblioteka prowadzona przez ogromn\u0105 mi\u0119dzynarodow\u0105 spo\u0142eczno\u015b\u0107, wykorzystuje weryfikator twierdze\u0144 Lean do weryfikacji poprawno\u015bci ka\u017cdego logicznego kroku w dowodzie. Z oko\u0142o 100 000 wynik\u00f3w matematycznych, jest to w zasadzie kopalnia z\u0142ota matematycznych odkry\u0107. <\/p>\n
Z drugiej strony jest LMFDB, gigantyczna cyfrowa encyklopedia wsp\u00f3\u0142czesnej teorii liczb. Zawieraj\u0105ca ponad miliard twierdze\u0144 matematycznych i punkt\u00f3w danych, jest \u017ar\u00f3d\u0142em informacji zar\u00f3wno dla profesjonalnych, jak i pocz\u0105tkuj\u0105cych matematyk\u00f3w. Zrozumienie tej kolosalnej g\u00f3ry danych jest trudnym zadaniem, ale Roe i Sutherland jako redaktorzy zarz\u0105dzaj\u0105cy LMFDB s\u0105 odpowiednimi lud\u017ami do tego zadania. <\/p>\n
Jak przyznaje Sutherland, tradycyjna \u015bcie\u017cka nauki do zrozumienia zautomatyzowanych system\u00f3w dowodzenia twierdze\u0144 jest stroma. Jednak ze wzgl\u0119du na rosn\u0105c\u0105 dost\u0119pno\u015b\u0107 i skuteczno\u015b\u0107 du\u017cych modeli j\u0119zykowych (LLM) i innych narz\u0119dzi sztucznej inteligencji, proces uczenia si\u0119 sta\u0142 si\u0119 mniej onie\u015bmielaj\u0105cy, zapraszaj\u0105c szersze grono matematyk\u00f3w do korzystania z tych system\u00f3w. <\/p>\n
G\u0142\u00f3wnym celem jest tutaj wykorzystanie ogromnych fakt\u00f3w z teorii liczb LMFDB w mathlib. Integracja ta otworzy\u0142aby nieograniczon\u0105 eksploracj\u0119 matematycznego wszech\u015bwiata zar\u00f3wno dla agent\u00f3w AI, jak i ludzkich matematyk\u00f3w. Aby to osi\u0105gn\u0105\u0107, zesp\u00f3\u0142 nie planuje formalizowa\u0107 ca\u0142ej LMFDB - co by\u0142oby niezwykle pracoch\u0142onne - a raczej opracowa\u0107 narz\u0119dzia, kt\u00f3re selektywnie wykorzystuj\u0105 jej zawarto\u015b\u0107. Taktyka ta, kt\u00f3ra ma obni\u017cy\u0107 koszty, zak\u0142ada, \u017ce nie wszystkie informacje wymagane do ustalenia nowych twierdze\u0144 musz\u0105 by\u0107 formalnie udowodnione. <\/p>\n
Nowoczesne twierdzenia matematyczne, takie jak dow\u00f3d ostatniego twierdzenia Fermata przeprowadzony przez Andrew Wilesa, opieraj\u0105 si\u0119 w du\u017cej mierze na krokach obliczeniowych, kt\u00f3re nie s\u0105 tak proste do sformalizowania r\u0119cznie. W\u0142a\u015bnie dlatego matematyczne bazy danych, takie jak LMFDB, s\u0105 nieocenione i s\u0142u\u017c\u0105 jako kluczowe zasoby dla matematyk\u00f3w. <\/p>\n
Znaczenie kurateli w matematycznych bazach danych jest nie do przecenienia. Na przyk\u0142ad, skupienie si\u0119 LMFDB na przewodniku w krzywych eliptycznych by\u0142o kluczowe dla niedawnej identyfikacji szemranych krzywych eliptycznych, zjawiska odkrytego przy u\u017cyciu technik uczenia maszynowego. <\/p>\n
Roe i jego zesp\u00f3\u0142 zamierzaj\u0105 rozpocz\u0105\u0107 ca\u0142e przedsi\u0119wzi\u0119cie od sformalizowania definicji, kt\u00f3re stanowi\u0105 podstaw\u0119 sekcji krzywej eliptycznej, pola liczbowego i formy modularnej LMFDB oraz umo\u017cliwiaj\u0105 wykonywanie wyszukiwa\u0144 LMFDB w mathlib. Ich plan otwiera mo\u017cliwo\u015bci dla student\u00f3w MIT, aby sta\u0107 si\u0119 cz\u0119\u015bci\u0105 tej wielkiej matematycznej przygody. <\/p>\n
Opr\u00f3cz Roe i Sutherlanda, czterech innych pionier\u00f3w matematyki z MIT - Anshula Gandhi, Viktor Kun\u010dak, Gireeja Ranade i Damiano Testa - otrzyma\u0142o granty AI for Math w uznaniu ich innowacyjnej pracy w tej dziedzinie. <\/p>\n