Mistral vydal Leanstral 1.5 — open-source model pre formálne dôkazy rieši 87 % PutnamBench problémov

Čo sa stalo

Mistral AI vydal Leanstral 1.5, aktualizáciu open-source modelu pre formálne dôkazy v Lean 4. Model je dostupný pod licenciou Apache 2.0 na Hugging Face aj ako bezplatný API endpoint na Mistral Labs.

Kontext a dopad

Formálne overovanie programov je kľúčové pre bezpečnosť kritického softvéru a matematické výskumy. Leanstral 1.5 saturuje celý miniF2F dataset (100 %) a rieši 587 z 672 PutnamBench problémov — nový state-of-the-art pre automatické dôkazovanie. Model objavil päť predtým neznámych bugov v 57 open-source repozitároch a dokázal time-complexity záruky pre implementáciu AVL stromov.

Detaily

• Parametre: 119B celkovo, 6B aktívnych (MoE architektúra)
• Kontext: 256k tokenov
• Licencia: Apache 2.0, váhy na Hugging Face
• miniF2F: 100 % (saturácia)
• PutnamBench: 587/672 (87 %)
• FATE-H: 87 %, FATE-X: 34 % (high school / graduate algebra)
• Reálna hodnota: 5 nových bugov v 57 repozitároch
• Prístup: zadarmo cez Mistral Labs API (leanstral-1-5)