Od počítania slovných úloh k porotám dôkazov: päť rokov AI matematiky

Matematika bola pre jazykové modely dlho zlomyseľným zrkadlom. Model dokázal napísať presvedčivý esej o teórii čísel, a vzápätí pokazil delenie, zamenil nutnú podmienku za postačujúcu alebo si v poslednom riadku odporoval. Jeho jazyk znel múdrejšie ako jeho výpočet.

Len za päť rokov sa ale zmenilo skoro všetko: úlohy, metriky, modely i predstava o tom, čo vlastne znamená „AI vyriešila matematický problém“. V roku 2021 sme merali, či jeden model na prvý pokus trafí krátku odpoveď. V roku 2026 sledujeme systémy, ktoré vytvárajú populáciu dôkazov, navzájom ich kritizujú, opravujú, púšťajú cez Python alebo Lean a až potom turnajovo vyberajú víťazov.

Tento text je technická história tej premeny. Nie rebríček značiek, ale mapa princípov: ktoré systémy v jednotlivých obdobiach vyhrávali, prečo vyhrávali a ktoré zdanlivo múdre nápady opakovane zlyhávali. Na konci ju prevediem do návrhu matematického režimu pre náš HyperFusion a experimenty na LUMI.

Hlavný záver: najväčšie skoky neprišli len z väčšieho modelu. Priniesli ich nové spôsoby využitia výpočtu: rozpísaný postup, diverzita kandidátov, hlasovanie, nástroje, verifikácia, cielená oprava a nakoniec orchestrácia celého dôkazového procesu.

Najskôr jedna nepríjemnosť: výsledky nie sú priamo porovnateľné

Číslo „90 % z matematiky“ môže znamenať štyri veľmi odlišné veci:

• model raz vygeneroval správne číslo;
• správna odpoveď sa objavila aspoň raz medzi stovkami pokusov;
• väčšina z mnohých riešení sa zhodla na správnom výsledku;
• formálny dôkaz prešiel kernelovým overovačom bez medzier.

Do toho vstupuje veľkosť modelu, prístup k nástrojom, počet vzoriek, dĺžka kontextu, časový limit, testovací hardvér, verejnosť dát a niekedy aj ľudská formalizácia zadania. Preto budem pri každom výsledku rozlišovať minimálne nasledujúce metriky:

Táto distinkcia je dôležitejšia ako poradie v tabuľke. Pokiaľ systém s 2 000 vzorkami porazí model na pass@1, neznamená to automaticky lepší základný model. Znamená to, že mal účinnejšiu kombináciu generátora, rozpočtu a selektora.

2021: MATH a GSM8K odhalili, že plynulosť nie je uvažovanie

MATH: súťažné úlohy ako studená sprcha

Benchmark MATH priniesol 12 500 súťažných stredoškolských úloh z algebry, geometrie, teórie čísel, pravdepodobnosti a ďalších oblastí. Každá mala nielen odpoveď, ale aj krokové riešenie. Vtedajšie veľké transformery dosahovali len jednotiek percent; autori uvádzali pásmo zhruba 2,9 až 6,9 %.

To bol kľúčový moment. Na bežných NLP benchmarkoch fungovalo škálovanie takmer ako univerzálny recept. MATH ukázal, že väčší jazykový model môže lepšie napodobniť formu matematického textu bez toho, aby spoľahlivo udrží dlhý reťazec závislostí. Chyba v prvom odhade sa v šiestom kroku zmenila na elegantne vysadený nezmysel.

Benchmark mal navyše neskôr zásadný kultúrny vplyv: zaviedol spoločný cieľ, na ktorom išlo merať tréning na matematických dátach, prompting, hlasovanie aj nástroje. Súčasne sa však postupne saturoval. Akonáhle sa test stane tréningovým kompasom pre celý odbor, prestáva byť neutrálnou krajinou.

GSM8K: jednoduchá aritmetika, ťažká jazyková štruktúra

V tom istom roku vznikol GSM8K: 8 500 slovných úloh na úrovni základnej školy, typicky s dvoma až ôsmimi krokmi. Nešlo o ťažkú ​​teóriu. Išlo o prevod príbehu na správnu postupnosť operácií.

Práve na GSM8K sa objavil jeden z najtrvanlivejších princípov celej histórie: generovať je jednoduchšie ako spoľahlivo vyberať. OpenAI nechalo model vyrobiť mnoho kandidátnych riešení a trénovalo verifier, ktorý ich radil. Zlepšenie verifiera mohlo mať podobný efekt ako dramatické zväčšenie generátora.

Lenže už vtedy sa ukázal budúci problém: s rastúcim počtom kandidátov sa objavujú riešenia, ktoré sú chybné, ale vedia verifier oklamať. Viac vzoriek pomáha iba do chvíle, kedy selektor rozoznáva kvalitu rýchlejšie, než generátor vyrába sofistikované chyby.

2022: model sa naučil „ukázať prácu“

Chain of Thought: medzivýsledky ako pracovná pamäť

Práca Chain-of-Thought Prompting ukázala, že niekoľko príkladov s rozpísaným postupom môže pri veľkom modeli vyvolať podstatne lepšie viackrokové riešenie. PaLM 540B s ôsmimi ukážkami dosiahol vtedajší špičkový výsledok na GSM8K.

