Mistral публикува Leanstral, AI модел за вайб-кодиране с формална верификация

Компанията Mistral AI представи голям езиков модел Devstral, ориентиран към разработка на приложения (вайб-кодинг) и оптимизиран за формална верификация на кода. Предполага се, че Devstral може да се използва за създаване на AI асистенти, които не само генерират код, но и гарантират, че в него няма грешки.

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 $.

Източник: opennet.ru