Od počítání slovních úloh k porotám důkazů: pět let AI matematiky

Matematika byla pro jazykové modely dlouho zlomyslným zrcadlem. Model dokázal napsat přesvědčivý esej o teorii čísel, a vzápětí pokazil dělení, zaměnil nutnou podmínku za postačující nebo si v posledním řádku odporoval. Jeho jazyk zněl chytřeji než jeho výpočet.

Za pouhých pět let se ale změnilo skoro všechno: úlohy, metriky, modely i představa o tom, co vlastně znamená „AI vyřešila matematický problém“. V roce 2021 jsme měřili, zda jeden model na první pokus trefí krátkou odpověď. V roce 2026 sledujeme systémy, které vytvářejí populaci důkazů, navzájem je kritizují, opravují, pouštějí přes Python nebo Lean a teprve potom turnajově vybírají vítěze.

Tento text je technická historie té proměny. Ne žebříček značek, ale mapa principů: které systémy v jednotlivých obdobích vyhrávaly, proč vyhrávaly a které zdánlivě chytré nápady opakovaně selhávaly. Na konci ji převedu do návrhu matematického režimu pro náš HyperFusion a experimenty na LUMI.

Hlavní závěr: největší skoky nepřišly jen z většího modelu. Přinesly je nové způsoby využití výpočtu: rozepsaný postup, diverzita kandidátů, hlasování, nástroje, verifikace, cílená oprava a nakonec orchestrace celého důkazového procesu.

Nejdřív jedna nepříjemnost: výsledky nejsou přímo srovnatelné

Číslo „90 % z matematiky“ může znamenat čtyři velmi odlišné věci:

• model jednou vygeneroval správné číslo;
• správná odpověď se objevila alespoň jednou mezi stovkami pokusů;
• většina z mnoha řešení se shodla na správném výsledku;
• formální důkaz prošel kernelovým ověřovačem bez mezer.

Do toho vstupuje velikost modelu, přístup k nástrojům, počet vzorků, délka kontextu, časový limit, testovací hardware, veřejnost dat a někdy i lidská formalizace zadání. Proto budu u každého výsledku rozlišovat minimálně následující metriky:

Tato distinkce je důležitější než pořadí v tabulce. Pokud systém s 2 000 vzorky porazí model na pass@1, neznamená to automaticky lepší základní model. Znamená to, že měl účinnější kombinaci generátoru, rozpočtu a selektoru.

2021: MATH a GSM8K odhalily, že plynulost není uvažování

MATH: soutěžní úlohy jako studená sprcha

Benchmark MATH přinesl 12 500 soutěžních středoškolských úloh z algebry, geometrie, teorie čísel, pravděpodobnosti a dalších oblastí. Každá měla nejen odpověď, ale i krokové řešení. Tehdejší velké transformery dosahovaly jen jednotek procent; autoři uváděli pásmo zhruba 2,9 až 6,9 %.

To byl klíčový moment. Na běžných NLP benchmarcích fungovalo škálování téměř jako univerzální recept. MATH ukázal, že větší jazykový model může lépe napodobit formu matematického textu, aniž spolehlivě udrží dlouhý řetězec závislostí. Chyba v prvním odhadu se v šestém kroku změnila v elegantně vysázený nesmysl.

Benchmark měl navíc později zásadní kulturní dopad: zavedl společný cíl, na kterém šlo měřit trénink na matematických datech, prompting, hlasování i nástroje. Současně se však postupně saturoval. Jakmile se test stane tréninkovým kompasem pro celý obor, přestává být neutrální krajinou.

GSM8K: jednoduchá aritmetika, těžká jazyková struktura

Ve stejném roce vznikl GSM8K: 8 500 slovních úloh na úrovni základní školy, typicky s dvěma až osmi kroky. Nešlo o obtížnou teorii. Šlo o převod příběhu na správnou posloupnost operací.

Právě na GSM8K se objevil jeden z nejtrvanlivějších principů celé historie: generovat je snazší než spolehlivě vybírat. OpenAI nechalo model vyrobit mnoho kandidátních řešení a trénovalo verifier, který je řadil. Zlepšení verifieru mohlo mít podobný efekt jako dramatické zvětšení generátoru.

Jenže už tehdy se ukázal budoucí problém: s rostoucím počtem kandidátů se objevují řešení, která jsou chybná, ale umějí verifier oklamat. Více vzorků pomáhá pouze do chvíle, kdy selektor rozeznává kvalitu rychleji, než generátor vyrábí sofistikované chyby.

2022: model se naučil „ukázat práci“

Chain of Thought: mezivýsledky jako pracovní paměť

