иcтoчник: www.kv.by
Mistral представила Leanstral - крупную языковую модель, ориентированную на разработку приложений (вайб-кодинг) и формальную верификацию кода. Предполагается, что Leanstral сможет использоваться для создания AI-ассистентов, которые не только генерируют программный код, но и гарантируют его корректность.
Leanstral стала первой открытой моделью, поддерживающей язык Lean 4 и связанный с ним инструментарий для математических доказательств. Lean 4 обеспечивает возможности проверки корректности кода и соответствия спецификациям, что в контексте вайб-кодинга позволяет удостовериться, что сгенерированный моделью код делает именно то, что задумано. Модель насчитывает 119 миллиардов параметров (при этом 6,5 миллиарда активируемых параметров на токен), учитывает контекст в 256 тысяч токенов и распространяется под лицензией Apache 2.0. Архив Leanstral для загрузки занимает 121 ГБ и предназначен для локального использования.
Для локального запуска доступны библиотеки vllm, transformers и SGLang. Среди возможных применений Leanstral - вайб-разработка в открытом агенте 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, though уступает Claude Opus 4.6. Так, Opus набрал 39,6 балла против 21,9 у Leanstral при одном проходе и 31,9 при 16 проходах. При этом стоимость использования Opus составила 1650 долларов, а Leanstral - 18 долларов за один проход и 290 долларов за 16 проходов. Haiku набрал 23 балла за 184 доллара, Sonnet - 23,7 балла за 549 долларов.