Prečo to fungovalo? Nie preto, že by textový postup bol automaticky dôkazom. Generované tokeny vytvorili externú pracovnú plochu. Model nemusel všetky medzivýsledky držať v jednom skrytom výpočte; mohol sa na nich v ďalších krokoch podmieniť.

CoT ale zaviedol nebezpečný zvyk: zamieňať presvedčivo znejúci postup za verný záznam vnútorného uvažovania. Jazykový reťazec môže byť racionalizácia. Môže dôjsť k správnemu číslu chybnou cestou alebo k chybe až v poslednom prepise. CoT je výkonný generátor kandidáta, nie certifikát.

PRIELOM 1: OSEM UKÁZOK ZMENILO SPÔSOB VÝPOČTU

Chain of thought: model dostal niekoľko vyriešených príkladov a začal si medzivýsledky zapisovať do vlastného výstupu. Text sa stal externou pracovnou pamäťou. Bol to posun od jednorazového tipu k auditovateľnej trajektórii, ešte nie k dôkazu.

Self-consistency: jedna cesta je vzorka, nie verdikt

Self-consistency nahradila greedy dekódovanie jednoduchou myšlienkou: nasampluj viac rôznych postupov a marginalizuj ich cez konečný výsledok. Na GSM8K priniesla v pôvodnej práci zlepšenie o 17,9 percentuálneho bodu, na SVAMP o 11 a na AQuA o 12,2 bodu.

Algoritmus je takmer banálny:

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

Jeho sila stojí na predpoklade, že správna odpoveď má mnoho nezávislých ciest, zatiaľ čo omyly sú rozptýlené. Pokiaľ ale všetky vzorky zdieľajú rovnaký mylný stereotyp, väčšinové hlasovanie chybu len zosilní. Diverzita textu nie je to isté ako diverzita chýb.

PRIELOM 2: +17,9 PERCENTNÉHO BODU NA GSM8K

Self-consistency: nasamplovať rôzne postupy, z každého vytiahnuť konečnú odpoveď, previesť ekvivalentné zápisy do rovnakého tvaru a zvoliť najčastejší výsledok. Rovnaký princíp pridal 11 bodov na SVAMP a 12,2 bodu na AQuA.

Minerva: špecializácia dát plus test-time compute

Minerva nadviazala na PaLM a pokračovala v tréningu na desiatkach miliárd tokenov technického obsahu, vrátane matematických webov a arXívu. Minerva 540B dosiahla na MATH 50,3% s majority voting. V roku 2021 by také číslo pôsobilo absurdne.

Vyhrala kombinácia troch vecí:

1. silný základný model;
2. doménovo bohatý pokračovací pretraining;
3. desiatky až stovky nezávislých riešení pri inferencii.

To je prvý jasný historický vzorec: tréning určuje distribúciu dostupných stratégií, inferencia rozhoduje, koľko z nich prehľadáme.

2022 až 2024: kalkulačka sa vrátila do miestnosti

Jazykový model je dobrý v návrhu postupu, ale plytvanie jeho kapacitou na presné násobenie je podobné, ako keby matematik nesmel použiť papier. Ďalšia generácia systémov preto oddelila plánovanie od vykonania.

PAL: model píše program, runtime počíta

Program-Aided Language Models nechali LLM vygenerovať program a konečný výsledok zverili Pythonu. PAL s Codexom na GSM8K prekonal rádovo väčší PaLM s chain of thought o 15 percentuálnych bodov.

Rozdelenie práce je elegantné:

• model rozpozná entity a vzťahy;
• vytvorí symbolický alebo programový postup;
• deterministický runtime vykoná aritmetiku;
• systém vráti výsledok aj auditovateľnú stopu výpočtu.

Tým nezmiznú všetky chyby. Model môže zle preložiť zadanie alebo napísať program, ktorý korektne počíta nesprávnu veličinu. Nástroj však odstráni celú triedu numerických prerieknutí a umožní automatické testy.

PRIELOM 3: +15 PERCENTNÝCH BODOV NA GSM8K

PAL: model už nepočítal každé číslo token po tokene. Preložil vzťahy do programu, Python vykonal aritmetiku a výsledok sa vrátil do odpovede. Rozdelenie rolí porazilo rádovo väčší PaLM s čistým chain of thought.

ToRA: striedanie textu a nástrojov

ToRA nepoužíva nástroj len na konci. Model strieda prirodzený jazyk s volaním Pythonu či symbolického solveru, pozoruje výsledok a pokračuje. ToRA-7B dosiahla na MATH 44,6 % a variant ToRA-Code-34B prekročil 50 %.

Architektonicky je to dôležitejšie ako samotné číslo. Riešenie sa zmenilo z monológu na uzavretú slučku:

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

Táto slučka je predchodcom dnešných agentov. Rozdiel je iba v počte rolí av tom, či korekciu vykonáva ten istý model, iný model, alebo formálny systém.

DeepSeekMath: dáta, GRPO a malý model, ktorý už nie je malý schopnosťami

