Mistral выпустила ИИ для вайб-кодинга, который доказывает корректность кода

Leanstral — большая языковая модель, оптимизированная для разработки с формальной верификацией. Это первая открытая модель, поддерживающая язык Lean 4, который позволяет математически доказывать корректность кода.

Модель имеет 119 млрд параметров (6.5 млрд активируемых на токен), контекст 256k токенов и распространяется под лицензией Apache 2.0. Архив весит 121 ГБ, запускать можно локально через vllm, transformers или SGLang. На вход принимает текст и изображения, на выходе только текст.

В тестах FLTEval Leanstral обогнала все открытые модели (Qwen3.5, Kimi-K2.5, GLM5) и сравнялась с Claude Haiku/Sonnet, но уступила Claude Opus. Зато цена значительно ниже: один проход на Leanstral стоит $18, на Opus $1650. При 16 проходах Leanstral набирает 31.9 балла за $290, Opus - 39.6 баллов за те же деньги, но дороже.

Leanstral также интегрируется с инструментом Aeneas для верификации Rust-кода и может использоваться в open-source агенте mistral-vibe.

Источник: vk.com

Комментарии: