Od liczenia problemów tekstowych po jury dowodowe: pięć lat matematyki AI

Matematyka od dawna jest złowrogim zwierciadłem modeli językowych. Model mógłby napisać przekonujący esej na temat teorii liczb, a następnie natychmiast pomylić się z dzieleniem, pomylić warunek konieczny z wystarczającym lub zaprzeczyć sobie w ostatnim wersie. Jego język brzmiał mądrzej niż jego obliczenia.

Jednak w ciągu zaledwie pięciu lat zmieniło się prawie wszystko: zadania, wskaźniki, modele i pojęcie, co właściwie oznacza „AI rozwiązała problem matematyczny”. W 2021 r. sprawdzaliśmy, czy dany model trafia krótką odpowiedź już za pierwszym razem. W 2026 roku przyjrzymy się systemom, które tworzą populację dowodów, wzajemnie się krytykują, naprawiają je, uruchamiają w Pythonie lub Lean, a dopiero potem wybierają zwycięzcę turnieju.

Niniejszy tekst jest techniczną historią tej transformacji. Nie ranking marek, ale mapa zasad: które systemy zwyciężyły w każdym okresie, dlaczego zwyciężyły i które z pozoru mądre pomysły wielokrotnie zawiodły. Na koniec przełożę to na projekt w trybie matematycznym dla naszego HyperFusion i eksperymentów na LUMI.

Główny wniosek: największe skoki nie wynikały tylko z większego modelu. Spowodowały je nowe sposoby wykorzystania kalkulacji: szczegółowa procedura, różnorodność kandydatów, głosowanie, narzędzia, weryfikacja, ukierunkowana korekta i wreszcie orkiestracja całego procesu sprawdzającego.

Po pierwsze, jedna niedogodność: wyniki nie są bezpośrednio porównywalne

Liczba „90% w matematyce” może oznaczać cztery bardzo różne rzeczy:

• model wygenerował poprawną liczbę raz;
• prawidłowa odpowiedź pojawiła się przynajmniej raz spośród setek prób;
• większość z wielu rozwiązań zgodziła się na poprawny wynik;
• formalny dowód przeszedł walidator jądra bez luk.

Obejmuje to rozmiar modelu, dostęp do narzędzi, liczbę próbek, długość kontekstu, limit czasu, sprzęt testowy, publiczne dane i czasami sformalizowanie zadania przez człowieka. Dlatego dla każdego wyniku wyróżnię przynajmniej następujące metryki:

To rozróżnienie jest ważniejsze niż kolejność w tabeli. Jeśli system z 2000 próbkami pokonuje model przy przepustowości @1, nie oznacza to automatycznie lepszego modelu podstawowego. Oznacza to, że miał bardziej efektywną kombinację generatora, budżetu i selektora.

2021: MATH i GSM8K ujawniają, że płynność nie oznacza rozumowania

MATEMATYKA: problemy związane z konkurencją, takie jak zimny prysznic

Test porównawczy MATH przyniósł 12 500 konkurencyjnych problemów dla szkół średnich z algebry, geometrii, teorii liczb, prawdopodobieństwa i innych dziedzin. Każdy miał nie tylko odpowiedź, ale także rozwiązanie krok po kroku. Wielkie transformatory tamtych czasów osiągały jedynie jednostki procentowe; autorzy podali zakres od około 2,9 do 6,9%.

To był kluczowy moment. W przypadku popularnych testów porównawczych NLP skalowanie działało prawie jak przepis uniwersalny. MATH pokazał, że większy model językowy może lepiej naśladować formę tekstu matematycznego bez niezawodnego utrzymywania długiego łańcucha zależności. Błąd w pierwszym przypuszczeniu zamienił się w elegancko zasadzony nonsens w szóstym kroku.

Ponadto punkt odniesienia miał później duży wpływ kulturowy: ustanowił wspólny cel, względem którego można było mierzyć szkolenia dotyczące danych matematycznych, podpowiedzi, głosowania i narzędzi. Jednocześnie jednak stopniowo ulegał nasyceniu. Gdy test stanie się kompasem treningowym dla całego pola, przestaje być neutralnym krajobrazem.

GSM8K: prosta arytmetyka, ciężka struktura językowa

W tym samym roku utworzono GSM8K: 8500 zadań tekstowych na poziomie szkoły podstawowej, zazwyczaj składających się z dwóch do ośmiu kroków. To nie była trudna teoria. Chodziło o przełożenie historii na odpowiednią sekwencję działań.

To właśnie w GSM8K pojawiła się jedna z najtrwalszych zasad w całej historii: łatwiej wygenerować niż rzetelnie wybrać. OpenAI zleciło modelowi wygenerowanie wielu potencjalnych rozwiązań i wytrenowało weryfikatora, aby je uszeregował. Ulepszenie weryfikatora mogło mieć podobny efekt, jak radykalne zwiększenie generatora.

Ale już wtedy pojawił się przyszły problem: wraz ze wzrostem liczby kandydatów pojawiają się rozwiązania, które są błędne, ale mogą zmylić weryfikatora. Więcej próbek pomaga tylko do czasu, gdy selektor rozpozna jakość szybciej niż generator wygeneruje wyrafinowane błędy.

2022: model nauczył się „pokazywać pracę”

Łańcuch myślowy: wyniki pośrednie, takie jak pamięć robocza

Praca Chain-of-Thought Prompting pokazała, że kilka przykładów wraz ze szczegółową procedurą może skłonić do znacznie lepszego, wieloetapowego rozwiązania dla dużego modelu. PaLM 540B z ośmioma próbkami osiągnął najwyższy wówczas wynik w GSM8K.

Dlaczego to zadziałało? Nie dlatego, że procedura tekstowa jest automatycznie dowodem. Wygenerowane tokeny utworzyły zewnętrzny pulpit. Model nie musiał zawierać wszystkich wyników pośrednich w jednym ukrytym obliczeniu; mógłby od nich uzależnić swoje działania w kolejnych krokach.

Jednak CoT nabrało niebezpiecznego nawyku: mylenia przekonująco brzmiącej procedury z wiernym zapisem wewnętrznego rozumowania. Łańcuch językowy może być racjonalizacją. Do prawidłowego numeru można dojść niewłaściwą ścieżką lub błąd może wystąpić tylko w ostatniej transkrypcji. CoT to potężny generator kandydatów, a nie certyfikat.

PRZERWA 1: OSIEM PRZYKŁADÓW ZMIENIŁO METODĘ OBLICZEŃ

Łańcuch myślowy: model otrzymał kilka rozwiązanych przykładów i zaczął zapisywać wyniki pośrednie we własnych wynikach. Tekst stał się zewnętrzną pamięcią roboczą. Było to przejście od jednorazowej wskazówki do trajektorii możliwej do sprawdzenia, co nie było jeszcze dowodem.

Spójność: jedna ścieżka to próbka, a nie werdykt

Własna spójność zastąpiła zachłanne dekodowanie prostym pomysłem: próbuj wiele różnych procesów i marginalizuj je w stosunku do wyniku końcowego. Na GSM8K poprawił oryginalną pracę o 17,9 punktu procentowego, na SVAMP o 11, a na AQuA o 12,2 punktu.

Algorytm jest prawie trywialny:

solutions = sample(model, problem, n=64, temperature>0)
answers   = normalize_final_answers(solutions)
winner    = most_frequent(answers)
return best_explanation_among(solutions_with(winner))

Jego siła polega na założeniu, że poprawna odpowiedź wiedzie wiele niezależnych ścieżek, natomiast błędy są rozproszone. Jeśli jednak wszystkie próbki podzielają ten sam fałszywy stereotyp, głosowanie większością tylko pogłębi błąd. Różnorodność tekstu to nie to samo, co różnorodność błędów.

PRZEŁOM 2: +17,9 PUNKTÓW PROCENTOWYCH W GSM8K

Samospójność: wypróbuj różne procedury, wyodrębnij z każdej z nich ostateczną odpowiedź, przekonwertuj równoważne zapisy do tej samej postaci i wybierz najczęstszy wynik. Na tej samej zasadzie dodano 11 punktów na SVAMP i 12,2 punktu na AQuA.

Minerva: specjalizacja danych plus obliczenia w czasie testów

Minerva kontynuował prace nad PaLM i kontynuował szkolenia dotyczące dziesiątek miliardów tokenów treści technicznych, w tym witryn matematycznych i arXiv. Minerva 540B uzyskała 50,3% w teście MATH przy większości głosów. W 2021 roku taka liczba wydawałaby się absurdalna.

Wygrała kombinacja trzech rzeczy:

1. mocny model podstawowy;
2. szkolenie wstępne kontynuacyjne bogate w domeny;
3. dziesiątki do setek niezależnych rozwiązań podczas wnioskowania.

Oto pierwszy wyraźny wzór historyczny: szkolenie określa rozkład dostępnych strategii, wnioskowanie decyduje o tym, ile z nich przeszukamy.

2022 do 2024: Kalkulator wrócił do pokoju

Model językowy jest dobry w projektowaniu procedur, ale marnowanie jego zdolności do dokładnego mnożenia jest równoznaczne z niepozwoleniem matematykowi na używanie papieru. Dlatego następna generacja systemów oddzieliła planowanie od wykonania.

PAL: model pisze program, środowisko wykonawcze oblicza

Modele języków wspomaganych programowo zleciły LLM wygenerowanie programu i powierzenie końcowego wyniku Pythonowi. PAL z Codexem na GSM8K uzyskał lepsze wyniki niż znacznie większy PaLM z łańcuchem myślowym o 15 punktów procentowych.

Podział pracy jest elegancki:

• model rozpoznaje byty i relacje;
• tworzy procedurę symboliczną lub programową;
• deterministyczne środowisko wykonawcze wykona arytmetykę;
• system zwraca wynik oraz możliwy do sprawdzenia ślad obliczenia.

Nie powoduje to zniknięcia wszystkich błędów. Model może błędnie przetłumaczyć dane wejściowe lub napisać program, który poprawnie obliczy niewłaściwą wielkość. Narzędzie usuwa jednak całą klasę przesłuchów numerycznych i umożliwia automatyczne testy.

PRZEŁOM 3: +15 PUNKTÓW PROCENTOWYCH W GSM8K

PAL: model nie liczy już żetonu po żetonie. Przetłumaczył relacje na program, Python wykonał arytmetykę, a wynik został zwrócony w odpowiedzi. Podział ról pokonuje PaLM o rząd wielkości czystym łańcuchem myślowym.

ToRA: naprzemienny tekst i narzędzia

ToRA nie używa narzędzia tylko na końcu. Model zamienia język naturalny z wywołaniami Pythona lub solwera symbolicznego, obserwuje wynik i kontynuuje. ToRA-7B uzyskało 44,6% w teście MATH, a wariant ToRA-Code-34B przekroczył 50%.

Architektonicznie jest to ważniejsze niż sama liczba. Rozwiązanie zmieniło się z monologu na pętlę zamkniętą:

plán → kód → výsledek nástroje → revize plánu → další kód → odpověď

Ta pętla jest prekursorem dzisiejszych agentów. Różnica polega jedynie na liczbie ról i na tym, czy korekta dokonywana jest przez ten sam model, inny model, czy też system formalny.

DeepSeekMath: dane, GRPO i mały model, który nie ma już małych możliwości

DeepSeekMath 7B kontynuował wstępne szkolenie na 120 miliardach tokenów matematycznych i wdrożył Optymalizację zasad względnej grupy, znaną później jako GRPO. Bez narzędzi i głosowania osiągnął 51,7% w MATH, przy spójności wewnętrznej 64 próbek wynoszącej 60,9%.

