Medale Fieldsa ostrzegają: matematyka i firmy AI mają różne cele

Napięcie między społecznością matematyczną a firmami rozwijającymi sztuczną inteligencję przestało być kuluarową dyskusją. W „Le Monde” ukazał się tekst podpisany przez dwudziestu pięciu laureatów medalu Fieldsa, najwyższego wyróżnienia w matematyce. Autorzy piszą wprost, że cele firm AI i cele wspólnoty matematycznej rozchodzą się głęboko. Zarzut nie dotyczy tego, że modele rozwiązują zadania. Chodzi o to, po co się je rozwiązuje i jak się o tym opowiada.

Dowód nie jest produktem

Kilka dni później „Le Monde” opublikował rozmowę ze Stéphane’em Mallatem, matematykiem z ENS, uhonorowanym w 2025 roku złotym medalem CNRS, współtwórcą algorytmu kompresji JPEG 2000. Jego zdanie jest hasłem przewodnim całej debaty: dowody wykonane przez AI mają niewiele wartości same w sobie, jeśli nie mamy wystarczającego przygotowania, żeby je zrozumieć. Mallat zajmuje się między innymi przekleństwem wielowymiarowości. W tym problemie liczba możliwych konfiguracji rośnie tak gwałtownie, że nabieranie intuicji z niskich wymiarów przestaje mieć sens.

Argument ten da się ująć konkretnie. Matematyka to nie tylko zbiór prawdziwych twierdzeń. To także technika rozumienia, dlaczego są prawdziwe. Weryfikator potwierdzi poprawność formalnego zapisu, nie przekaże jednak uczniowi żadnej z tych umiejętności, dopóki nie zostanie ona wyłożona i przedyskutowana.

Co dziś umie maszynowa weryfikacja

Równolegle powstają prace, które pokazują, jak wygląda rzetelna współpraca człowieka z maszyną. Mario Carneiro dowodzi w artykule na arXiv, że w teorii typów asystenta Lean wystarczy prawo wyłączonego środka, bez aksjomatu wyboru, bez ekstensjonalności zdań i bez ilorazów, żeby udowodnić niesprzeczność teorii mnogości ZF, i to w formie w pełni sformalizowanej. To wynik techniczny, ale ma ciężar filozoficzny. Dotąd można było sądzić, że bez operatora wyboru siła teorii typów spada znacznie poniżej ZF.

Drugi nurt to przeszukiwanie wspomagane weryfikacją. Model proponuje programy w stylu FunSearch, twardy ewaluator je ocenia, a wybór zostawia najlepsze. Autorzy jednej z takich prac prowadzili eksperyment nawet na laptopie, z lokalnym modelem trzydziestomiliardowym i od 120 do 600 zweryfikowanych próbek na przebieg. Wynik jest dwuznaczny i dlatego cenny. Przeszukiwanie zatrzymało się po zamknięciu nieco ponad 90 proc. luki do rekordu na zadaniu flagowym. Gdy podano modelowi wskazówkę o rodzinie konstrukcji, pętla zoptymalizowała podany pomysł, choć żadne z samodzielnych uruchomień go nie odkryło.

W tle pozostaje kwestia zachęt. Jeśli najważniejszym kryterium staje się rekord w tabeli, matematyka zamienia się w zestaw benchmarków, a nie w praktykę rozumienia. Ostrożność przed takim uproszczeniem nie jest wrogością wobec narzędzi. To warunek, żeby narzędzia były do czegokolwiek trwale przydatne.