Práce Chain-of-Thought Prompting ukázala, že několik příkladů s rozepsaným postupem může u velkého modelu vyvolat podstatně lepší vícekrokové řešení. PaLM 540B s osmi ukázkami dosáhl tehdejšího špičkového výsledku na GSM8K.

Proč to fungovalo? Ne proto, že by textový postup byl automaticky důkazem. Generované tokeny vytvořily externí pracovní plochu. Model nemusel všechny mezivýsledky držet v jednom skrytém výpočtu; mohl se na ně v dalších krocích podmínit.

CoT ale zavedl nebezpečný zvyk: zaměňovat přesvědčivě znějící postup za věrný záznam vnitřního uvažování. Jazykový řetězec může být racionalizace. Může dojít ke správnému číslu chybnou cestou nebo k chybě až v posledním přepisu. CoT je výkonný generátor kandidáta, nikoli certifikát.

PRŮLOM 1: OSM UKÁZEK ZMĚNILO ZPŮSOB VÝPOČTU

Chain of thought: model dostal několik vyřešených příkladů a začal si mezivýsledky zapisovat do vlastního výstupu. Text se stal externí pracovní pamětí. Byl to posun od jednorázového tipu k auditovatelné trajektorii, ještě ne k důkazu.

Self-consistency: jedna cesta je vzorek, ne verdikt

Self-consistency nahradila greedy dekódování jednoduchou myšlenkou: nasampluj více různých postupů a marginalizuj je přes konečný výsledek. Na GSM8K přinesla v původní práci zlepšení o 17,9 procentního bodu, na SVAMP o 11 a na AQuA o 12,2 bodu.

Algoritmus je téměř banální:

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 síla stojí na předpokladu, že správná odpověď má mnoho nezávislých cest, zatímco omyly jsou rozptýlené. Pokud ale všechny vzorky sdílejí stejný mylný stereotyp, většinové hlasování chybu jen zesílí. Diverzita textu není totéž co diverzita chyb.

PRŮLOM 2: +17,9 PROCENTNÍHO BODU NA GSM8K

Self-consistency: nasamplovat různé postupy, z každého vytáhnout konečnou odpověď, převést ekvivalentní zápisy do stejného tvaru a zvolit nejčastější výsledek. Stejný princip přidal 11 bodů na SVAMP a 12,2 bodu na AQuA.

Minerva: specializace dat plus test-time compute

Minerva navázala na PaLM a pokračovala v tréninku na desítkách miliard tokenů technického obsahu, včetně matematických webů a arXivu. Minerva 540B dosáhla na MATH 50,3 % s majority voting. V roce 2021 by takové číslo působilo absurdně.

Vyhrála kombinace tří věcí:

1. silný základní model;
2. doménově bohatý pokračovací pretraining;
3. desítky až stovky nezávislých řešení při inferenci.

To je první jasný historický vzorec: trénink určuje distribuci dostupných strategií, inference rozhoduje, kolik z nich prohledáme.

2022 až 2024: kalkulačka se vrátila do místnosti

Jazykový model je dobrý v návrhu postupu, ale plýtvání jeho kapacitou na přesné násobení je podobné, jako kdyby matematik nesměl použít papír. Další generace systémů proto oddělila plánování od vykonání.

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

Program-Aided Language Models nechaly LLM vygenerovat program a konečný výsledek svěřily Pythonu. PAL s Codexem na GSM8K překonal řádově větší PaLM s chain of thought o 15 procentních bodů.

Rozdělení práce je elegantní:

• model rozpozná entity a vztahy;
• vytvoří symbolický nebo programový postup;
• deterministický runtime provede aritmetiku;
• systém vrátí výsledek i auditovatelnou stopu výpočtu.

Tím nezmizí všechny chyby. Model může špatně přeložit zadání nebo napsat program, který korektně počítá nesprávnou veličinu. Nástroj však odstraní celou třídu numerických přeřeknutí a umožní automatické testy.

PRŮLOM 3: +15 PROCENTNÍCH BODŮ NA GSM8K

PAL: model už nepočítal každé číslo token po tokenu. Přeložil vztahy do programu, Python provedl aritmetiku a výsledek se vrátil do odpovědi. Rozdělení rolí porazilo řádově větší PaLM s čistým chain of thought.

ToRA: střídání textu a nástrojů

ToRA nepoužívá nástroj jen na konci. Model střídá přirozený jazyk s voláním Pythonu či symbolického solveru, pozoruje výsledek a pokračuje. ToRA-7B dosáhla na MATH 44,6 % a varianta ToRA-Code-34B překročila 50 %.

Architektonicky je to důležitější než samotné číslo. Řešení se změnilo z monologu na uzavřenou smyčku:

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

Tato smyčka je předchůdcem dnešních agentů. Rozdíl je pouze v počtu rolí a v tom, zda korekci provádí tentýž model, jiný model, nebo formální systém.

DeepSeekMath: data, GRPO a malý model, který už není malý schopnostmi

DeepSeekMath 7B pokračoval v pretrainingu na 120 miliardách matematických tokenů a zavedl Group Relative Policy Optimization, později známé jako GRPO. Bez nástrojů a hlasování dosáhl na MATH 51,7 %, se self-consistency 64 vzorků 60,9 %.

Zatímco Minerva ukázala sílu obřího specializovaného modelu, DeepSeekMath ukázal, že kvalitní matematický korpus, cílený post-training a test-time sampling mohou dostat 7B model do oblasti, která ještě nedávno patřila stovkám miliard parametrů.

PRŮLOM 4: +9,2 PROCENTNÍHO BODU DÍKY 64 POKUSŮM

DeepSeekMath: stejný 7B checkpoint měl 51,7 % na pass@1 a 60,9 % se self-consistency nad 64 vzorky. Rozdíl přesně ukazuje, kolik schopnosti už bylo v generátoru, ale jeden pokus ji neuměl spolehlivě vytěžit.

Benchmark se brání: robustnost, multimodalita a opravdu těžké otázky

Jakmile MATH a GSM8K začaly být příliš známé, vznikly testy, které útočily na jejich slabiny.

OlympiadBench: text nestačí

OlympiadBench obsahuje 8 476 bilingvních multimodálních úloh z matematiky a fyziky. Diagram už není dekorace; nese část informace. Při uvedení dosáhl GPT-4V celkově 17,97 %. Benchmark oddělil schopnost číst obraz, formalizovat situaci a provést výpočet.

GSM-Symbolic: změň čísla a sleduj, co zůstane

GSM-Symbolic generuje symbolické varianty stejných šablon. Model tedy nemůže těžit jen z konkrétního znění známé otázky. Autoři ukázali výraznou varianci mezi numerickými instancemi a velké propady po přidání irelevantní informace.

To je výstraha pro každý leaderboard: vysoké průměrné skóre nemusí znamenat invariantní algoritmus. Model může mít naučené lokální heuristiky, které fungují na typickém povrchu dat, ale rozpadají se při malé transformaci.

FrontierMath: návrat otázky, kterou model pravděpodobně neviděl

FrontierMath vznikl jako kolekce nových, odborníky vytvořených problémů od vyšší univerzitní po výzkumnou úroveň. Při uvedení v roce 2024 dosahovaly vedoucí modely nejvýše přibližně dvou procent. Tady nepomohlo pouze hladké napodobení olympiádního stylu.

U FrontierMath je zároveň nutné sledovat governance. Epoch AI později vysvětlil, že část otázek byla vytvořena na zakázku pro OpenAI a firma měla přístup ke všem kromě holdoutu. To neanuluje benchmark, ale mění interpretaci výsledku. Provenance a přístup k datům jsou součást metriky.

2024: AIMO 1 a vítězství otevřeného 7B systému

První Progress Prize soutěže AI Mathematical Olympiad přilákala přes tisíc týmů. Vyhrál projekt Numina se systémem postaveným na DeepSeekMath-Base 7B. Ve veřejném řešení NuminaMath nebylo kouzlo v jediné výzvě modelu, ale v přesně navrženém datovém a inferenčním řetězci.

Proč soutěžící nepoužili frontier API

Pravidla byla záměrně jiná než běžný chatbotový benchmark. Hodnotilo se na skryté sadě 50 úloh podobných AMC 12 a AIME, každá s celočíselnou odpovědí. Povoleny byly pouze veřejné modely s otevřenými vahami vydané před rozhodným datem. Submission běžela jako offline Kaggle notebook bez internetu a externích API, na P100 nebo dvou T4, nejvýše devět hodin. Proto dává smysl 7B checkpoint: soutěžilo se v kvalitě celého lokálního systému pod pevným výpočetním limitem, ne v tom, kdo zavolá nejdražší uzavřený model. Podrobnosti uvádí technický popis vítězného řešení.

Numina shromáždila přibližně milion matematických problémů, čistila a anotovala řešení, rozdělila trénink na klasický chain of thought a tool-integrated reasoning a při inferenci používala SC-TIR. Veřejný popis uvádí přibližně 860 tisíc CoT příkladů a 70 tisíc TIR příkladů. Finální DeepSeekMath-Base 7B prošel plným fine-tuningem nejdříve na CoT, potom na TIR, a běžel jako 8bitová AutoGPTQ varianta.

Replikovatelný vítězný recept: 48 kandidátů krát 4 cykly