Podczas gdy Minerva pokazała siłę gigantycznego, wyspecjalizowanego modelu, DeepSeekMath pokazała, że wysokiej jakości korpus matematyczny, ukierunkowane próbkowanie po treningu i próbkowanie w czasie testu mogą do niedawna przenieść model 7B w sferę setek miliardów parametrów.

** PRZEŁOM 4: +9,2 PUNKTÓW PROCENTOWYCH PRZEZ 64 PRÓBY**

DeepSeekMath: ten sam punkt kontrolny 7B miał 51,7% przy pierwszym przejściu i 60,9% przy samospójności w 64 próbkach. Różnica pokazuje dokładnie, ile zdolności było już w generatorze, ale jedna próba nie pozwoliła na ich niezawodne wydobycie.

Benchmark broni: solidności, multimodalności i naprawdę trudnych pytań

Ponieważ MATH i GSM8K stały się zbyt popularne, stworzono testy mające na celu wyeliminowanie ich słabych stron.

OlympiadBench: tekst to za mało

OlympiadBench zawiera 8476 dwujęzycznych, multimodalnych problemów matematycznych i fizycznych. Schemat nie jest już ozdobą; niesie część informacji. W momencie premiery GPT-4V uzyskał ogólny wynik 17,97%. W benchmarku wyodrębniono umiejętność odczytania obrazu, sformalizowania sytuacji i wykonania obliczeń.

GSM-Symboliczny: zmień numery i zobacz, co pozostanie

GSM-Symbolic generuje symboliczne warianty tych samych szablonów. Zatem model nie może czerpać korzyści jedynie z konkretnego sformułowania znanego pytania. Autorzy wykazali znaczną rozbieżność między przypadkami liczbowymi a dużymi spadkami po dodaniu nieistotnych informacji.

Jest to zastrzeżenie w przypadku każdej tabeli liderów: wysoki średni wynik niekoniecznie oznacza niezmienny algorytm. Model mógł nauczyć się lokalnych heurystyk, które działają na typowej powierzchni danych, ale załamują się pod wpływem niewielkiej transformacji.

FrontierMath: zwrócenie pytania, którego model prawdopodobnie nie widział

FrontierMath powstał jako zbiór nowych, stworzonych przez ekspertów problemów od poziomu wyższego uniwersytetu do poziomu badawczego. W momencie wprowadzenia na rynek w 2024 r. wiodące modele osiągnęły maksymalnie około 2% ceny. Nie pomogła tu jedynie płynna imitacja stylu olimpijskiego.

W przypadku FrontierMath trzeba też kontrolować zasady dostępu do danych. Epoch AI wyjaśnił później, że część pytań powstała na zamówienie OpenAI, a firma miała dostęp do wszystkich poza zbiorem holdout. Nie unieważnia to benchmarku, ale zmienia interpretację wyniku. Pochodzenie danych i dostęp do nich są częścią metryki.

2024: AIMO 1 i zwycięstwo otwartego systemu 7B

W pierwszym konkursie o Nagrodę Postępu AI Mathematical Olympiad wzięło udział ponad tysiąc zespołów. Wygrał projekt Numina z systemem zbudowanym na DeepSeekMath-Base 7B. W publicznym rozwiązaniu NuminaMath magia nie tkwiła w pojedynczym wyzwaniu modelu, ale w precyzyjnie zaprojektowanym łańcuchu danych i wnioskowań.

Dlaczego uczestnicy nie korzystali z frontier API

Zasady celowo różniły się od zwykłego benchmarku chatbota. Oceniano 50 ukrytych zadań podobnych do AMC 12 i AIME, każde z odpowiedzią całkowitą. Dozwolone były wyłącznie publiczne modele z otwartymi wagami wydane przed datą graniczną. Zgłoszenie działało jako notebook Kaggle offline, bez internetu i zewnętrznych API, na jednej P100 albo dwóch T4, najwyżej przez dziewięć godzin. Dlatego checkpoint 7B ma sens: konkurs mierzył jakość całego lokalnego systemu przy stałym budżecie obliczeniowym, a nie dostęp do najdroższego zamkniętego modelu. Szczegóły opisuje raport techniczny zwycięskiego rozwiązania.

Numina zebrała około miliona problemów matematycznych, oczyściła i opatrzyła rozwiązania, podzieliła szkolenie na klasyczny łańcuch myślowy i rozumowanie zintegrowane z narzędziami oraz wykorzystała SC-TIR do wnioskowania. W publicznym opisie wymieniono około 860 000 przykładów CoT i 70 000 przykładów TIR. Ostateczna wersja DeepSeekMath-Base 7B została w pełni dostrojona najpierw do CoT, a następnie do TIR i działała jako 8-bitowy wariant AutoGPTQ.

Powtarzalna zwycięska recepta: 48 kandydatów razy 4 cykle

Dla każdego zadania wygenerowano kandydatów N = 48. Kiedy kandydat otworzył blok Pythona, generowanie zostało zatrzymane, kod został uruchomiony, a dane wyjściowe lub śledzenie wróciły do ​​kontekstu. Cykl ten może trwać maksymalnie przez rundy M = 4. Niedokończone trajektorie zostały odrzucone. Z pozostałych wyników losowano końcowe liczby całkowite i wygrywała najczęstsza znormalizowana odpowiedź. Większe Nlub Mnie pomogły już w limicie dziewięciu godzin.

for candidate in 48_parallel_samples:
    repeat at most 4 times:
        generate until Python block or final answer
        if Python block: execute and append stdout or traceback

answers = normalize(extract_integer(completed_candidates))
return most_frequent(answers)