DeepSeekMath 7B pokračoval v pretrainingu na 120 miliardách matematických tokenov a zaviedol Group Relative Policy Optimization, neskôr známe ako GRPO. Bez nástrojov a hlasovania dosiahol na MATH 51,7%, so self-consistency 64 vzoriek 60,9%.

Zatiaľ čo Minerva ukázala silu obrieho špecializovaného modelu, DeepSeekMath ukázal, že kvalitný matematický korpus, cielený post-training a test-time sampling môžu dostať 7B model do oblasti, ktorá ešte nedávno patrila stovkám miliárd parametrov.

PRIELOM 4: +9,2 PERCENTNÉHO BODU VĎAKA 64 POKUSOM

DeepSeekMath: rovnaký 7B checkpoint mal 51,7 % na pass@1 a 60,9 % so self-consistency nad 64 vzorkami. Rozdiel presne ukazuje, koľko schopnosti už bolo v generátore, ale jeden pokus ju nevedel spoľahlivo vyťažiť.

Benchmark sa bráni: robustnosť, multimodalita a naozaj ťažké otázky

Akonáhle MATH a GSM8K začali byť príliš známe, vznikli testy, ktoré útočili na ich slabiny.

OlympiadBench: text nestačí

OlympiadBench obsahuje 8 476 bilingválnych multimodálnych úloh z matematiky a fyziky. Diagram už nie je dekorácia; nesie časť informácie. Pri uvedení dosiahol GPT-4V celkovo 17,97 %. Benchmark oddelil schopnosť čítať obraz, formalizovať situáciu a vykonať výpočet.

GSM-Symbolic: zmeň čísla a sleduj, čo zostane

GSM-Symbolic generuje symbolické varianty rovnakých šablón. Model teda nemôže ťažiť len z konkrétneho znenia známej otázky. Autori ukázali výraznú varianciu medzi numerickými inštanciami a veľké prepady po pridaní irelevantné informácie.

To je výstraha pre každý leaderboard: vysoké priemerné skóre nemusí znamenať invariantný algoritmus. Model môže mať naučené lokálne heuristiky, ktoré fungujú na typickom povrchu dát, ale rozpadajú sa pri malej transformácii.

FrontierMath: návrat otázky, ktorú model pravdepodobne nevidel

FrontierMath vznikol ako kolekcia nových, odborníkmi vytvorených problémov od vyššej univerzitnej po výskumnú úroveň. Pri uvedení v roku 2024 dosahovali vedúce modely najviac približne dvoch percent. Tu nepomohlo iba hladké napodobnenie olympiádneho štýlu.

Pri FrontierMath je zároveň nutné sledovať governance. Epoch AI neskôr vysvetlil, že časť otázok bola vytvorená na zákazku pre OpenAI a firma mala prístup ku všetkým okrem holdoutu. To neanuluje benchmark, ale mení interpretáciu výsledku. Provenancia a prístup k údajom sú súčasťou metriky.

2024: AIMO 1 a víťazstvo otvoreného 7B systému

Prvá Progress Prize súťaže AI Mathematical Olympiad prilákala cez tisíc tímov. Vyhral projekt Numina so systémom postaveným na DeepSeekMath-Base 7B. Vo verejnom riešení NuminaMath nebolo kúzlo v jedinej výzve modelu, ale v presne navrhnutom dátovom a inferenčnom reťazci.

Prečo súťažiaci nepoužili frontier API

Pravidlá boli zámerne iné ako bežný chatbotový benchmark. Hodnotilo sa na skrytej sade 50 úloh podobných AMC 12 a AIME, každá s celočíselnou odpoveďou. Povolené boli iba verejné modely s otvorenými váhami vydané pred rozhodným dátumom. Submission bežala ako offline Kaggle notebook bez internetu a externých API, na P100 alebo dvoch T4, najviac deväť hodín. Preto dáva zmysel 7B checkpoint: súťažilo sa v kvalite celého lokálneho systému pod pevným výpočtovým limitom, nie v tom, kto zavolá najdrahší uzavretý model. Podrobnosti uvádza technický popis víťazného riešenia.

Numina zhromaždila približne milión matematických problémov, čistila a anotovala riešenia, rozdelila tréning na klasický chain of thought a nástroj integrovanej reakcie a pri inferencii používala SC-TIR. Verejný opis uvádza približne 860 tisíc CoT príkladov a 70 tisíc TIR príkladov. Finálny DeepSeekMath-Base 7B prešiel plným fine-tuningom najskôr na CoT, potom na TIR, a bežal ako 8-bitový AutoGPTQ variant.

Replikovateľný víťazný recept: 48 kandidátov krát 4 cykly

Pre každú úlohu sa generovalo N = 48 kandidátov. Keď kandidát otvoril blok Pythona, generácia sa zastavila, kód sa spustil a výstup alebo traceback sa vrátil do kontextu. Tento cyklus mohol pokračovať najviac M = 4 kola. Nedokončené trajektórie sa zahodili. Z preživších výstupov sa vytiahli finálne celé čísla a vyhrala najčastejšia normalizovaná odpoveď. Väčšie N alebo M už v deväťhodinovom limite nepomohli.

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)