Pro každou úlohu se generovalo N = 48 kandidátů. Když kandidát otevřel blok Pythonu, generace se zastavila, kód se spustil a výstup nebo traceback se vrátil do kontextu. Tento cyklus mohl pokračovat nejvýše M = 4 kola. Nedokončené trajektorie se zahodily. Z přeživších výstupů se vytáhla finální celá čísla a vyhrála nejčastější normalizovaná odpověď. Větší N nebo M už v devítihodinovém limitu nepomohly.

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)

Normalizace není LLM soudce. Je to deterministická funkce, která vytáhne požadované celé číslo, odstraní obal jako \boxed{...}, sjednotí ekvivalentní zápisy a odmítne neplatný formát. Potom se spočítají četnosti. Kandidáti nehlasují podle délky ani přesvědčivosti postupu, každý platný výsledek přidá jeden hlas svému číslu.

PRŮLOM 5: 48 KANDIDÁTŮ × 4 CYKLY PYTHONU

Numina SC-TIR: otevřený 7B model, 8bitová kvantizace, 48 trajektorií, nejvýše čtyři návraty z Pythonu a prostá většina normalizovaných čísel. Výsledek byl 29 správných z 50.

Původní schéma vítězného týmu Numina. Zdroj: project-numina/aimo-progress-prize, licence Apache 2.0.

2025: AIMO 2 a okamžik, kdy prostá většina přestala stačit

Druhou Progress Prize vyhrál NVIDIA NemoSkills se skóre 34/50. Systém popisuje paper OpenMathReasoning a veřejný repozitář NeMo Skills.

Pravidla byla znovu lokální a offline. Soukromý test měl 50 úloh, notebook dostal čtyři L4 GPU a pět hodin. Vítězný checkpoint vycházel z Qwen2.5-14B-Base. Osm epoch se učil na 2,2 milionu DeepSeek-R1 CoT řešení. Následovalo krátké TIR doladění na 15 tisících příkladů, 400 kroků s learning rate 1e-5. Autoři pak lineárně sloučili checkpointy v poměru 0,3 × CoT + 0,7 × TIR.

Vítězná inference používala FP8, spekulativní dekódování ReDrafter a téměř greedy teplotu 0. Model mohl vytvořit až 16 kandidátů, ale systém ukončil běh, jakmile se první čtyři až pět dokončených odpovědí shodlo. Na jednu úlohu přidělil základ 350 sekund, nevyužitý čas přesouval do rezervy a těžké úloze mohl dát až 560 sekund. Python byl povolen nejvýše šestkrát v jedné trajektorii, s timeoutem dvě sekundy a vrácením pouze prvních 200 znaků výstupu.

PRŮLOM 6: 34 Z 50 POD PĚTIHODINOVÝM LIMITEM

Vítězný běh AIMO 2: 14B checkpoint složený v poměru 0,3 CoT a 0,7 TIR, FP8, ReDrafter, až 16 téměř greedy kandidátů a brzké ukončení při shodě čtyř až pěti odpovědí. Klíčem nebyl další obří model, ale práce s časem a rychlé nalezení stabilní většiny.

Důležitá oprava: GenSelect nebyl ve vítězném běhu

OpenMathReasoning skutečně vyvinul GenSelect, který dostane problém a několik úplných řešení a generativně vybírá nejslibnější kandidát. Vítězná AIMO 2 submission ho ale kvůli časovému limitu nepoužila. Předchozí verze tohoto článku tyto dvě části paperu spojovala, což bylo nepřesné.

Ve výzkumném protokolu GenSelect pracoval s 64 vygenerovanými řešeními. Opakovaně dostával podmnožiny 16 kandidátů, výběr se provedl 64krát a finální odpověď vznikla většinou nad vybranými výsledky. Nad 32 generací začínal být nestabilní, protože se všechny trajektorie nevešly do jednoho promptu. Je to cenná cesta pro další výzkum, ale není to recept, který vyhrál 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

Pozdější společné vyhodnocení AIMO ukázalo, jak silně výsledky rostou s rozpočtem. Kombinace veřejných systémů se při velmi velkém počtu pokusů dostala na 47/50. To je působivé, ale je to současně pass@velmi-vysoké-k. Náklad a selekční mechanismus patří do titulku stejně jako počet bodů.

Pravidla tří AIMO soutěží v jedné tabulce

Proto v AIMO nevyhrává automaticky největší dostupný frontier model. Pravidla odstraňují internet a proprietární API, omezují hardware i čas a vyžadují lokálně kontrolovatelný artefakt. Soutěž tak měří model, kvantizaci, serving, práci s nástroji, time management i selekci jako jeden celek.

Paralelní větev: od odpovědi k důkazu, který přijme kernel

Klasické benchmarky často kontrolují konečné číslo. Matematika ale není jen odpověď. V důkazu je důležité, že každý krok plyne z předchozích tvrzení.

miniF2F a PutnamBench

