Что произошло
Французская 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. Открытые модели всё чаще догоняют закрытые в узких, но сложных задачах.