Normalizácia nie je LLM sudca. Deterministicky vytiahne požadované celé číslo, odstráni obal ako \boxed{...}, zjednotí ekvivalentné zápisy a odmietne neplatný formát. Potom sa spočítajú početnosti. Dĺžka ani presvedčivosť postupu nerozhodujú. Každý platný výsledok pridá jeden hlas svojmu číslu.

PRIELOM 5: 48 KANDIDÁTOV × 4 CYKLY PYTHÓNU

Numina SC-TIR: otvorený 7B model, 8bitová kvantizácia, 48 trajektórií, najviac štyri návraty z Pythona a jednoduchá väčšina normalizovaných čísel. Výsledok bol 29 správnych z 50.

Pôvodná schéma víťazného tímu Numina. Zdroj: project-numina/aimo-progress-prize, licencia Apache 2.0.

2025: AIMO 2 a okamih, kedy jednoduchá väčšina prestala stačiť

Druhú Progress Prize vyhral NVIDIA NemoSkills so skóre 34/50. Systém popisuje papier OpenMathReasoning a verejný repozitár NeMo Skills.

Pravidlá boli znova lokálne a offline. Súkromný test mal 50 úloh, notebook dostal štyri L4 GPU a päť hodín. Víťazný checkpoint vychádzal z Qwen2.5-14B-Base. Osem epoch sa učil na 2,2 milióna DeepSeek-R1 CoT riešení. Nasledovalo krátke TIR doladenie na 15 tisícoch príkladov, 400 krokov s learning rate 1e-5. Autori potom lineárne zlúčili checkpointy v pomere 0,3 × CoT + 0,7 × TIR.

Víťazná inferencia používala FP8, špekulatívne dekódovanie ReDrafter a takmer greedy teplotu 0. Model mohol vytvoriť až 16 kandidátov, ale systém ukončil beh, akonáhle sa prvé štyri až päť dokončených odpovedí zhodlo. Na jednu úlohu pridelil základ 350 sekúnd, nevyužitý čas presúval do rezervy a ťažkej úlohe mohol dať až 560 sekúnd. Python bol povolený najviac šesťkrát v jednej trajektórii, s timeoutom dve sekundy a vrátením iba prvých 200 znakov výstupu.

PRIELOM 6: 34 Z 50 POD PÄTIHODINOVÝM LIMITOM

Víťazný beh AIMO 2: 14B checkpoint zložený v pomere 0,3 CoT a 0,7 TIR, FP8, ReDrafter, až 16 takmer greed kandidátov a skoré ukončenie pri zhode štyroch až piatich odpovedí. Kľúčom nebol ďalší obrí model, ale práca s časom a rýchle nájdenie stabilnej väčšiny.

Dôležitá oprava: GenSelect nebol vo víťaznom behu

OpenMathReasoning skutočne vyvinul GenSelect, ktorý dostane problém a niekoľko úplných riešení a generatívne vyberá najsľubnejší kandidát. Víťazná AIMO 2 submission ho ale kvôli časovému limitu nepoužila. Predchádzajúca verzia tohto článku tieto dve časti papiera spájala, čo bolo nepresné.

Vo výskumnom protokole GenSelect pracoval so 64 vygenerovanými riešeniami. Opakovane dostával podmnožiny 16 kandidátov, výber sa vykonal 64-krát a finálna odpoveď vznikla väčšinou nad vybranými výsledkami. Nad 32 generácií začínal byť nestabilný, pretože sa všetky trajektórie nezmestili do jedného promptu. Je to cenná cesta pre ďalší výskum, ale nie je to recept, ktorý vyhral 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

Neskoršie spoločné vyhodnotenie AIMO ukázalo, ako silne výsledky rastú s rozpočtom. Kombinácia verejných systémov sa pri veľmi veľkom počte pokusov dostala na 47/50. To je pôsobivé, ale je to súčasne pass@veľmi-vysoké-k. Náklad a selekčný mechanizmus patria do titulku rovnako ako počet bodov.

Pravidlá troch AIMO súťažia v jednej tabuľke

Preto v AIMO nevyhráva automaticky najväčší dostupný frontier model. Pravidlá odstraňujú internet a proprietárne API, obmedzujú hardvér aj čas a vyžadujú lokálne kontrolovateľný artefakt. Súťaž tak meria model, kvantizáciu, serving, prácu s nástrojmi, time management aj selekciu ako jeden celok.

Paralelná vetva: od odpovede k dôkazu, ktorý prijme kernel

Klasické benchmarky často kontrolujú konečné číslo. Matematika ale nie je len odpoveď. V dôkaze je dôležité, že každý krok vyplýva z predchádzajúcich tvrdení.

miniF2F a PutnamBench

miniF2F priniesol 488 formálnych tvrdení v systémoch ako Lean, Metamath a Isabelle. PutnamBench rozšíril ambíciu na 1 692 formalizácií 640 vysokoškolských súťažných viet.

Formálne dokazovanie mení rozhodcu. Namiesto skórujúceho modelu nastúpi malý dôveryhodný kernel. Dôkaz buď typovo a logicky sedí, alebo nie. Tým mizne veľká časť estetického biasu, ale prichádza iná cena: prevod prirodzeného zadania do formálneho jazyka, vyhľadávanie knižničných lemmat a obrovský priestor možných taktík.

AlphaProof: striebro na IMO, ale s ručnou formalizáciou