miniF2F přinesl 488 formálních tvrzení v systémech jako Lean, Metamath a Isabelle. PutnamBench rozšířil ambici na 1 692 formalizací 640 vysokoškolských soutěžních vět.

Formální dokazování mění rozhodčího. Místo skórujícího modelu nastoupí malý důvěryhodný kernel. Důkaz buď typově a logicky sedí, nebo ne. Tím mizí velká část estetického biasu, ale přichází jiná cena: převod přirozeného zadání do formálního jazyka, vyhledávání knihovních lemmat a obrovský prostor možných taktik.

AlphaProof: stříbro na IMO, ale s ruční formalizací

V roce 2024 dosáhly AlphaProof a AlphaGeometry 2 dohromady 28 z 42 bodů na Mezinárodní matematické olympiádě, tedy úrovně stříbrné medaile. Vyřešily čtyři ze šesti úloh.

AlphaProof používal Lean a reinforcement learning pro hledání formálních důkazů. Zadání však musela být ručně převedena do formálního jazyka a některé úlohy systém zpracovával až několik dnů. Výsledek tedy nebyl „chatbot vyřešil IMO v běžné konverzaci“, ale triumf kombinace formalizace, vyhledávání a verifikace.

AlphaGeometry 2 naopak těžila z úzké domény a symbolického geometrického enginu. To je další historická lekce: specializovaný solver s tvrdými invariancemi může v úzké třídě porazit obecnější systém.

DeepSeek-Prover a Goedel-Prover: kompilátor jako učitel

DeepSeek-Prover-V2 pracoval s rekurzivním rozkladem na podcíle a reinforcement learningem. Autoři reportovali 88,9 % na miniF2F a 49 vyřešených problémů z 658 v PutnamBench, ovšem u 671B modelu a s konkrétním samplingovým rozpočtem.

Goedel-Prover-V2 ukázal, jak rychle se účinnost posunula. Jeho 8B varianta reportuje 84,6 % na miniF2F při pass@32; 32B se self-correction 90,4 %. Oprava používá zpětnou vazbu Lean kompilátoru: model nedostane vágní „zkus to znovu“, ale konkrétní místo a typ chyby.

PRŮLOM 7: 90,4 % S KOMPILÁTOREM V KONTROLNÍ SMYČCE

Goedel-Prover-V2 32B: navrhne formální důkaz, Lean vrátí přesnou diagnostiku a model opraví lokalizovaný problém. Kernel nehodnotí styl ani sebejistotu. Důkaz buď projde, nebo neprojde.

Zásadní princip je univerzální:

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

To je mnohem spolehlivější než požadavek „zkontroluj si odpověď“, protože kritika pochází z jiného mechanismu než generace.

2025: zlato na IMO v přirozeném jazyce

Google DeepMind oznámil, že pokročilý Gemini Deep Think dosáhl na IMO 2025 35 bodů ze 42, tedy zlaté medailové úrovně. Vyřešil pět ze šesti úloh, řešení byla oficiálně hodnocena a vznikla v přirozeném jazyce během soutěžního limitu 4,5 hodiny.

Oproti AlphaProofu 2024 je kvalitativní rozdíl obrovský: žádná ruční formalizace vstupu a žádné vícedenní hledání. Deep Think využívá paralelní uvažování. Opět tedy nejde o jednu dokonale přímou stopu, ale o prohledávání více cest a jejich kombinaci.

Je však fér říci, že jde o uzavřený systém. Neznáme všechny detaily tréninku, počet interních kandidátů ani přesný selektor. Výsledek je oficiální, reprodukovatelnost architektury nikoli.

2026: AIMO 3 a konec iluze, že soutěží jen model

AIMO 3 přinesla 110 nových úloh od národní olympiádní po IMO úroveň, z algebry, kombinatoriky, geometrie a teorie čísel. Odpověď měla pět číslic. Soutěžící pracovali v offline notebooku s H100 a mohli stavět na otevřených vahách, například gpt-oss-120b nebo Qwen3-Next.

Vyhlášení vítězů uvádí pořadí Exalted Joseph, varianceofx, SKobayak, TAMU-TACO a yemao ye mezi předními oceněnými. Zdůraznilo dva znaky nové éry: velmi silný společný základní model s vysokou variancí a sdílené notebooky, které rychle rozšířily nejlepší harnessy mezi týmy. Přední výsledky se shlukly. Rozdíl se přesunul od „mám tajný model“ k „umím z modelu konzistentně vytěžit dobré kandidáty a nenechat je zahodit“.

