Devstral стала первой открытой моделью, поддерживающей язык программирования Lean 4 и связанный с ним инструментарий для проверки математических доказательств. Lean 4 предоставляет возможности для математического доказательства корректности кода и его соответствия спецификации, что в контексте вайб-кодинга позволяет подтвердить, что сгенерированный AI-моделью код делает именно то, что задумано.
Модель охватывает 119 миллиардов параметров (6.5 млрд активируемых параметров на токен), учитывает контекст в 256 тысяч токенов и опубликована под лицензией Apache 2.0. Загружаемый архив с Leanstral занимает 121 ГБ и пригоден для использования на локальных системах. Для локального запуска могут применяться библиотеки vllm, transformers и SGLang.
Среди прочего модель может применяться для вайб-разработки в открытом агенте mistral-vibe, а также интегрироваться с инструментарием Aeneas для верификации кода на языке Rust. В качестве входных параметров принимается текст и изображения, на выходе выдаётся только текст. Поддерживается анализ содержимого изображений.
Для оценки возможностей AI-моделей с учётом качества проведения формальной верификации кода и написания математических доказательств разработан новый набор тестов 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.
Источник: http://www.opennet.ru/opennews/art.shtml?num=65005