Компания Mistral AI представила большую языковую модель Leanstral. Это проект для разработки приложений с помощью вайб‑кодинга и оптимизированный для формальной верификации кода. Предполагается, что Leanstral может применяться для создания ИИ‑ассистентов, позволяющих не просто генерировать код, но и гарантировать отсутствие в нём ошибок.
Leanstral стала первой открытой моделью, поддерживающей язык программирования Lean 4 и связанный с ним инструментарий для проверки математических доказательств. Lean 4 предоставляет возможности для математического доказательства корректности кода и его соответствия спецификации, что в контексте вайб‑кодинга позволяет подтвердить, что сгенерированный ИИ‑моделью код делает именно то, что задумано.
Модель Leanstral охватывает 119 миллиардов параметров (6.5 млрд активируемых параметров на токен), учитывает контекст в 256 тысяч токенов и опубликована под лицензией Apache 2.0. Загружаемый архив с Leanstral занимает 121 ГБ и пригоден для использования на локальных системах. Для локального запуска могут применяться библиотеки vllm, transformers и SGLang.
Для оценки возможностей ИИ-моделей с учётом качества проведения формальной верификации кода и написания математических доказательств разработан новый набор тестов FLTEval. В проведённых тестах модель Leanstral обогнала существующие открытые модели Qwen3.5 397B‑A17B, Kimi‑K2.5 1T‑A32B и GLM5 744B‑A40B, показала сходные результаты с моделями Claude Haiku 4.5 и Claude Sonnet 4.6 от компании Anthropic, но отстала от модели Claude Opus 4.6. В частности, модель Opus набрала 39.6 баллов, а Leanstral — 21.9 при одном проходе и 31.9 при 16 проходах. При этом затраты при использовании Opus составили $1650, а Leanstral — $18 при одном проходе и $290 при 16 проходах. Модель Haiku набрала 23 балла при затратах $184, а модель Sonnet — 23.7 при затратах $549.