Normalizacja nie jest sędzią LLM. Deterministycznie wyodrębnia wymaganą liczbę całkowitą, usuwa opakowanie takie jak \boxed{...}, ujednolica równoważne zapisy i odrzuca nieprawidłowy format. Następnie zlicza się częstości. Długość ani perswazyjność rozwiązania nie mają znaczenia. Każdy prawidłowy wynik dodaje jeden głos swojej liczbie.

PRZEŁOM 5: 48 KANDYDATÓW × 4 CYKLE PYTHONA

Numina SC-TIR: otwarty model 7B, 8-bitowa kwantyzacja, 48 trajektorii, maksymalnie cztery zwroty z Pythona i zwykła większość znormalizowanych liczb. Wynik wyniósł 29 poprawnych na 50.

Oryginalny schemat zwycięskiej drużyny Numina. Źródło: project-numina/aimo-progress-prize, Apache License 2.0.

2025: AIMO 2 i moment, w którym zwykła większość już nie wystarczyła

Drugą nagrodę Progress zdobyła firma NVIDIA NemoSkills z wynikiem 34/50. System opisano w artykule OpenMathReasoning oraz w publicznym repozytorium NeMo Skills.

Zasady znów były lokalne i offline. Test prywatny miał 50 zadań, laptop dostał cztery procesory graficzne L4 i pięć godzin. Zwycięski punkt kontrolny został oparty na bazie Qwen2.5-14B. Osiem epok zostało przeszkolonych na 2,2 milionach rozwiązań DeepSeek-R1 CoT. Następnie nastąpiło krótkie strojenie TIR na 15 tysiącach przykładów, 400 kroków z szybkością uczenia się 1e-5. Następnie autorzy połączyli liniowo punkty kontrolne w stosunku 0,3 × CoT + 0,7 × TIR.

Zwycięskie wnioskowanie wykorzystało FP8, spekulatywne dekodowanie ReDrafter i niemal zachłanną temperaturę 0. Model mógł wygenerować do 16 kandydatów, ale system zakończył serię, gdy pierwsze cztery do pięciu kompletnych odpowiedzi pasowało. Na jedno zadanie przeznaczył bazę 350 sekund, niewykorzystany czas przesunął do rezerwy, a na trudne zadanie mógł przeznaczyć aż 560 sekund. Python mógł wystąpić maksymalnie sześć razy w jednej trajektorii, z limitem czasu wynoszącym dwie sekundy i zwróceniem tylko pierwszych 200 znaków danych wyjściowych.

PRZEŁOM 6: 34 Z 50 W LIMICIE PIĘCIU GODZIN

Zwycięski przebieg AIMO 2: checkpoint 14B złożony z 0,3 CoT i 0,7 TIR, FP8, ReDrafter, do 16 niemal zachłannych kandydatów i wczesne zakończenie po zgodności czterech do pięciu odpowiedzi. Kluczem nie był kolejny gigantyczny model, ale zarządzanie czasem i szybkie znalezienie stabilnej większości.

Ważna korekta: GenSelect nie był częścią zwycięskiego przebiegu

Rzeczywiście, OpenMathReasoning opracował GenSelect, który otrzymuje problem i kilka kompletnych rozwiązań i generatywnie wybiera najbardziej obiecującego kandydata. Jednak zwycięskie zgłoszenie AIMO 2 nie wykorzystało go ze względu na limit czasu. Poprzednia wersja tego artykułu łączyła dwie części artykułu, co było niedokładne.

W protokole badawczym GenSelect pracował z 64 wygenerowanymi rozwiązaniami. Wielokrotnie otrzymywał podzbiory po 16 kandydatów, selekcji dokonano 64 razy, a ostateczna odpowiedź została wygenerowana w większości na podstawie wyselekcjonowanych wyników. Powyżej 32 pokoleń zaczęło to być niestabilne, ponieważ nie wszystkie trajektorie mieściły się w jednym podpowiedzi. To cenny kierunek dalszych badań, ale to nie przepis zwyciężył w AIMO 2.

majority:  argmax_a  sum_i 1[normalize(answer_i) = a]
GenSelect: repeat 64 times select_one(problem, subset_of_16_solutions)
           then vote over normalized answers of selected solutions

Późniejsza wspólna ocena AIMO pokazała, jak silnie wyniki rosną wraz z budżetem. Kombinacja systemów publicznych dotarła do 47/50. w bardzo dużej liczbie prób. To imponujące, ale to także pass@very-high-k. Mechanizm obciążenia i selekcji jest zawarty w tytule i liczbie punktów.

Regulamin trzech zawodów AIMO w jednej tabeli

Dlatego też największy dostępny model frontierowy nie wygrywa automatycznie w AIMO. Reguły usuwają Internet i zastrzeżone interfejsy API, ograniczają sprzęt i czas oraz wymagają lokalnie kontrolowanego artefaktu. Konkurs mierzy zatem model, kwantyzację, obsługę, pracę z instrumentami, zarządzanie czasem i selekcję jako całość.

Oddział równoległy: od odpowiedzi do dowodu zaakceptowanego przez jądro

Klasyczne benchmarki często sprawdzają ostateczną liczbę. Ale matematyka nie jest jedyną odpowiedzią. W dowodzie ważne jest, aby każdy krok wynikał z poprzednich stwierdzeń.

miniF2F i PutnamBench

miniF2F dało 488 formalnych asercji w systemach takich jak Lean, Metamath i Isabelle. PutnamBench rozszerzył swoje ambicje do 1692 formalizacji 640 twierdzeń dotyczących konkurencji licencjackich.

Formalne dowody zmieniają sędziego. Małe zaufane jądro zastępuje model scoringowy. Dowód albo pasuje typologicznie i logicznie, albo nie. Eliminuje to dużą część uprzedzeń estetycznych, ale ma inną cenę: konwersję naturalnego wkładu na język formalny, poszukiwanie lematów bibliotecznych i ogromną przestrzeń możliwych taktyk.