V roku 2024 dosiahli AlphaProof a AlphaGeometry 2 dohromady 28 z 42 bodov na Medzinárodnej matematickej olympiáde, teda úroveň striebornej medaily. Vyriešili štyri zo šiestich úloh.

AlphaProof používal Lean a reinforcement learning na hľadanie formálnych dôkazov. Zadanie však muselo byť ručne prevedené do formálneho jazyka a niektoré úlohy systém spracovával až niekoľko dní. Výsledok teda nebol „chatbot vyriešil IMO v bežnej konverzácii“, ale triumf kombinácie formalizácie, vyhľadávania a verifikácie.

AlphaGeometry 2 naopak ťažila z úzkej domény a symbolického geometrického enginu. To je ďalšia historická lekcia: špecializovaný solver s tvrdými invarianciami môže v úzkej triede poraziť všeobecnejší systém.

DeepSeek-Prover a Goedel-Prover: kompilátor ako učiteľ

DeepSeek-Prover-V2 pracoval s rekurzívnym rozkladom na podciele a reinforcement learningom. Autori reportovali 88,9 % na miniF2F a 49 vyriešených problémov z 658 v PutnamBench, avšak pri 671B modeli as konkrétnym samplingovým rozpočtom.

Goedel-Prover-V2 ukázal, ako rýchlo sa účinnosť posunula. Jeho 8B variant reportuje 84,6% na miniF2F pri pass@32; 32B so self-correction 90,4 %. Oprava používa spätnú väzbu Lean kompilátora: model nedostane vágny „skús to znova“, ale konkrétne miesto a typ chyby.

PRIELOM 7: 90,4 % S KOMPILÁTOROM V KONTROLNEJ SLUČKE

Goedel-Prover-V2 32B: navrhne formálny dôkaz, Lean vráti presnú diagnostiku a model opraví lokalizovaný problém. Kernel nehodnotí štýl ani sebaistotu. Dôkaz buď prejde, alebo neprejde.

Zásadný princíp je univerzálny:

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

To je oveľa spoľahlivejšie ako požiadavka „skontroluj si odpoveď“, pretože kritika pochádza z iného mechanizmu ako generácie.

2025: zlato na IMO v prirodzenom jazyku

Google DeepMind oznámil, že pokročilý Gemini Deep Think dosiahol na IMO 2025 35 bodov zo 42, teda zlatej medailovej úrovne. Vyriešil päť zo šiestich úloh, riešenia boli oficiálne hodnotené a vznikli v prirodzenom jazyku počas súťažného limitu 4,5 hodiny.

Oproti AlphaProofu 2024 je kvalitatívny rozdiel obrovský: žiadna ručná formalizácia vstupu a žiadne viacdenné hľadanie. Deep Think využíva paralelné uvažovanie. Opäť teda nejde o jednu dokonale priamu stopu, ale o prehľadávanie viacerých ciest a ich kombináciu.

Je však fér povedať, že ide o uzavretý systém. Nepoznáme všetky detaily tréningu, počet interných kandidátov ani presný selektor. Výsledok je oficiálny, reprodukovateľnosť architektúry nie.

2026: AIMO 3 a koniec ilúzie, že súťaží len model

AIMO 3 priniesla 110 nových úloh od národnej olympiádnej po IMO úroveň, z algebry, kombinatoriky, geometrie a teórie čísel. Odpoveď mala päť číslic. Súťažiaci pracovali v offline notebooku s H100 a mohli stavať na otvorených váhach, napríklad gpt-oss-120b alebo Qwen3-Next.

Vyhlásenie víťazov uvádza poradie Exalted Joseph, varianceofx, SKobayak, TAMU-TACO a yemao ye medzi poprednými ocenenými. Zdôraznilo dva znaky novej éry: veľmi silný spoločný základný model s vysokou varianciou a zdieľané notebooky, ktoré rýchlo rozšírili najlepšie harnessy medzi tímami. Predné výsledky sa zhlukli. Rozdiel sa presunul od „mám tajný model“ k „viem z modelu konzistentne vyťažiť dobrých kandidátov a nenechať ich zahodiť“.

Pri prvom mieste nie je v oficiálnom súhrne jeden kompaktný recept s bezpečne citovateľným počtom kandidátov. Nechcem ho domýšľať. Presne replikovateľný je ale verejný systém druhého miesta varianceofx: lokálny gpt-oss-120b cez vLLM, stavový Jupyter Python sandbox, až osem paralelných pokusov a kombinácia jednoduchej väčšiny s entropicky váženým skóre. To je užitočnejšie ako neurčité tvrdenie, že „vyhral 120B model“.

PRIELOM 8: AŽ 8 POKUSOV A ENTROPICKY VÁŽENÝ HLAS

Verejný recept 2. miesta AIMO 3: gpt-oss-120b generuje až osem riešení s prístupom do stavového Pythonu. Zhoda odpovedí je hlavný signál, ale istota tokenov upravuje ich váhu. Kandidát teda nie je silnejší len preto, že je dlhý alebo štylisticky uhladený.

AIMO 3 tak potvrdila, že je nutné publikovať celý experimentálny kontrakt:

