Zdaniem Timothy’ego Gowersa niemal wszystkie najgłośniejsze problemy rozwiązane do tej pory przez modele miały charakter przykładu albo kontrprzykładu, a nie dowodu. Laureat Medalu Fieldsa napisał o tym 12 sierpnia i nie jest to zarzut wobec tych wyników, bo nazywa je nadzwyczaj imponującymi. Jego rozumowanie idzie w inną stronę. Duże modele językowe pracują znacznie szybciej od ludzi, więc gdyby były od nich lepsze w każdym dziale matematyki, wyników powinno być dziś znacznie więcej. Skoro tak się nie dzieje, warto zapytać, w jakiej matematyce te modele są naprawdę dobre. Autor od razu zaznacza, że opisuje początek sierpnia 2026 i spodziewa się, że tekst szybko stanie się zapisem chwili.
Co dokładnie zauważył Timothy Gowers
Wpis powstał kilka dni po ogłoszeniu przez OpenAI, że firma rozwiązała dziesięć dużych problemów matematycznych i informatycznych. Pisaliśmy o tym przy dziesięciu formalizacjach sprawdzanych w Leanie. Dwa z nich Gowers wymienia z nazwy. Pierwszy to konstrukcja grupy niesoficznej. Na podstawie wykładów, w których brał udział, uznaje ją za jeden z najważniejszych nierozwiązanych problemów teorii grup. Drugi to dowód, że wielobarwna liczba Ramseya rośnie superwykładniczo. Tego akurat nie spodziewał się zobaczyć rozwiązanego za swojego życia.
Jego obserwacja dotyczy formy tych rozstrzygnięć. Najgłośniejsze wyniki modeli polegały na wskazaniu obiektu, który psuje regułę, a nie na wykazaniu, że reguła zawsze działa. Poza dwoma wymienionymi wyżej Gowers przywołuje hipotezę jakobianową i hipotezę odległości jednostkowej, o której obaleniu pisaliśmy osobno.
Jedno zastrzeżenie jest przy tym kluczowe i sam autor stawia je wprost. Modele potrafią również dowodzić trudnych twierdzeń. Rzecz w tym, że ich najsilniejsze osiągnięcia to jak dotąd te, które nazwalibyśmy przykładami.
Dlaczego kontrprzykład to nie to samo co dowód
Zanim Gowers przechodzi do wyjaśnień, rozbraja własną tezę. Podział na przykład i kontrprzykład jest mniej ostry, niż się wydaje. Nie decyduje o nim sama forma logiczna zdania. Znaczenie ma również kontekst matematyczny oraz to, czy istniały dobre powody, by spodziewać się prawdziwości obalonego twierdzenia.
Stąd bierze się jego rewizja jednego z dwóch flagowych wyników. Zdaniem Gowersa grupa niesoficzna to raczej przykład niż kontrprzykład. W literaturze krążyły już propozycje jej konstrukcji, a on sam nie sądzi, żeby wielu badaczy mocno wierzyło w soficzność wszystkich grup. Odnotowuje przy tym, że OpenAI zatytułowało tę część swojej pracy kontrprzykładem dla hipotezy o soficzności.
Podobnie rozkłada wynik dla liczby Ramseya. Część środowiska spodziewała się oszacowania wykładniczego i dla tych osób nowy wynik faktycznie jest kontrprzykładem. Gowers do nich nie należał, bo pracował kiedyś nad równoważnym sformułowaniem i szedł akurat w tę stronę, która okazała się właściwa. Ten sam wynik jest więc dla jednych zaskoczeniem, a dla innych potwierdzeniem przeczucia.
Skąd według Gowersa bierze się przewaga modeli
Autor stawia hipotezę, a nie diagnozę, i sam pisze o niej jak o przypuszczeniu. Zaczyna od dwóch rzeczy, co do których jego zdaniem możemy być pewni. Pierwsza to bardzo szeroka wiedza, dzięki której problem rozwiązywalny stosunkowo standardowym argumentem ma duże szanse zostać rozwiązany. Druga wynika po prostu z tego, że modele są komputerami: pracują szybko, więc stać je na wiele nieudanych prób przed trafieniem.
Z tych dwóch cech Gowers wyprowadza styl pracy. Modele powinny mieć przewagę tam, gdzie w szukaniu dowodu jest element losowy. Chodzi o problemy, przy których trzeba wypróbować mnóstwo niekoniecznie odkrywczych pomysłów, aż któryś zadziała. Według tego przypuszczenia ludzie mieliby na razie przewagę w argumentach zaskakujących i pojęciowych, gdzie metodą jest drążenie jednego tropu coraz głębiej.
Pewnego wsparcia dostarczają reakcje ekspertów na głośne rozwiązania. Gowers przytacza ich typowe brzmienie, nie cytując nikogo z nazwiska. Najpierw pada zdumienie, że problem w ogóle padł. Po bliższym oglądzie przychodzi wniosek, że podejście nie było wcale takie nowatorskie, a odpowiednio biegły człowiek trafiłby na nie przy jednej drobnej podpowiedzi.
Czego według Gowersa modelom brakuje
Umiejętność, której według jego przypuszczenia modelom może jeszcze brakować, autor nazywa węchem. Chodzi o wyczucie, czy obrany kierunek dokądś prowadzi, i o wynikającą z niego zdolność do bezlitosnego przycinania drzewa poszukiwań. Bez takiego przycinania drzewo może urosnąć zbyt wielkie nawet dla komputera, a z nim wystarczy sprawdzić ułamek możliwości.
Gowers opisuje to na własnym doświadczeniu z modelem 5.6 Pro. Dostaje od niego podejścia, które brzmią obiecująco, dopóki nie zacznie się w nie wczytywać. Model często kończy też odpowiedź informacją, że nie rozwiązał postawionego pytania, ale sprowadził je do węższego i bardziej precyzyjnego. Brzmi to zachęcająco za pierwszym razem, mniej po piątym bez widocznego postępu.
Ciekawsze jest jednak wyjaśnienie, dlaczego ten węch może nie pojawić się sam wraz ze skalą. Powody są dwa. W danych treningowych modele widzą zwykle wygładzone dowody, które ukrywają drogę odkrycia, więc prawie nie mają wglądu w to, jak wygląda porzucanie złych tropów. Do tego model zdolny do przeszukiwania siłowego nie ma powodu, żeby oszczędzać sobie pracy, a człowiek ma.
Pierwsza Misja AI · Kodożercy
AI zmienia rynek pracy. Zacznij rozumieć o co chodzi.
Kurs Pierwsza Misja AI to najkrótszy kurs, po którym naprawdę rozumiesz AI, a na koniec możesz to pokazać certyfikatem. Sci-fi fabuła i gamifikacja sprawiają, że nie nudzisz się ani minuty.
Dołącz do kursantów →
Po czym poznamy, że przeszkoda została pokonana
Największą zaletą tego wpisu jest to, że autor nie zostawia swojej tezy jako nastroju. Podaje warunek, który da się sprawdzić. Uzna sprawę za rozstrzygniętą, gdy model przedstawi dowód tak zaskakujący, jak rozwiązanie problemu zbioru bez trójek arytmetycznych z 2016 roku. Wcześniejsze oszacowania zostały wtedy całkowicie pobite, a metoda okazała się zupełnie inna niż wszystko, co rozważano. Po publikacji ruszyła fala prac rozwijających nową technikę.
Gowers proponuje też dwa sposoby wcześniejszego sprawdzenia swojej hipotezy. Pierwszy to inna struktura nagrody w trenowaniu. Model dostawałby nagrodę za rozwiązanie, ale dodatkowo karę za nadmiar ślepych zaułków i za odtworzenie odpowiedzi z literatury. Drugi to test na słabszych modelach, do pewnego stopnia odizolowanych od literatury matematycznej, na specjalnie dobranym zestawie problemów.
Zastrzeżenie autora jest przy tym mocniejsze, niż wygląda cały wywód. Gowers pisze wprost, że nie twierdzi, jakoby modele czegoś nigdy nie potrafiły. Uważa za prawdopodobne, że będą potrafiły, i to raczej szybko, biorąc pod uwagę tempo ostatnich trzech lat. Jego zdanie brzmi ostrożniej: może istnieć jedna przeszkoda, której pokonanie nie pójdzie tak gładko jak poprzednich.
Co z tego wynika poza matematyką
Ta sekcja jest już naszym przeniesieniem, bo Gowers pisze wyłącznie o matematyce. Punktem wyjścia jest jedno jego spostrzeżenie, którego nie da się rozstrzygnąć z zewnątrz. Kiedy model wpada na pomysł wyglądający na owoc głębokiego namysłu, nigdy nie mamy pewności, czy ten namysł faktycznie się odbył. Równie dobrze model mógł odtworzyć wzorzec gotowy w literaturze.
W codziennej pracy z modelem różnicy między znalezieniem odpowiedzi a zrozumieniem zadania też nie zawsze widać po wyniku. Naszym zdaniem podobny wzorzec można zauważyć przy pisaniu kodu. Szeroka wiedza, dużo szybkich prób i trafienie, którego autor nie potrafi potem uzasadnić. Przy zadaniach rutynowych to działa świetnie. Przy zadaniach, gdzie właściwy kierunek trzeba wyczuć, kończy się serią poprawnych, ale jałowych podejść.
Praktyczny wniosek jest prosty. Wynik od modelu warto oceniać po tym, czy da się odtworzyć drogę do niego, a nie po tym, jak pewnie brzmi. W matematyce służy do tego formalna weryfikacja, która sprawdza poprawność gotowego dowodu, choć nie odtwarza procesu jego odkrycia. Pisaliśmy o niej przy Leanstralu i sprawdzaniu dowodów w Leanie 4.
Najczęstsze pytania
Czy Gowers twierdzi, że modele nie potrafią dowodzić twierdzeń?
Nie i zaznacza to wprost. Pisze, że modele znajdują dowody trudnych stwierdzeń, a nie tylko kontrprzykłady. Jego obserwacja jest węższa. Spośród wszystkiego, co do tej pory rozwiązały, najmocniejsze wyniki to te, które nazwalibyśmy przykładami. Najmocniejsze wyniki w kategorii twierdzeń są od nich słabsze. To jest zdanie o rozkładzie osiągnięć, nie o brakującej umiejętności. Podobnej ostrożności wymaga czytanie wyników na testach rozumowania, co widać na przykładzie rezultatu Pathwaya na ARC-AGI-1.
Czy z tego wpisu wynika, że postęp w matematyce AI zwolni?
Autor nie stawia takiej tezy i osobno się przed nią zabezpiecza. Uważa za prawdopodobne, że modele pokonają opisaną przez niego przeszkodę, i to raczej szybko. Jego zastrzeżenie dotyczy sposobu, w jaki to nastąpi. Samo powiększanie modeli może nie wystarczyć, bo dane treningowe pokazują gotowe dowody, a nie proces dochodzenia do nich. Możliwe więc, że potrzebna będzie zmiana w treningu, a nie kolejna skala.
Podsumowanie
Wpis Gowersa jest rzadkim głosem. Pochodzi od czynnego matematyka i laureata Medalu Fieldsa, a nie od laboratorium ogłaszającego własny wynik. Nie neguje postępu i nie wieszczy ściany. Robi coś pożyteczniejszego: rozkłada głośne osiągnięcia na części i pyta, jakiego rodzaju są to osiągnięcia. Jego hipoteza brzmi, że wśród najmocniejszych wyników modeli przeważają przykłady i kontrprzykłady. Przypuszcza, że sprzyjają temu szeroka wiedza oraz możliwość szybkiego sprawdzenia wielu ścieżek. Podejrzewaną, a nie ustaloną przeszkodą pozostaje wyczucie kierunku, którego trudno wypatrzyć w danych treningowych, bo publikowane dowody ukrywają porzucone tropy. Autor sam podaje warunek, po którym pozna, że problem zniknął, i to jest w całym tekście najuczciwsze.
Newsletter · DevstockAcademy & Kodożercy
Bądź na bieżąco ze światem IT, AI i automatyzacji
Co wtorek: newsy z branży, praktyczne tipy i narzędzia które warto znać. Zero spamu.
