Mistral AI uderza w kod i matematykę. Leanstral 1.5 znajduje krytyczne luki w bibliotekach Rusta

Mistral AI właśnie wypuścił następcę swojego marcowego modelu, rzucając wyzwanie światu akademickiemu i inżynierom oprogramowania równocześnie. Udostępniony 30 czerwca 2026 roku Leanstral 1.5 nie jest typowym chatbotem, który układa wiersze. To wyspecjalizowana jednostka oparta na architekturze Mixed Expert (MoE), posiadająca 119 miliardów parametrów, która weryfikuje dowody matematyczne i logikę systemów informatycznych z precyzją, o jakiej zamknięte modele mogą na razie pomarzyć.

Dlaczego to ważne teraz

Premiera Leanstral 1.5 to moment, w którym weryfikacja formalna wychodzi z sal wykładowych wprost do narzędzi deweloperskich. Po raz pierwszy model open-source osiągnął 100-procentową skuteczność w matematycznym benchmarku miniF2F. Oznacza to, że AI potrafi już bezbłędnie poradzić sobie z zadaniami na poziomie olimpijskim, dając inżynierom narzędzie do automatycznego wykrywania błędów logicznych, których klasyczne testy jednostkowe po prostu nie zauważą.

Matematyczna supremacja open-source

Liczby mówią same za siebie. W prestiżowym teście PutnamBench Leanstral 1.5 poprawnie rozwiązał 587 z 672 problemów, deklasując model Claude Sonnet 4.6. Co więcej, w testach FLTEval, opartych na formalizacji Lematu Fermata, Leanstral osiągnął wynik 26,3 przy pass@2. Koszt tej operacji wyniósł zaledwie 36 dolarów, podczas gdy konkurencyjny Claude za gorszy wynik (23,7 punktu) wymagał opłaty rzędu 549 dolarów. Jak podkreśla Mistral AI Team, to „model zoptymalizowany pod automatyczne dowodzenie twierdzeń i automatyczną formalizację dla narzędzia Lean 4”, co czyni go unikalnym w obecnym krajobrazie AI.

Od teorii grup do błędów w Rust

Prawdziwa siła modelu objawia się jednak w praktyce programistycznej. Podczas analizy 57 otwartych projektów Leanstral 1.5 zidentyfikował pięć nieznanych wcześniej luk. Najpoważniejszą z nich okazał się krytyczny błąd przepełnienia (overflow) w bibliotece varinteger napisanej w języku Rust. Statystyka ta potwierdza słowa ekspertów Mistral AI, że formalna weryfikacja „przestaje być domeną czysto akademicką i staje się realnym wsparciem dla inżynierów dbających o najwyższą jakość oprogramowania”.

Dostępność i architektura

Choć model operuje na ogromnej bazie 119 miliardów parametrów, w czasie rzeczywistym aktywnych jest tylko 6,5 miliarda z nich, co pozwala na sprawniejszą obsługę kontekstu sięgającego 256 tysięcy tokenów. Leanstral 1.5 jest dostępny bezpłatnie na licencji Apache 2.0. Można go przetestować w oficjalnym playgroundzie oraz przez API obsługujące zaawansowane funkcje, takie jak Function Calling czy agenci konwersacyjni. Warto się jednak spieszyć z testami – zgodnie z dokumentacją, obecna iteracja modelu ma zostać wycofana we wrześniu, by ustąpić miejsca jeszcze nowszej wersji SFT z wydłużonym czasem rozumowania.