U svetu veštačke inteligencije, potrebna je dodatna inteligencija kako bi se osigurala tačnost i pouzdanost. Francuska kompanija Mistral predstavlja Leanstral, alat za verifikaciju koda koji koristi programski jezik Lean.
Mistral ističe da formalna verifikacija koda smanjuje potrebu za ljudskim pregledima, koji mogu biti dugotrajni. Kroz dokaze, testove i specifikacije, AI alati mogu bolje prilagoditi svoj rad stvarnosti i generisati kvalitetnije rezultate.
Leanstral je dostupan sa otvorenim težinama (Apache 2.0) kao deo Mistral Vibe i putem besplatnog API-ja. Uz njega dolaze i rezultati iz testiranja FLTEval, koji procenjuje kako AI modeli rešavaju inženjerske dokaze.
Prema Mistralu, Leanstral-120B-A6B pokazuje bolje rezultate od većih rivala kao što su GLM5-744B-A40B i Qwen3.5-397B-A17B na FLTEval testovima.
Još zanimljivije, Leanstral je povoljnija alternativa skupljim modelima poput Claude-a. Mistral tvrdi da Leanstral nudi konkurentne performanse po znatno nižoj ceni. Na primer, Leanstral postigne rezultat od 26.3 na testu, dok je Sonnet znatno skuplji za korišćenje.
Dok Claude Opus 4.6, premium model kompanije Anthropic, ima višu ocenu na FLTEval (39.6), njegova cena je više od 1.600 dolara, dok Leanstral košta oko 290 dolara.
Mistral je takođe pokazao sposobnost Leanstrala da se nosi sa testiranjem, tako što je agent uspešno rešio konkretan problem iz Lean 4 koda.
Osim Leanstrala, Mistral je objavio i Mistral Small 4, model koji obuhvata razne zadatke, uključujući kodiranje i vođenje razgovora, čineći prelazak između specijalizovanih modela nepotrebnim.
