Liczmy (się) z papugami
AI sformułowała nowe twierdzenie matematyczne. „Największe zmiany zobaczymy tam, gdzie ludzki umysł napotyka swoje naturalne ograniczenia”
MARCIN ROTKIEWICZ: – W londyńskiej siedzibie Google DeepMind ważne osiągnięcia ogłasza się uderzeniami w gong. Zabrzmiał on m.in. pół roku temu, kiedy program AlphaProof otarł się o złoty medal międzynarodowej olimpiady matematycznej. Czy AI niedługo okaże się lepsza od ludzi w matematyce?
PUSHMEET KOHLI: – Postępy w tym obszarze dokonują się naprawdę szybko. Bo choć AlphaProof nie zdobył złotego medalu (zabrakło mu jednego punktu – przyp. red.), to już dokonał czegoś przełomowego. Po raz pierwszy pokazaliśmy, że system AI może rozumować na tak wysokim poziomie złożoności, gdyż problemy z olimpiady wymagają analizy w wielu długich krokach myślowych.
Spośród sześciu zadań AlphaProof rozwiązał cztery. Z czym sobie nie poradził?
Z kombinatoryką (dział matematyki zajmujący się – w uproszczeniu – liczeniem możliwości: np. mamy klocki, z których budujemy wieżę, i obliczamy, na ile różnych sposobów da się to zrobić – przyp. red.). Zadania z tej dziedziny wymagają analizy ogromnej liczby potencjalnych rozwiązań. Cały czas intensywnie badamy, dlaczego właśnie kombinatoryka okazała się tak trudna dla AI, i pracujemy nad ulepszeniami algorytmu.
Jak w ogóle działa AlphaProof?
Pracuje w specjalnym języku formalnym Lean, który służy do precyzyjnego zapisu zagadnień matematycznych. Aby wytrenować AlphaProof, zebraliśmy wiele takich problemów zapisanych po angielsku i stworzyliśmy translator, który przekładał je na Lean. Tak powstał pokaźny zbiór danych treningowych. Następnie program próbował rozwiązywać trudne problemy matematyczne, tworząc ich różne warianty, czasami prostsze. Ten ostatni etap może trwać nawet kilka dni.
Czy AlphaProof zastąpi kiedyś matematyków?