• checkpoint a kvantizáciu;
• sampling parametre;
• počet a dĺžku pokusov;
• normalizáciu odpovede;
• recovery pri nedokončenom reasoning výstupe;
• timeouty a využitie hardvéru;
• selekčný algoritmus.

Bez toho je skóre len výsledok neviditeľnej zmesi modelu a infraštruktúry.

Proof Pilot: 25 volaní jedného 32B modelu ako dôkazová organizácia

Po AIMO 3 bol spustený Proof Pilot zameraný na ľudsky čitateľné dôkazy. Víťazné otvorené riešenie Yi-Chia Chena je mimoriadne poučné práve tým, že sa nespolieha na obrovský proprietárny model. Verejný repozitár a deploy bundle popisujú model odvodený od OLMo 3.1 32B Think, s tokenizérom DeepSeek-V4, distiláciou z DeepSeek-V4-Flash a kvantizovaným servisom.

Najdôležitejšia je ale inferencia. Jeden checkpoint prepína role promptom:

1. šesť proverov vytvorí nezávislé dôkazy;
2. každý návrh dostane dva verifikačné posudky, teda dvanásť kritík;
3. tri refiner priechody opraví najsľubnejších kandidátov;
4. štyri selektory hlasujú o víťazovi.

Konfigurácia 6 / 2 / 3 / 4 znamená celkom 25 modelových volaní na úlohu. Vo zverejnenom harnesse je navyše watchdog, práca s veľmi dlhým kontextom, záchrana nedokončeného <think> bloku a fallbacky. To nie sú prevádzkové detaily pod čiarou. U reasoning modelu sú súčasťou algoritmu.

PRIELOM 9: 25 VOLANIE ROZDELENÝCH DO ŠTVOR PROFESÍ

Proof Pilot: 6 nezávislých dôkazov, 12 kritik, 3 cielené opravy a 4 selekčné hlasy. Dôležitý nie je iba počet vzoriek, ale poradie rolí a informácie, ktorú si medzi sebou odovzdávajú.

Modelový bundle reportuje na IMO-ProofBench v2 priemerné skóre 4,48/7pri Claude cross-checku a 3,808/7s DeepSeek graderom; učiteľský DeepSeek-V4-Flash je uvedený na 4,83/7. Rozdiel medzi dvoma gradermi je sám o sebe varovaním: u prirodzených dôkazov nie je judge obyčajný merací prístroj, ale ďalší model s vlastnou chybou.

Technicky je zaujímavý aj rozdiel medzi teacherom a študentom. Modelová karta uvádza približne 18,74 GB pre GPTQ variant oproti asi 65 GB v BF16. Schopnosť sa teda neprenášala len cez tvrdé odpovede, ale cez viacfázovú distiláciu a soft targets. Pri kompresii ale autori spomínajú sklony k opakovaniu a slučkám. Presne tento typ degradácie môže viacagentový systém násobiť, pokiaľ nemá watchdog.

Čo v histórii skutočne vyhrávalo

Tabuľka nie je jeden leaderboard. Každý riadok má iný dataset a rozpočet. Ukazuje však konzistentný trend: víťazia systémy, ktoré premenili nadbytočný výpočet na kontrolovanú diverzitu a kvalitný výber.

Čo naopak opakovane nefungovalo

1. „Nechaj model premýšľať dlhšie“ bez kontroly

Dlhší reasoning môže priniesť opravu, ale aj rumináciu, slučku a seba-utvrdenie. Zvlášť kvantizovaný model môže vytvoriť tisíce tokenov stále rovnaké chyby. Rozpočet bez verifikácie nie je garancia kvality.

2. Viac vzoriek bez merania oracle gapu

Ak oracle@64 = 90 %, ale selektor dosiahne 65%, problém nie je v generátore. Ďalšie vzorky môžu selektor ešte viac zahltiť. Najskôr je potrebné analyzovať, prečo správne riešenie nevyhráva.

3. Väčšina medzi modelmi s rovnakou chybou

Tri checkpointy z rovnakej rodiny, trénované na podobných dátach a vyzvané rovnakým promptom nie sú tri nezávislé hlasy. Sú to tri merania rovnakého biasu. Pre fúziu je niekedy cennejší slabší, ale odlišný solver ako ďalšia kópia najsilnejšieho.

4. Generatívny sudca ako jediný zdroj pravdy

LLM judge ľahko zamení dĺžku, sebaistotu alebo známy štýl za správnosť. Môže preferovať odpoveď rovnakej rodiny. Kde existuje Python, SymPy, unit test alebo Lean, musí mať tvrdý signál vyššiu prioritu ako estetický posudok.

5. Syntéza, ktorá „vylepší“ správny základ na nepoznanie

V interných testoch HyperFusion na DRACO sme videli extrémne zlyhanie starého generatívneho zlučovania: odpoveď GPT-5.5 s hodnotením 88,7 % sa po agresívnej kompresii prepadla na 13,9 % az približne 27 tisíc znakov zostalo 295. Syntetizér neurobil drobnú chybu; zničil dôkazný obsah.

