Mistral vydal Leanstral 1.5 pre formálne dôkazy v Lean 4

Mistral AI predstavil Leanstral 1.5, špecializovaný model pre formálne dokazovanie v systéme Lean 4. Firma ho opisuje ako otvorene dostupný model s licenciou Apache 2.0, ktorý má 119 miliárd celkových parametrov a pri inferencii aktivuje približne 6 miliárd z nich. Nejde teda o univerzálny chatbot, ale o model navrhnutý pre úzku, no čoraz dôležitejšiu oblasť: písanie, opravovanie a overovanie matematických dôkazov a vlastností kódu v prostredí, kde správnosť nakoniec kontroluje kompilátor alebo formálny verifikátor.

Podstatné je, že Mistral nepredáva Leanstral 1.5 iba ako ďalší model pre matematické úlohy. Jadrom oznámenia je spôsob práce: model má fungovať v slučke s nástrojmi, čítať spätnú väzbu z Lean kompilátora, opravovať dôkazy, dopĺňať pomocné lemy a pokračovať vo viacťahových úlohách. To posúva formálne dokazovanie bližšie k agentickému vývojárskemu workflowu. Model nedostane iba otázku a jednorazovo nevráti odpoveď; môže opakovane skúšať kroky, spúšťať kontrolu, učiť sa z chýb kompilácie a meniť súbory v repozitári.

Výsledky, ktoré Mistral uvádza, sú pre túto špecializovanú oblasť výrazné. Leanstral 1.5 podľa oznámenia saturuje benchmark miniF2F, vyriešil 587 zo 672 úloh PutnamBench a dosahuje nové najlepšie výsledky na benchmarkoch FATE-H a FATE-X z abstraktnej algebry. Pri praktickejšom benchmarku FLTEval, ktorý vychádza z reálnych pull requestov okolo formalizácie Fermatovej poslednej vety, má nový model zlepšiť pass@1 z 21,9 na 28,9 a pass@8 z 31,9 na 43,2. Tieto čísla treba čítať opatrne, pretože formálne benchmarky sa líšia rozpočtom na pokusy, dostupnými nástrojmi aj tým, či model dostáva prirodzeno-jazykové náznaky. Napriek tomu ukazujú, že špecializované modely pre verifikáciu už nie sú iba akademickou kuriozitou.

Zaujímavá je aj ekonomika pokusov. Mistral tvrdí, že Leanstral 1.5 rieši PutnamBench približne za štyri doláre na problém, zatiaľ čo niektoré porovnávané systémy používajú násobne vyšší výpočtový rozpočet. Ak sa tento pomer potvrdí mimo interných meraní, môže byť dôležitejší než samotné poradie v tabuľke. Formálne dôkazy a verifikácia kódu sú prakticky použiteľné iba vtedy, keď sa dajú spúšťať opakovane, nad veľkým počtom cieľov a nie iba ako drahá demonštrácia na vybraných úlohách.

Pre vývojárov je najpraktickejšia druhá časť oznámenia: Leanstral 1.5 nebol trénovaný len na statické theorem-proving úlohy, ale aj v prostredí podobnom kódovaciemu agentovi. Model môže pracovať so súborovým systémom, spúšťať shell príkazy, používať Lean language server, čítať typové informácie a opravovať ciele, ktoré sa objavia až počas kompilácie. To je bližšie realite väčších Lean projektov, kde problém často nespočíva v jednom izolovanom dôkaze, ale v navigácii cez existujúcu knižnicu, meniacich sa závislostiach a potrebe vytvoriť pomocný medzikrok bez rozbitia zvyšku projektu.

Mistral zároveň zverejňuje alebo odkazuje viacero sprievodných artefaktov. Váhy modelu sú dostupné na Hugging Face pod názvom mistralai/Leanstral-1.5-119B-A6B, model má byť dostupný aj cez API ako leanstral-1-5 a firma odkazuje na SafeVerify fork používaný na kontrolu správnosti. Dôležité je aj otvorenie FLTEval, pretože bez verejných, reprodukovateľných testov sa v tejto oblasti ťažko oddeľuje skutočný pokrok od selektívnych ukážok. Pri formálnych dôkazoch nestačí, že model vyzerá presvedčivo; výsledný dôkaz musí prejsť overením.

Pre širší AI trh je Leanstral 1.5 signálom, že modelové firmy hľadajú hodnotu mimo všeobecných konverzačných schopností. Formálne metódy sú menšia disciplína než bežné kódovanie, no majú vysokú hodnotu v kryptografii, bezpečnostne kritickom softvéri, čipoch, matematike a časti infraštruktúrneho softvéru. Ak model dokáže skrátiť čas od neformálnej myšlienky k overenému dôkazu, môže znížiť bariéru pre tímy, ktoré by si dnes plnohodnotné formálne overovanie nemohli dovoliť.

Zároveň nejde o náhradu ľudských expertov. Oznámenie samo ukazuje, že výkon závisí od test-time scalingu, počtu pokusov, nástrojového prostredia a presného nastavenia verifikácie. Model môže objaviť pomocný dôkaz alebo nájsť chybu v repozitári, ale výber správnej špecifikácie, interpretácia rizika a rozhodnutie, čo sa má vôbec dokazovať, ostáva na ľuďoch. V praxi môže byť Leanstral 1.5 najužitočnejší ako kopilot pre expertov na Lean, nie ako autonómny garant správnosti.

Pre slovenské firmy a výskumné tímy je táto správa zaujímavá najmä tam, kde sa stretáva AI, bezpečnosť a softvérové inžinierstvo. Otvorené váhy umožňujú experimentovať lokálne alebo v kontrolovanom prostredí, API znižuje vstupnú bariéru a licenčný model Apache 2.0 je priaznivejší pre komerčné prototypy než uzavreté experimentálne systémy. Najbližší praktický test však nebude v tom, či model vyrieši ďalší benchmark, ale či dokáže spoľahlivo pomáhať pri údržbe reálnych formálnych knižníc, pri verifikácii kritického kódu a pri hľadaní chýb, ktoré by bežné testy nezachytili.

Leanstral 1.5 preto zapadá do väčšieho trendu: AI agenti sa začínajú merať nielen podľa toho, čo napíšu, ale podľa toho, čo vedia overiť. V bežnom kódovaní sa úspech často hodnotí testami a review procesom; vo formálnom dokazovaní je latka tvrdšia, pretože výstup buď prejde kontrolou, alebo nie. Ak sa špecializované modely naučia efektívne pracovať s takýmto spätnoväzbovým signálom, môže to ovplyvniť aj širšie nástroje pre vývoj softvéru: menej dôvery v pekne znejúce odpovede a viac dôrazu na strojovo kontrolovateľné dôkazy, špecifikácie a opakovateľné hodnotenie.