U prvního místa není v oficiálním souhrnu jeden kompaktní recept s bezpečně citovatelným počtem kandidátů. Nechci ho domýšlet. Přesně replikovatelný je ale veřejný systém druhého místa varianceofx: lokální gpt-oss-120b přes vLLM, stavový Jupyter Python sandbox, až osm paralelních pokusů a kombinace prosté většiny s entropicky váženým skóre. To je užitečnější než neurčité tvrzení, že „vyhrál 120B model“.

PRŮLOM 8: AŽ 8 POKUSŮ A ENTROPICKY VÁŽENÝ HLAS

Veřejný recept 2. místa AIMO 3: gpt-oss-120b generuje až osm řešení s přístupem do stavového Pythonu. Shoda odpovědí je hlavní signál, ale jistota tokenů upravuje jejich váhu. Kandidát tedy není silnější jen proto, že je dlouhý nebo stylisticky uhlazený.

AIMO 3 tak potvrdila, že je nutné publikovat celý experimentální kontrakt:

• checkpoint a kvantizaci;
• sampling parametry;
• počet a délku pokusů;
• normalizaci odpovědi;
• recovery při nedokončeném reasoning výstupu;
• timeouty a využití hardwaru;
• selekční algoritmus.

Bez toho je skóre jen výsledek neviditelné směsi modelu a infrastruktury.

Proof Pilot: 25 volání jednoho 32B modelu jako důkazová organizace

Po AIMO 3 byl spuštěn Proof Pilot zaměřený na lidsky čitelné důkazy. Vítězné otevřené řešení Yi-Chia Chena je mimořádně poučné právě tím, že nespoléhá na obří proprietární model. Veřejný repozitář a deploy bundle popisují model odvozený od OLMo 3.1 32B Think, s tokenizerem DeepSeek-V4, distilací z DeepSeek-V4-Flash a kvantizovaným servisem.

Nejdůležitější je ale inference. Jeden checkpoint přepíná role promptem:

1. šest proverů vytvoří nezávislé důkazy;
2. každý návrh dostane dva verifikační posudky, tedy dvanáct kritik;
3. tři refiner průchody opraví nejslibnější kandidáty;
4. čtyři selektory hlasují o vítězi.

Konfigurace 6 / 2 / 3 / 4 znamená celkem 25 modelových volání na úlohu. Ve zveřejněném harnessu je navíc watchdog, práce s velmi dlouhým kontextem, záchrana nedokončeného <think> bloku a fallbacky. To nejsou provozní detaily pod čarou. U reasoning modelu jsou součástí algoritmu.

PRŮLOM 9: 25 VOLÁNÍ ROZDĚLENÝCH DO ČTYŘ PROFESÍ

Proof Pilot: 6 nezávislých důkazů, 12 kritik, 3 cílené opravy a 4 selekční hlasy. Důležitý není pouze počet vzorků, ale pořadí rolí a informace, kterou si mezi sebou předávají.

Modelový bundle reportuje na IMO-ProofBench v2 průměrné skóre 4,48/7 při Claude cross-checku a 3,808/7 s DeepSeek graderem; učitelský DeepSeek-V4-Flash je uveden na 4,83/7. Rozdíl mezi dvěma gradery je sám o sobě varováním: u přirozených důkazů není judge pouhý měřicí přístroj, ale další model s vlastní chybou.

Technicky je zajímavý i rozdíl mezi teacherem a studentem. Modelová karta uvádí přibližně 18,74 GB pro GPTQ variantu proti asi 65 GB v BF16. Schopnost se tedy nepřenášela jen přes tvrdé odpovědi, ale přes vícefázovou distilaci a soft targets. U komprese ale autoři zmiňují sklony k opakování a smyčkám. Přesně tento typ degradace může víceagentní systém násobit, pokud nemá watchdog.

Co v historii skutečně vyhrávalo

Tabulka není jeden leaderboard. Každý řádek má jiný dataset a rozpočet. Ukazuje však konzistentní trend: vítězí systémy, které proměnily nadbytečný výpočet v kontrolovanou diverzitu a kvalitní výběr.

Co naopak opakovaně nefungovalo

1. „Nech model přemýšlet déle“ bez kontroly

Delší reasoning může přinést opravu, ale také ruminaci, smyčku a sebe-utvrzení. Zvlášť kvantizovaný model může vytvořit tisíce tokenů stále stejné chyby. Rozpočet bez verifikace není garance kvality.

2. Více vzorků bez měření oracle gapu

Pokud oracle@64 = 90 %, ale selektor dosáhne 65 %, problém není v generátoru. Další vzorky mohou selektor ještě více zahltit. Nejdřív je potřeba analyzovat, proč správné řešení nevyhrává.

3. Většina mezi modely se stejnou chybou

Tři checkpointy ze stejné rodiny, trénované na podobných datech a vyzvané stejným promptem nejsou tři nezávislé hlasy. Jsou to tři měření stejného biasu. Pro fúzi je někdy cennější slabší, ale odlišný solver než další kopie nejsilnějšího.