Novšia stratégia v3augment najprv vyberie najsilnejší základ, zachová ho a iba cielene dopĺňa nekonfliktné poznatky. V danej sade dosiahla priemer 84,9 %, zatiaľ čo najlepšia jednotlivá surová odpoveď 81,6 %. Pre matematiku z toho vyplýva prísnejšie pravidlo: vyber a over; neprepisuj, pokiaľ nemáš lokalizovanú chybu.

6. Benchmark bez dátovej provencie

Výsledok bez informácie o dátume, verzii datasetu, prístupe k testu a spôsobe evaluácie starne zle. Pri matematických benchmarkoch je kontaminácia obzvlášť nebezpečná: známa úloha môže vyzerať ako generalizácia, aj keď ide o rekonštrukciu zapamätanej šablóny.

Ako by som z toho postavil HyperFusion Math

Doterajší HyperFusion používa panel modelov, anonymizovaného sudcu a syntetizátor. Pre všeobecné rešerše je select-and-augment rozumný. Pre exaktnú matematiku by som však pridal samostatný režim s poradím dôvery:

1. deterministický test: výpočet, substitúcia, numerická kontrola, invariancia;
2. formálny test: ak je úloha formalizovateľná a knižnica dostupná;
3. nezávislá kritika: hľadanie chýb v premise a úplnosti;
4. vážená zhoda: až ako doplnkový signál;
5. štýl a zrozumiteľnosť: posledný, nie prvý filter.

Skóre kandidáta môže mať napríklad tvar:

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

Kde:

• V_exec je výsledok kódu, substitúcie alebo testu;
• V_formal je prijatie formálnym overovačom;
• P_selector je pravdepodobnosť generatívneho selektora;
• w_i je váha riešiteľa odhadnutá na trénovacej časti;
• risk penalizuje parse fail, nedokončené uvažovanie, nepodložený krok alebo rozpor medzi dôkazom a odpoveďou.

Koeficienty nesmú vzniknúť na finálnom teste. Je potrebné dataset rozdeliť po rodinách úloh, nie náhodne po riadkoch, inak sa takmer rovnaké šablóny dostanú do tréningu aj testu.

Experiment, ktorý by som spustil ako ďalší na LUMI

Ak máme uložené odpovede viacerých lokálnych modelov, nemusíme najskôr utrácať ďalšie inferencie. Môžeme offline zmerať, ktoré kombinácie vôbec majú potenciál.

Fáza A: bez sudcu, iba z existujúcich odpovedí

Pre každý model a režim uložiť:

• normalizovanú finálnu odpoveď;
• správnosť;
• parse fail a truncation;
• dĺžku, čas, tokeny a pamäť;
• identifikátor rodiny modelu a režimu think/nothink.

Potom pre všetky dvojice, trojice a štvorice spočítať:

1. individuálny pass@1;
2. majority/weightedvote;
3. oracle@k: či mal pravdu aspoň jeden člen;
4. disagreement rate;
5. párovú koreláciu chýb;
6. výkon na kategóriách a obtiažnostiach;
7. cenu za ďalší percentuálny bod.

Najzaujímavejšie nie je kombinácia s najvyšším súčtom individuálnych skóre. Je to kombinácia s vysokým oracle ceiling a nízkou koreláciou chýb.

Fáza B: tréning selektora bez úniku

Rozdelenie by som navrhol takto:

Ak je dataset malý, použil by som nested cross-validation po typoch úloh. Pri 60 položkách typu GPQA-Diamond je interval neistoty široký; rozdiel niekoľkých bodov môže byť jediná otázka. Pre matematické benchmarky je ideálny výrazne väčší holdout.

Fáza C: drahý judge len tam, kde má informačnú hodnotu

Judge by som nevolal vždy. Spustil by som ho iba vtedy, keď:

• preživší kandidáti dávajú rôzne odpovede;
• tvrdé testy nerozhodli;
• oracle analýza ukazuje, že správne riešenie často existuje, ale jednoduché hlasovanie ho nevie nájsť.

Tým vznikne kaskáda: jednoduché otázky vyrieši lacná zhoda, výpočtové úlohy Python, formálne úlohy Lean a iba skutočné konflikty dostanú drahú porotu.

Konkrétny prvý panel

Pre prvý experiment by som zachoval náš navrhnutý trio panel Gemma-4-31B think + Qwen-27B nothink + GLM-5.2 Q4 nothink, pretože kombinuje odlišné režimy aj rodiny. Gemmu by som ale automaticky nemenoval sudcom len preto, že má najlepšie individuálne skóre. Najprv by som na historických odpovediach zmeral:

• koľkokrát Gemma opraví spor správne;
• koľkokrát preferuje vlastný štýl;
• aký je rozdiel medzi jej selection accuracy a jednoduchou väčšinou;
• či menší špecializovaný verifier neprinesie rovnaký výsledok lacnejšie.

Najsilnejší solver a najlepší sudca sú dve rôzne role. História GSM8K, GenSelect aj Proof Pilotu je v tomto prekvapivo konzistentná.

Čo sledovať namiesto jediného čísla

Pre každý experiment by som publikoval minimálne tento vektor:

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

Z neho je možné diagnostikovať, kde systém stráca:

• nízke oracle@k → chýba schopný generátor alebo diverzita;
• vysoké oracle@k, nízke selector@k→ zlyháva sudca;
• vysoké selector@k, nízke formal_or_exec_pass→ judge oceňuje plausibilitu;
• vysoké skóre, vysoký parse_fail_rate → pipeline je laboratórne silná, prevádzkovo krehká;
• malý zisk za násobne vyššie tokeny → test-time compute už má klesajúci výnos.

A čo práca z roku 2026?

Výskum sa rýchlo presúva od jednoduchého best-of-N k populáciám dôkazov. MaxProof napríklad popisuje jeden model v štyroch roliach: generátor, verifier, refiner a ranker. Používa populačné hľadanie a turnajovú selekciu. Autori preprintu reportujú 35/42na IMO 2025 a 36/42na USAMO 2026. Je dôležité dodať, že ide o autorský výsledok preprintu, nie oficiálny súťažný verdikt.

DeepMind pri systéme Aletheia popisuje cyklus generovania, overovania a revízie a rast výkonu s test-time compute. Trend je rovnaký: model sa mení z odpovedača na proces.

Súčasne sa ukazuje, že generatívne verifiery nie sú neutrálne. Práca o škálovanie generatívnych verifiérov upozorňuje na citlivosť k promptu a rozdiel medzi výberom správnej odpovede a hodnotením kvality dôkazu. Reinforcement learning môže zlepšiť procedurálne metriky bez toho, aby rovnako zlepší presnosť finálneho answer selection.

Preto bude podľa mňa ďalší rozhodujúci krok menej efektný ako „ešte väčší reasoning model“: kalibrovaná, heterogénna a auditovateľná verifikácia.

Záver: matematiku nevyhral jeden model, ale nový spôsob organizácie výpočtu

Od roku 2021 do roku 2026 sa opakuje jediný veľký príbeh.

MATH a GSM8K ukázali, že jazyková plynulosť nestačí. Chain of thought vytvoril pracovnú stopu. Self-consistency z jednej stopy urobila populáciu. PAL a ToRA zverili presný výpočet nástrojom. Numina ukázala silu otvoreného modelu, dát a hlasovania. Víťazný NeMo Skills spojil TIR, checkpoint merge, rýchle dekódovanie a early stop; jeho výskumná vetva GenSelect ukázala múdrejší výber pre budúce systémy. Lean zmenil kompilátor na rozhodcu. AlphaProof spojil formalizáciu s RL search. Gemini Deep Think priniesol zlato v prirodzenom jazyku. Proof Pilot ukázal, že jediný 32B checkpoint môže byť organizáciou so štyrmi profesiami.

Pre HyperFusion z toho neplynie, že máme slepo kopírovať 25 volaní na každú otázku. Plynie z toho niečo praktickejšie:

1. pestovať skutočnú diverzitu chýb, nie len viac textu;
2. merať oracle ceiling skôr, než kúpime drahšieho sudcu;
3. dávať tvrdému overeniu prednosť pred vkusom LLM;
4. opravovať lokalizovanú chybu, nie prepisovať správny základ;
5. oddeliť generátor, verifier, refiner a selector aj vtedy, keď ich fyzicky hrá jeden model;
6. uvádzať rozpočet inferencie rovnako viditeľne ako skóre;
7. chrániť test pred únikom pri učení váh a routingu.

Najlepší matematický systém budúcnosti možno nebude model, ktorý „vie najviac“. Bude to systém, ktorý najlepšie spozná, kedy nevie, kto z ostatných práve vie viac a ako to overiť skôr, než odpoveď pošle ďalej.

---

Primárne zdroje a reprodukčné materiály

• Hendrycks et al.: MATH
• Cobbe et al.: GSM8K a trénované verifiery
• Wei et al.: Chain-of-Thought Prompting
• Wang et al.: Self-Consistency
• Lewkowycz et al.: Minerva
• Gao et al.: PAL
• Gou et al.: ToRA
• Shao et al.: DeepSeekMath
• He et al.: OlympiadBench
• Mirzadeh et al.: GSM-Symbolic
• Epoch AI: FrontierMath
• Numina: AIMO 1 winning solution a technický rozbor 48 × 4 SC-TIR
• NVIDIA: AIMO 2 paper a NeMo Skills
• AIMO Prize: pravidlá a spustenie AIMO 3 a vyhlásenie víťazov
• varianceofx: reprodukčný recept 2. miesta AIMO 3
• DeepMind: AlphaProof a AlphaGeometry 2
• DeepMind: Gemini Deep Think na IMO 2025
• Zheng et al.: miniF2F
• Tsoukalas et al.: PutnamBench
• Ren et al.: DeepSeek-Prover-V2
• Goedel-LM: Goedel-Prover-V2
• Yi-Chia Chen: Proof Pilot code a deploy bundle
• Jiang et al.: LLM-Blender
• Wang et al.: Mixture-of-Agents
• DeepSeek-AI: DeepSeek-R1
• Chen et al.: MaxProof

Poznámka k číslam: každý výsledok v texte patrí ku konkrétnemu protokolu autorov. Pass@1, self-consistency, pass@k, oficiálne olympiádne body a LLM-judge skóre nie sú vzájomne zameniteľné. Pri preprintoch uvádzam výsledky ako tvrdenia autorov, nie ako nezávisle potvrdený rekord.