Firma Mistral AI przedstawiła dużą model językowy Devstral, zaprojektowany do tworzenia aplikacji (wib-kodowanie) i zoptymalizowany do formalnej weryfikacji kodu. Zakłada się, że Devstral może być stosowany do tworzenia asystentów AI, którzy nie tylko generują kod, ale także gwarantują brak błędów w nim.
Devstral stała się pierwszym otwartym modelem obsługującym język programowania Lean 4 oraz powiązane narzędzia do weryfikacji dowodów matematycznych. Lean 4 oferuje możliwości matematycznego dowodzenia poprawności kodu i jego zgodności ze specyfikacją, co w kontekście wib-kodowania umożliwia potwierdzenie, że wygenerowany kod przez model AI robi dokładnie to, co zaplanowano.
Model obejmuje 119 miliardów parametrów (6,5 mld aktywowanych parametrów na token), uwzględnia kontekst w 256 tysiącach tokenów i jest opublikowany na licencji Apache 2.0. Pobierany archiwum Leanstral zajmuje 121 GB i nadaje się do wykorzystania na lokalnych systemach. Do lokalnego uruchomienia mogą być używane biblioteki vllm, transformers i SGLang.
Między innymi model może być używany do wib-rozwoju w otwartym agencie mistral-vibe, a także integrować się z narzędziem Aeneas do weryfikacji kodu w języku Rust. Jako dane wejściowe przyjmowane są teksty i obrazy, a na wyjściu zwracany jest tylko tekst. Obsługiwana jest analiza zawartości obrazów.
Aby ocenić możliwości modeli AI, biorąc pod uwagę jakość formalnej weryfikacji kodu i pisania dowodów matematycznych, opracowano nowy zestaw testów FLTEval. W przeprowadzonych testach model Leanstral znacznie przewyższył istniejące otwarte modele Qwen3.5 397B-A17B, Kimi-K2.5 1T-A32B i GLM5 744B-A40B, pokazując podobne wyniki z modelami Claude Haiku 4.5 i Claude Sonnet 4.6 firmy Anthropic, ale pozostawiając w tyle model Claude Opus 4.6. W szczególności model Opus zdobył 39,6 punktu, a Leanstral 21,9 przy jednym przebiegu i 31,9 przy 16 przebiegach. Koszty użycia Opus wyniosły 1650 dolarów, a Leanstral 18 dolarów przy jednym przebiegu i 290 dolarów przy 16 przebiegach. Model Haiku zdobył 23 punkty przy kosztach 184 dolarów, a model Sonnet 23,7 przy kosztach 549 dolarów.
Źródło: opennet.ru
