Що сталося
Французька Mistral AI випустила Leanstral 1.5 — відкриту модель для формальної верифікації мовою Lean 4. Модель поширюється за ліцензією Apache 2.0 і доступна на Hugging Face та через безкоштовний API (оголошено 4 липня 2026 року).
Деталі
- Архітектура: MoE-модель
Leanstral-1.5-119B-A6B— 119 млрд параметрів усього, близько 6 млрд активних. - Бенчмарки з формальної математики: 100% на miniF2F; 587 із 672 завдань PutnamBench (математична олімпіада Патнема); 87% на FATE-H (алгебра рівня магістратури) і 34% на FATE-X (докторський рівень).
- На верифікації коду модель просканувала 57 open-source репозиторіїв і знайшла п’ять раніше невідомих багів — зокрема переповнення в Rust-бібліотеці varinteger.
Що це означає
Формальна верифікація — це математичний доказ того, що код або теорема правильні без винятків. Раніше така робота була справою вузьких фахівців вручну; Leanstral показує, що LLM уже здатна доводити теореми й знаходити реальні баги в бойовому коді, а не лише розв’язувати навчальні завдання. Практичний наслідок для розробника: відкриту модель можна завантажити й запустити локально, отримавши інструмент, який ловить класи помилок, невидимі звичайним тестам, — переповнення, граничні випадки. Поки це нішевий інструмент для критичного коду (криптографія, фінанси, ядро ОС), але планку «що вміє відкрита модель» помітно піднято.
Контекст
Leanstral продовжує хвилю сильних open-weights релізів — услід за GLM-5.2 від Zhipu AI. Відкриті моделі дедалі частіше наздоганяють закриті у вузьких, але складних завданнях.