AlphaProof: srebrny na IMO, ale z ręczną formalizacją

W 2024 roku AlphaProof i AlphaGeometry 2 łącznie zdobyły 28 z 42 punktów na Międzynarodowej Olimpiadzie Matematycznej, co stanowiło srebrny medal. Rozwiązali cztery z sześciu zadań.

AlphaProof wykorzystał Lean i uczenie się przez wzmacnianie do poszukiwania formalnych dowodów. Jednakże zadania trzeba było ręcznie konwertować na język formalny, a przetworzenie niektórych zadań przez system trwało kilka dni. Rezultatem nie był więc „rozwiązanie chatbota IMO w normalnej rozmowie”, ale triumf połączenia formalizacji, wyszukiwania i weryfikacji.

Z drugiej strony AlphaGeometry 2 skorzystała z wąskiej domeny i silnika geometrii symbolicznej. To kolejna lekcja historii: wyspecjalizowany moduł rozwiązywania z twardymi niezmiennikami może pokonać bardziej ogólny system w wąskiej klasie.

DeepSeek-Prover i Goedel-Prover: kompilator w roli nauczyciela

DeepSeek-Prover-V2 pracował z rekursywnym rozkładem na cele cząstkowe i uczeniem się przez wzmacnianie. Autorzy zgłosili 88,9% na miniF2F i 49 rozwiązało problemy z 658 w PutnamBench, ale z modelem 671B i przy określonym budżecie próbkowania.

Goedel-Prover-V2 pokazał, jak szybko zmieniała się wydajność. Jego wariant 8B zgłasza 84,6% na miniF2F przy przepustce@32; 32B z autokorektą 90,4%. Poprawka wykorzystuje informacje zwrotne od kompilatora Lean: model nie otrzymuje niejasnego komunikatu „spróbuj ponownie”, ale konkretną lokalizację i typ błędu.

PRZEŁOM 7: 90,4% Z KOMPILATOREM W PĘTLI STEROWANIA

Goedel-Prover-V2 32B: zaprojektuje formalny dowód, Lean zwróci dokładną diagnozę, a model naprawi zlokalizowany problem. Kernel nie ocenia stylu i pewności siebie. Dowód albo przechodzi, albo nie.

Podstawowa zasada jest uniwersalna:

navrhni důkaz → spusť ověřovač → přečti diagnostiku → oprav lokální chybu → znovu ověř

Jest to o wiele bardziej niezawodne niż prośba o „sprawdzenie odpowiedzi”, ponieważ krytyka pochodzi z innego mechanizmu niż pokolenie.

2025: złoty język naturalny w IMO

Google DeepMind ogłosił, że zaawansowany Gemini Deep Think osiągnął IMO 2025 35 punktów z 42, poziomu złotego medalu. Rozwiązał pięć z sześciu zadań, rozwiązania zostały poddane oficjalnej ocenie i stworzone w języku naturalnym w ramach konkursu wynoszącego 4,5 godziny.

W porównaniu z AlphaProof 2024 różnica jakościowa jest ogromna: nie ma ręcznego formowania danych wejściowych ani wielodniowego wyszukiwania. Deep Think wykorzystuje rozumowanie równoległe. Ponownie nie chodzi o jeden idealnie prosty tor, ale o przeszukiwanie wielu ścieżek i łączenie ich.

Można jednak śmiało powiedzieć, że jest to system zamknięty. Nie znamy wszystkich szczegółów szkolenia, liczby kandydatów wewnętrznych ani dokładnego selekcjonera. Wynik jest oficjalny, powtarzalność architektury nie.

2026: AIMO 3 i koniec złudzenia, że konkuruje tylko model

AIMO 3 przeniósł 110 nowych problemów z Ogólnopolskiej Olimpiady na poziom IMO, z algebry, kombinatoryki, geometrii i teorii liczb. Odpowiedź miała pięć cyfr. Konkurenci pracowali na laptopie offline z H100 i mogli budować na otwartych skalach, takich jak gpt-oss-120b lub Qwen3-Next.

Ogłoszenie zwycięzców wymienia Exalted Joseph, varianceofx, SKobayak, TAMU-TACO i yemao ye wśród najważniejszych wyróżnionych. Podkreśliło dwie cechy charakterystyczne nowej ery: bardzo mocny wspólny model podstawowy o dużej wariancji i współdzielone notesy, które szybko rozpowszechniają najlepsze uprzęże między zespołami. Wiodące wyniki zostały skupione. Różnica zmieniła się z „Mam tajny model” na „Mogę konsekwentnie wyodrębniać z modelu dobrych kandydatów i nie pozwolić im upaść”.

Po pierwsze, w oficjalnym podsumowaniu nie ma jednej zwartej recepty na bezpieczną liczbę kandydatów. Nie chcę go sobie wyobrażać. Ale system publiczny drugiego miejsca jest dokładnie replikowalny wariancjax: lokalny gpt-oss-120b przez vLLM, stanowa piaskownica Jupyter Python, do ośmiu równoległych prób i kombinacja zwykłej większości z punktacją ważoną entropią. Jest to bardziej przydatne niż niejasne twierdzenie, że „wygrał model 120B”.

Przełom 8: DO 8 PRÓB I ENTROPICZNIE WAŻONY GŁOS

Publiczna receptura AIMO 3 drugiego miejsca: gpt-oss-120b generuje do ośmiu rozwiązań z dostępem do stanowego języka Python. Zgodność odpowiedzi jest głównym sygnałem, ale pewność żetonów reguluje ich wagę. Zatem kandydat nie jest silniejszy tylko dlatego, że jest wysoki lub elegancki stylistycznie.

AIMO 3 potwierdziło zatem konieczność opublikowania całego kontraktu eksperymentalnego:

• punkt kontrolny i kwantyzacja;
• parametry próbkowania;
• liczba i długość prób;
• normalizacja odpowiedzi;
• odzyskiwanie w przypadku niepełnego wyniku rozumowania;
• przekroczenia limitu czasu i wykorzystanie sprzętu;
• algorytm selekcji.

Bez tego wynik byłby po prostu wynikiem niewidzialnego połączenia modelu i infrastruktury.

Proof Pilot: 25 połączeń jednego modelu 32B jako organizacji sprawdzającej

Po AIMO 3 wprowadzono pilotażowy dowód, którego celem było tworzenie dowodów czytelnych dla człowieka. Zwycięskie otwarte rozwiązanie Yi-Chia Chena jest niezwykle pouczające właśnie dlatego, że nie opiera się na gigantycznym, zastrzeżonym modelu. Publiczne repozytorium i deploy package opisują model wywodzący się z OLMo 3.1 32B Think, z tokenizerem DeepSeek-V4, destylacją z DeepSeek-V4-Flash i usługą kwantyzowaną.

Ale najważniejsze jest wyciąganie wniosków. Jeden punkt kontrolny przełącza role za pomocą monitu:

1. sześciu dowódców przedstawi niezależne dowody;
2. każdy wniosek otrzymuje dwie recenzje weryfikacyjne, czyli dwunastu krytyków;
3. trzy przejścia rafineryjne udoskonalają najbardziej obiecujących kandydatów;
4. czterech selektorów głosuje na zwycięzcę.

Konfiguracja 6 / 2 / 3 / 4 oznacza w sumie 25 wywołań modeli na zadanie. Ponadto opublikowana uprząż posiada watchdog, pracujący z bardzo długim kontekstem, zapisując niedokończony blok <think> i rezerwy. To nie są szczegóły operacyjne poniżej linii. W modelu rozumowania są one częścią algorytmu.

PRZEŁOM 9: 25 POWOŁAŃ PODZIELONYCH NA CZTERY ZAWODY

Proof Pilot: niezależne dowody 6, krytycy 12, ukierunkowane poprawki 3i głosy wybrane 4. Ważna jest nie tylko liczba próbek, ale kolejność ról i informacje, którymi się dzielą.

Pakiet modeli zgłasza średni wynik IMO-ProofBench v2 wynoszący 4,48/7w przypadku kontroli krzyżowej Claude i 3,808/7w przypadku równiarki DeepSeek; DeepSeek-V4-Flash nauczyciela jest wymieniony pod numerem 4.83/7.. Różnica między tymi dwoma równiarkami sama w sobie jest ostrzeżeniem: w przypadku dowodów naturalnych sędzia nie jest tylko urządzeniem pomiarowym, ale innym modelem z własnym błędem.

Z technicznego punktu widzenia różnica między nauczycielem a uczniem jest również interesująca. Model karty zawiera około 18,74 GB dla wariantu GPTQ w porównaniu do około 65 GB w BF16. Zatem zdolność ta została przekazana nie tylko poprzez twarde odpowiedzi, ale także poprzez destylację wielofazową i miękkie cele. Natomiast w przypadku kompresji autorzy wspominają o tendencjach do powtórzeń i zapętleń. To właśnie ten rodzaj degradacji może się powielać w systemie wieloagentowym, jeśli nie posiada modułu nadzorującego.

Co tak naprawdę zwyciężyło w historii

Tabela nie jest jedną tabelą liderów. Każdy wiersz ma inny zbiór danych i budżet. Pokazuje jednak stały trend: systemy, które przekształcają nadmiarowe obliczenia w kontrolowaną różnorodność i selekcję jakości, wygrywają.

Co wręcz przeciwnie, wielokrotnie nie działało

1. „Pozwól modelowi pomyśleć dłużej” bez sprawdzania

Dłuższe rozumowanie może przynieść korektę, ale także rozmyślania, zapętlenia i samowzmocnienie. Szczególnie skwantowany model może generować tysiące tokenów tego samego błędu w kółko. Budżet bez weryfikacji nie jest gwarancją jakości.

2. Więcej próbek bez pomiaru luki Oracle

Jeśli oracle@64 = 90 % ale selektor osiągnie 65%, problem nie leży w generatorze. Dodatkowe próbki mogą jeszcze bardziej przytłoczyć selektora. Przede wszystkim należy przeanalizować, dlaczego właściwe rozwiązanie nie wygrywa.

3. Większość wśród modeli z tym samym błędem

Trzy punkty kontrolne z tej samej rodziny, przeszkolone na podstawie podobnych danych i wywołane tym samym komunikatem, nie są trzema niezależnymi głosami. Są to trzy pomiary tego samego błędu systematycznego. W przypadku fuzji czasami słabszy, ale inny solwer jest cenniejszy niż kolejna kopia najsilniejszego.

4. Sędzia generatywny jako jedyne źródło prawdy

Sędzia LLM łatwo myli długość, pewność siebie lub znajomy styl z poprawnością. Może preferować tę samą reakcję rodziny. Tam, gdzie jest Python, SymPy, test jednostkowy lub Lean, twardy sygnał musi mieć pierwszeństwo przed oceną estetyczną.

5. Synteza, która „wzmocni” właściwy fundament do nierozpoznawalności

W wewnętrznych testach HyperFusion na platformie DRACO zaobserwowaliśmy skrajną porażkę starej fuzji generatywnej: odpowiedź GPT-5.5 oceniona na 88,7% spadła do 13,9% po agresywnej kompresji, pozostawiając 295 znaków z około 27 000 znaków. Syntezator nie popełnił najmniejszego błędu; zniszczona treść dowodowa.

Nowsza strategia v3augment najpierw wybiera najsilniejszą podstawę, zachowuje ją i jedynie celowo dodaje wiedzę niesprzeczną. Wynosił on średnio 84,9% w całym zestawie, podczas gdy najlepsza pojedyncza surowa odpowiedź wyniosła 81,6%. W przypadku matematyki wynika z tego bardziej rygorystyczna zasada: wybieraj i sprawdzaj; nie nadpisuj, chyba że masz zlokalizowany błąd.

