Są większe problemy niż obliczenie opłaty od Taurona. Potrzebujemy do nich wsparcia AI
Problemy Hilberta, Landau, Smale? Matematyka posiada wiele nierozwiązanych dowodów, przy których wykładają się nawet superkomputery. Sporą część z największych zagadek matematyki udałoby się rozwiązać, gdybyśmy byli w stanie przetłumaczyć je na systemy formalne. Na szczęście z pomocą przychodzi nie kto inny jak sztuczna inteligencja, która odpowiednio wytrenowana jest w stanie przetłumaczyć dowody matematyczne na język zrozumiały dla komputera.
Zadania matematyczne takie jak obliczenie opłaty od Taurona nie są dla komputerów wielkim wyzwaniem - o ile są zapisane w sposób zrozumiały dla komputera. Jak dowodzą inżynierowie i naukowcy współpracujący z Google, sztuczna inteligencja może tłumaczyć problemy matematyczne napisane prostym językiem angielskim na system formalny. A to z kolei ułatwi komputerom rozwiązywanie zadań matematycznych, rozwiązanie wcześniej niemożliwych do rozwiązania dowodów oraz zbliży świat nauki do zbudowania maszyny zdolnej do odkrywania nowej matematyki.
Sztuczna inteligencja pomoże z matematycznymi problemami
Matematycy już od lat wspomagają się komputerami przy weryfikacji dowodów matematycznych. Jednocześnie, pomimo stałego rozwoju technologii na ich drodze wciąż stoi jedna przeszkoda - język. Naukowcy mogą wykorzystać komputer do potwierdzania dowodów matematycznych tylko wtedy, gdy problemy zostały przygotowane w specjalnie zaprojektowanym języku dowodowym, a nie jako kombinacja notacji matematycznej i tekstu pisanego używanego przez matematyków. Ten proces, znany jako formalizacja - w przypadku niektórych dowodów - może zająć miesiące, a nawet lata. Tak więc tylko niewielka część wiedzy matematycznej została sformalizowana, a następnie udowodniona przez maszynę.
Yuhuai Wu z Google i jego współpracownicy korzystali z sieci neuronowej o nazwie Codex stworzonej przez firmę OpenAI. Codex został przeszkolony w zakresie dużych ilości danych tekstowych oraz programistycznych z Internetu i może być używany przez programistów do generowania działającego kodu - tłumaczenia dowodów matematycznych na system formalny, zrozumiały dla komputera.
Biorąc pod uwagę, że systemy formalne używane w matematyce mają dużo wspólnego z językami programowania, zespół postanowił sprawdzić, czy Codex jest w stanie sformalizować zbiór 12 500 zadań konkursowych z matematyki na poziomie szkoły średniej. Sieć neuronowa była w stanie przetłumaczyć jedną czwartą wszystkich problemów na format zgodny z programem do rozwiązywania formalnych dowodów o nazwie Isabelle. Wiele nieudanych tłumaczeń było wynikiem braku zrozumienia przez system pewnych pojęć matematycznych, mówi Wu. "Jeśli pokażesz modelowi przykład, który wyjaśnia tę koncepcję, model może szybko go załapać.
Aby przetestować skuteczność tego procesu autoformalizacji, zespół zastosował Codex do zestawu problemów, które zostały już sformalizowane przez ludzi. Codex wygenerował własne formalne wersje tych problemów, a zespół wykorzystał inną sztuczną inteligencję - MiniF2F, do rozwiązania obu wersji.
Automatycznie sformalizowane problemy poprawiły skuteczność MiniF2F z 29 proc. do 35 proc. A to z kolei, według naukowców, sugeruje, że Codex był lepszy niż ludzie w formalizowaniu przedstawionych mu problemów.
Dalsza poprawa skuteczności pozwoliłaby sztucznej inteligencji konkurować z ludzkimi matematykami, mówi członek zespołu Wu, Albert Jiang z University of Cambridge.
Chociaż bezpośrednim celem jest ulepszenie modeli autoformalizacji i zautomatyzowanych maszyn udowadniających, efekty mogą zaskoczyć świat nauki. Zdaniem Wu, modele mogą odkryć obszary matematyki obecnie nieznane ludziom.
Zdolność rozumowania w takiej maszynie może również sprawić, że będzie ona dobrze dostosowana do zadań weryfikacyjnych w szerokim zakresie dziedzin. Jak mówi Alber Jiang, stu procentowa skuteczność maszyny dałaby ludziom możliwość zastosowania jej przy autoweryfikacji czy - na przykład - oprogramowanie działa zgodnie z zamierzeniem jego twórcy.