4. Generativní soudce jako jediný zdroj pravdy

LLM judge snadno zamění délku, sebejistotu nebo známý styl za správnost. Může preferovat odpověď stejné rodiny. Kde existuje Python, SymPy, unit test nebo Lean, musí mít tvrdý signál vyšší prioritu než estetický posudek.

5. Syntéza, která „vylepší“ správný základ k nepoznání

V interních testech HyperFusion na DRACO jsme viděli extrémní selhání starého generativního slučování: odpověď GPT-5.5 s hodnocením 88,7 % se po agresivní kompresi propadla na 13,9 % a z přibližně 27 tisíc znaků zůstalo 295. Syntetizér neudělal drobnou chybu; zničil důkazní obsah.

Novější strategie v3augment nejprve vybere nejsilnější základ, zachová ho a pouze cíleně doplňuje nekonfliktní poznatky. V dané sadě dosáhla průměru 84,9 %, zatímco nejlepší jednotlivá surová odpověď 81,6 %. Pro matematiku z toho plyne přísnější pravidlo: vyber a ověř; nepřepisuj, pokud nemáš lokalizovanou chybu.

6. Benchmark bez datové provenance

Výsledek bez informace o datu, verzi datasetu, přístupu k testu a způsobu evaluace stárne špatně. U matematických benchmarků je kontaminace obzvlášť nebezpečná: známá úloha může vypadat jako generalizace, i když jde o rekonstrukci zapamatované šablony.

Jak bych z toho postavil HyperFusion Math

Dosavadní HyperFusion používá panel modelů, anonymizovaného soudce a syntetizér. Pro obecné rešerše je select-and-augment rozumný. Pro exaktní matematiku bych však přidal samostatný režim s pořadím důvěry:

1. deterministický test: výpočet, substituce, numerická kontrola, invariance;
2. formální test: pokud je úloha formalizovatelná a knihovna dostupná;
3. nezávislá kritika: hledání chyb v premise a úplnosti;
4. vážená shoda: až jako doplňkový signál;
5. styl a srozumitelnost: poslední, nikoli první filtr.

Skóre kandidáta může mít napří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ýsledek kódu, substituce nebo testu;
• V_formal je přijetí formálním ověřovačem;
• P_selector je pravděpodobnost generativního selektoru;
• w_i je váha řešitele odhadnutá na trénovací části;
• risk penalizuje parse fail, nedokončené uvažování, nepodložený krok nebo rozpor mezi důkazem a odpovědí.

Koeficienty nesmějí vzniknout na finálním testu. Je potřeba dataset rozdělit po rodinách úloh, ne náhodně po řádcích, jinak se téměř stejné šablony dostanou do tréninku i testu.

Experiment, který bych spustil jako další na LUMI

Máme-li uložené odpovědi více lokálních modelů, nemusíme nejdřív utrácet další inference. Můžeme offline změřit, které kombinace vůbec mají potenciál.

Fáze A: bez soudce, pouze z existujících odpovědí

Pro každý model a režim uložit:

• normalizovanou finální odpověď;
• správnost;
• parse fail a truncation;
• délku, čas, tokeny a paměť;
• identifikátor rodiny modelu a režimu think/nothink.

Potom pro všechny dvojice, trojice a čtveřice spočítat:

1. individuální pass@1;
2. majority/weighted vote;
3. oracle@k: zda měl pravdu alespoň jeden člen;
4. disagreement rate;
5. párovou korelaci chyb;
6. výkon na kategoriích a obtížnostech;
7. cenu za další procentní bod.

Nejzajímavější není kombinace s nejvyšším součtem individuálních skóre. Je to kombinace s vysokým oracle ceiling a nízkou korelací chyb.

Fáze B: trénink selektoru bez úniku

Rozdělení bych navrhl takto:

Pokud je dataset malý, použil bych nested cross-validation po typech úloh. U 60 položek typu GPQA-Diamond je interval nejistoty široký; rozdíl několika bodů může být jediná otázka. Pro matematické benchmarky je ideální výrazně větší holdout.

Fáze C: drahý judge jen tam, kde má informační hodnotu

Judge bych nevolal vždy. Spustil bych ho pouze tehdy, když:

• přeživší kandidáti dávají různé odpovědi;
• tvrdé testy nerozhodly;
• oracle analýza ukazuje, že správné řešení často existuje, ale jednoduché hlasování ho neumí najít.

Tím vznikne kaskáda: snadné otázky vyřeší levná shoda, výpočetní úlohy Python, formální úlohy Lean a pouze skutečné konflikty dostanou drahou porotu.

Konkrétní první panel

