Nowe modele AI zaczynają skutecznie rozwiązywać zadania, które dotąd uchodziły za domenę wąskiej elity matematyków. Najnowsze przykłady dotyczą problemów z listy Erdősa, a część rozwiązań przeszła weryfikację narzędziami do formalizacji. To krok, który zmienia dyskusję o tym, jak daleko mogą zajść duże modele językowe.

Nowe modele uczą się rozumować. Wyniki zaczynają zaskakiwać

Inżynier i założyciel startupu Neel Somani przetestował najnowszy model OpenAI i po kilkunastu minutach otrzymał pełne rozwiązanie trudnego problemu z kombinatoryki i teorii liczb. Rozumowanie zostało następnie ujednolicone w narzędziu Harmonic i pozytywnie zweryfikowane.

Model sięgnął po znane fakty, między innymi wzór Legendre’a, postulat Bertranda oraz twierdzenie zwane Gwiazdą Dawida. W trakcie pracy odnalazł też dyskusję sprzed lat, w której znany matematyk z Harvardu proponował pokrewne rozwiązanie, ale finalny dowód AI był inny i pełniej odpowiadał na wariant problemu Erdősa.

Statystyki mówią o przełomie. To może zmienić sposób pracy matematyków

Od Świąt na stronie katalogującej problemy Erdősa status z otwartego na rozwiązany zmieniono przy 15 pozycjach. W 11 z nich autorzy wprost wskazali, że w rozwiązaniu pomogły modele AI.

Uzupełniający przegląd przygotowany przez cenionego badacza pokazuje osiem przypadków, gdzie modele samodzielnie popchnęły dowodzenie do przodu, oraz sześć, w których kluczowe było odnalezienie i zsyntetyzowanie wcześniejszej literatury. To potwierdza, że AI nie jest jeszcze w pełni autonomicznym matematykiem, ale ma realny wkład w zamykanie kolejnych zagadek.

Coraz większe znaczenie ma formalizacja dowodów, która ułatwia ich sprawdzanie i późniejszą rozbudowę. Ważną rolę odgrywa tu otwarte środowisko Lean oraz narzędzia automatyzujące, takie jak Aristotle od Harmonic.

Dla twórców tych narzędzi liczy się nie tylko liczba „odhaczonych” zadań, ale przede wszystkim to, że po rozwiązania sięgają profesorowie matematyki i informatyki. Akceptacja w środowisku naukowym bywa mocniejszym sygnałem niż pojedyncze spektakularne case study.

Skalowalność daje przewagę. Długi ogon problemów może paść szybciej

Badacze zwracają uwagę, że skalowalny charakter systemów AI sprzyja hurtowemu atakowaniu wielu mniejszych, rzadziej opisywanych zadań. W tak zwanym długim ogonie jest wiele problemów, które mają względnie proste rozwiązania, a AI potrafi je wyłuskać dzięki szybkiej syntezie znanych faktów.

Pełna autonomia w matematyce to wciąż odległy cel, jednak kierunek jest jasny. Najbliższe lata mogą należeć do duetów człowiek, maszyna, w których AI przyspiesza weryfikację, podpowiada tropy i porządkuje dowody.

Źródło: TechCrunch