6. Benchmark bez pochodzenia danych

Wynik bez informacji o dacie, wersji zbioru danych, dostępie do testu i sposobie oceny źle się starzeje. W przypadku wzorców matematycznych zanieczyszczenie jest szczególnie niebezpieczne: znajome zadanie może wyglądać jak uogólnienie, nawet jeśli jest rekonstrukcją zapamiętanego szablonu.

Jak zbudowałbym z tego HyperFusion Math

Obecna HyperFusion wykorzystuje panel modeli, anonimowego sędziego i syntezator. W przypadku wyszukiwań ogólnych rozsądne jest zaznaczanie i powiększanie. Jednak dla dokładnej matematyki dodałbym osobny tryb z stopniem ufności:

1. test deterministyczny: obliczenia, podstawienie, kontrola numeryczna, niezmienność;
2. test formalny: jeśli zadanie można sformalizować i dostępna jest biblioteka;
3. niezależna krytyka: szukanie błędów w założeniach i kompletności;
4. dopasowanie ważone: tylko jako dodatkowy sygnał;
5. styl i przejrzystość: ostatni filtr, nie pierwszy.

Na przykład wynik kandydata może mieć postać:

score(c) = α · V_exec(c)
         + β · V_formal(c)
         + γ · log P_selector(c)
         + δ · Σ_i w_i · 1[answer_i = answer_c]
         - λ · risk(c)

Gdzie:

• V_exec jest wynikiem kodu, podstawienia lub testu;
• V_formal oznacza akceptację przez weryfikatora formalnego;
• P_selector jest prawdopodobieństwem selektora generatywnego;
• w_i to waga rozwiązania oszacowana w części szkoleniowej;
• risk karze za niepowodzenie analizy, niekompletne rozumowanie, niepotwierdzony krok lub sprzeczność między dowodem a odpowiedzią.

Na teście końcowym nie można tworzyć współczynników. Konieczne jest podzielenie zbioru danych na rodziny zadań, a nie losowo na wiersze, w przeciwnym razie do trenowania i testowania trafią prawie te same szablony.

Eksperyment, który następnie przeprowadzę na LUMI

Jeśli mamy zapisane odpowiedzi kilku modeli lokalnych, nie musimy najpierw wyciągać dodatkowych wniosków. Możemy zmierzyć offline, które kombinacje mają w ogóle potencjał.

Faza A: bez oceniania, tylko na podstawie istniejących odpowiedzi

Dla każdego modelu i trybu zapisu:

• znormalizowana ostateczna odpowiedź;
• poprawność;
• analiza nie powiodła się i została obcięta;
• długość, czas, tokeny i pamięć;
• rodzina modeli i identyfikator trybu think/nothink.

Następnie dla wszystkich par, trójek i czwórek oblicz:

1. przepustka indywidualna@1;
2. większość/weightedgłosowanie;
3. oracle@k: czy przynajmniej jeden członek miał rację;
4. wskaźnik niezgody;
5. korelacja parami błędów;
6. wydajność w kategoriach i trudnościach;
7. cenę o kolejny punkt procentowy.

Zestawienie z największą sumą indywidualnych wyników nie należy do najciekawszych. Jest to połączenie wysokiego pułapu wyroczni i niskiej korelacji błędów.

Faza B: trening selektora bez wycieku danych

Sugerowałbym taki podział:

Jeśli zbiór danych jest mały, zastosowałbym zagnieżdżoną weryfikację krzyżową według typów zadań. Dla 60 elementów typu GPQA-Diamond przedział niepewności jest szeroki; różnica kilku punktów może oznaczać pojedyncze pytanie. W przypadku testów matematycznych idealny jest znacznie większy odstęp.

Faza C: kosztowny sędzia tylko tam, gdzie wnosi informację

Nie zawsze dzwoniłem do Sędziego. Uruchomiłbym to tylko wtedy, gdyby:

• kandydaci, którzy przeżyli, udzielają różnych odpowiedzi;
• twarde testy nie rozstrzygnęły;
• Analiza Oracle pokazuje, że często istnieje właściwe rozwiązanie, ale proste głosowanie nie może go znaleźć.

Tworzy to kaskadę: łatwe pytania są rozwiązywane w drodze taniego konsensusu, zadania obliczeniowe w Pythonie, formalne zadania Lean i tylko prawdziwe konflikty trafiają do kosztownego jury.

Konkretny pierwszy panel

Do pierwszego eksperymentu zachowałbym proponowany przez nas panel trio Gemma-4-31B myślę + Qwen-27B nie myślę + GLM-5.2 Q4 nie myślę, ponieważ łączy w sobie różne tryby i rodziny. Ale nie mianowałabym automatycznie Gemmy sędzią tylko dlatego, że ma najlepszy wynik indywidualny. Po pierwsze, oceniłbym reakcje historyczne:

• ile razy Gemma poprawnie koryguje spór;
• ile razy woli swój własny styl;
• jaka jest różnica między trafnością jego wyboru a większością zwykłą;
• czy mniejszy wyspecjalizowany weryfikator nie przyniesie tego samego wyniku taniej.

Najsilniejszy rozwiązujący i najlepszy sędzia to dwie różne role. Historia GSM8K, GenSelect i Proof Pilot jest w tym zaskakująco konsekwentna.

Co oglądać zamiast pojedynczego numeru

Dla każdego eksperymentu publikowałbym przynajmniej ten wektor:

pass@1
oracle@k
maj@k
selector@k
formal_or_exec_pass
mean_tokens
p95_latency
peak_memory_gb
parse_fail_rate
cost_per_correct

Można go wykorzystać do zdiagnozowania, gdzie system traci:

• niski oracle@k → brak zdolnego generatora lub różnorodności;
• wysoki oracle@k, niski selector@k→ sędzia nie zdał;
• wysoki selector@k, niski formal_or_exec_pass→ sędzia ocenia wiarygodność;
• wysoki wynik, wysoki parse_fail_rate → rurociąg jest wytrzymały laboratoryjnie i niestabilny w działaniu;
• mały zysk za wielokrotnie wyższe tokeny → obliczenia w czasie testu już przynoszą malejący zwrot.

A co z badaniami z 2026 roku?

Badania szybko przechodzą od prostych najlepszych z N do populacji opartych na dowodach. Na przykład MaxProof opisuje jeden model w czterech rolach: generator, weryfikator, rafiner i rankinger. Wykorzystuje wyszukiwanie populacji i selekcję turniejów. Autorzy raportu preprintu 35/42na IMO 2025 oraz 36/42na USAMO 2026. Warto dodać, że jest to autorski wynik preprintu, a nie oficjalny werdykt konkursu.

DeepMind dla systemu Aletheia opisuje cykl generowania, weryfikacji i rewizji oraz wzrost wydajności przy obliczeniach w czasie testowania. Trend jest ten sam: model zmienia się z respondenta w proces.

Jednocześnie okazuje się, że weryfikatory generatywne nie są neutralne. Praca nad skalowaniem weryfikatorów generatywnych zwraca uwagę na wrażliwość na szybkość reakcji oraz różnicę pomiędzy wyborem prawidłowej odpowiedzi a oceną jakości dowodu. Uczenie się przez wzmacnianie może poprawić wskaźniki proceduralne bez poprawy dokładności ostatecznego wyboru odpowiedzi.

Dlatego moim zdaniem kolejny decydujący krok będzie mniej skuteczny niż „jeszcze większy model rozumowania”: weryfikacja skalibrowana, heterogeniczna i audytowalna.

Wniosek: matematykę wygrał nie jeden model, ale nowy sposób organizacji obliczeń

W latach 2021 do 2026 powtarza się jedna wielka historia.

MATH i GSM8K pokazały, że biegłość językowa nie wystarczy. Łańcuch myśli stworzył ścieżkę pracy. Własna spójność zamieniła pojedynczy ślad w populację. PAL i ToRA pozostawiły dokładne obliczenia narzędziom. Numina pokazała siłę otwartego modelu, danych i głosowania. Zwycięskie umiejętności NeMo łączyły TIR, łączenie punktów kontrolnych, szybkie dekodowanie i wczesne zatrzymanie; jego dział badawczy GenSelect wykazał mądrzejszy dobór dla przyszłych systemów. Lean zmienił kompilator w sędziego. AlphaProof połączył formalizację z wyszukiwaniem RL. Gemini Deep Think osiągnęło złoto w języku naturalnym. Dowód Pilot pokazał, że pojedynczy punkt kontrolny 32B może stanowić organizację czterech zawodów.

W przypadku HyperFusion nie oznacza to, że musimy na ślepo kopiować 25 wywołań na każde pytanie. Prowadzi to do czegoś bardziej praktycznego:

1. kultywuj prawdziwą różnorodność błędów, a nie tylko więcej tekstu;
2. zmierz sufit Oracle, zanim kupimy droższego sędziego;
3. preferowanie twardej walidacji od talentu LLM;
4. popraw zlokalizowany błąd, a nie przepisz poprawną podstawę;
5. oddzielny generator, weryfikator, rafiner i selektor, nawet jeśli fizycznie odtwarza je jeden model;
6. podaj budżet wnioskowania równie wyraźnie jak wynik;
7. chroń test przed wyciekiem podczas nauki ciężarów i trasowania.

Najlepszy system matematyczny przyszłości może nie być modelem, który „wie najwięcej”. Będzie to system, który wie najlepiej kiedy nie wie, który z pozostałych po prostu wie więcej i jak to zweryfikować przed wysłaniem odpowiedzi dalej.

---

Źródła pierwotne i materiały reprodukcyjne

• Hendrycks i in.: MATH
• Cobbe i in.: GSM8K i przeszkoleni weryfikatorzy
• Wei i wsp.: Podpowiadanie łańcucha myśli
• Wang i in.: Self-Consistency
• Lewkowycz i in.: Minerva
• Gao i wsp.: PAL
• Gou i wsp.: ToRA
• Shao i wsp.: DeepSeekMath
• On i wsp.: OlympiadBench
• Mirzadeh i in.: GSM-Symbolic
• AI epoki: FrontierMath
• Numina: Zwycięskie rozwiązanie AIMO 1 i analiza techniczna 48 × 4 SC-TIR
• NVIDIA: Dokument AIMO 2 i Umiejętności NeMo
• Nagroda AIMO: regulamin i uruchomienie AIMO 3 oraz ogłoszenie zwycięzców
• wariancjaofx: przepis hodowlany 2 miejsce AIMO 3
• DeepMind: AlphaProof i AlphaGeometry 2
• DeepMind: Gemini Deep Think na IMO 2025
• Zheng i wsp.: miniF2F
• Tsoukalas i wsp.: PutnamBench
• Ren i wsp.: DeepSeek-Prover-V2
• Goedel-LM: Goedel-Prover-V2
• Yi-Chia Chen: Proof Pilot code i wdrożenie pakietu
• Jiang i wsp.: LLM-Blender
• Wang i in.: Mixture-of-Agents
• DeepSeek-AI: DeepSeek-R1
• Chen i wsp.: MaxProof

Uwaga do rycin: każdy wynik w tekście należy do konkretnego protokołu autorów. Pass@1, samokonsekwencja, pass@k, oficjalne punkty olimpijskie i wyniki sędziów LLM nie są zamienne. W przypadku preprintów wyniki przedstawiam jako twierdzenia autorów, a nie jako niezależnie potwierdzony zapis.