Pro první experiment bych zachoval náš navržený trio panel Gemma-4-31B think + Qwen-27B nothink + GLM-5.2 Q4 nothink, protože kombinuje odlišné režimy i rodiny. Gemmu bych ale automaticky nejmenoval soudcem jen proto, že má nejlepší individuální skóre. Nejprve bych na historických odpovědích změřil:

• kolikrát Gemma opraví spor správně;
• kolikrát preferuje vlastní styl;
• jaký je rozdíl mezi jejím selection accuracy a prostou většinou;
• zda menší specializovaný verifier nepřinese stejný výsledek levněji.

Nejsilnější solver a nejlepší soudce jsou dvě různé role. Historie GSM8K, GenSelect i Proof Pilotu je v tomto překvapivě konzistentní.

Co sledovat místo jediného čísla

Pro každý experiment bych publikoval minimálně 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 něj lze diagnostikovat, kde systém ztrácí:

• nízké oracle@k → chybí schopný generátor nebo diverzita;
• vysoké oracle@k, nízké selector@k → selhává soudce;
• vysoké selector@k, nízké formal_or_exec_pass → judge oceňuje plausibilitu;
• vysoké skóre, vysoký parse_fail_rate → pipeline je laboratorně silná, provozně křehká;
• malý zisk za násobně vyšší tokeny → test-time compute už má klesající výnos.

A co práce z roku 2026?

Výzkum se rychle přesouvá od jednoduchého best-of-N k populacím důkazů. MaxProof například popisuje jeden model ve čtyřech rolích: generátor, verifier, refiner a ranker. Používá populační hledání a turnajovou selekci. Autoři preprintu reportují 35/42 na IMO 2025 a 36/42 na USAMO 2026. Je důležité dodat, že jde o autorský výsledek preprintu, nikoli oficiální soutěžní verdikt.

DeepMind u systému Aletheia popisuje cyklus generování, ověřování a revize a růst výkonu s test-time compute. Trend je stejný: model se mění z odpovídače na proces.

Současně se ukazuje, že generativní verifiery nejsou neutrální. Práce o škálování generativních verifierů upozorňuje na citlivost k promptu a rozdíl mezi výběrem správné odpovědi a hodnocením kvality důkazu. Reinforcement learning může zlepšit procedurální metriky, aniž stejně zlepší přesnost finálního answer selection.

Proto bude podle mě další rozhodující krok méně efektní než „ještě větší reasoning model“: kalibrovaná, heterogenní a auditovatelná verifikace.

Závěr: matematiku nevyhrál jeden model, ale nový způsob organizace výpočtu

Od roku 2021 do roku 2026 se opakuje jediný velký příběh.

MATH a GSM8K ukázaly, že jazyková plynulost nestačí. Chain of thought vytvořil pracovní stopu. Self-consistency z jedné stopy udělala populaci. PAL a ToRA svěřily přesný výpočet nástrojům. Numina ukázala sílu otevřeného modelu, dat a hlasování. Vítězný NeMo Skills spojil TIR, checkpoint merge, rychlé dekódování a early stop; jeho výzkumná větev GenSelect ukázala chytřejší výběr pro budoucí systémy. Lean změnil kompilátor v rozhodčího. AlphaProof spojil formalizaci s RL search. Gemini Deep Think přinesl zlato v přirozeném jazyce. Proof Pilot ukázal, že jediný 32B checkpoint může být organizací o čtyřech profesích.

Pro HyperFusion z toho neplyne, že máme slepě kopírovat 25 volání na každou otázku. Plyne z toho něco praktičtějšího:

1. pěstovat skutečnou diverzitu chyb, ne jen více textu;
2. měřit oracle ceiling dřív, než koupíme dražšího soudce;
3. dávat tvrdému ověření přednost před vkusem LLM;
4. opravovat lokalizovanou chybu, ne přepisovat správný základ;
5. oddělit generátor, verifier, refiner a selector i tehdy, když je fyzicky hraje jeden model;
6. uvádět rozpočet inference stejně viditelně jako skóre;
7. chránit test před únikem při učení vah a routingu.

Nejlepší matematický systém budoucnosti možná nebude model, který „ví nejvíc“. Bude to systém, který nejlépe pozná, kdy neví, kdo z ostatních právě ví víc a jak to ověřit dřív, než odpověď pošle dál.

---

Primární 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: pravidla a spuštění AIMO 3 a vyhlášení vítězů
• varianceofx: reprodukční recept 2. místa 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 číslům: každý výsledek v textu patří ke konkrétnímu protokolu autorů. Pass@1, self-consistency, pass@k, oficiální olympiádní body a LLM-judge skóre nejsou vzájemně zaměnitelné. U preprintů uvádím výsledky jako tvrzení autorů, nikoli jako nezávisle potvrzený rekord.