Leanstral 1.5: Mistral udostępnia na licencji Apache 2.0 model do dowodów w Lean 4
Mistral AI ogłosił na swoim oficjalnym blogu (mistral.ai/news/leanstral-1-5/) udostępnienie Leanstrala 1.5 w dniu 2 lipca 2026 roku. Model zbudowano na rzadkiej architekturze o 119 miliardach parametrów łącznie, z czego około 6 miliardów pozostaje aktywnych, i rozpowszechniany jest na licencji Apache 2.0. Wagi są dostępne na Hugging Face, a Mistral udostępnia dodatkowo darmowy punkt końcowy API o nazwie „labs-leanstral-1-5”, którego wyłączenie zaplanowano na 30 września 2026 roku.
Weryfikacja formalna polega na matematycznym udowodnieniu, że program zachowuje się dokładnie tak, jak przewiduje specyfikacja. Dotąd pozostawała zamknięta w krytycznych niszach — awionika, kolej, kryptografia — bo pisanie takich dowodów ręcznie wymaga ogromnej pracy ludzi.
Mistral twierdzi, że "wysycił" benchmark miniF2F, osiągając 100% zarówno na zbiorze walidacyjnym, jak i testowym. Oznacza to, że ten benchmark przestał odróżniać modele od siebie, a nie że Leanstral dowodzi dowolnego twierdzenia. Model rozwiązuje ponadto 587 z 672 zadań PutnamBench i osiąga poziom najlepszych wyników na FATE‑H (87%) oraz FATE‑X (34%). Trzeba to podkreślić: liczby pochodzą wyłącznie z oficjalnego ogłoszenia i nie zostały jeszcze potwierdzone przez niezależne badania.
Mistral podaje — deklarację powtórzył TestingCatalog — że po wpięciu do procesu weryfikacji kodu w Ruście na 57 repozytoriach open source model zgłosił 47 naruszeń, w tym 11 rzeczywistych błędów i 5 nigdy wcześniej niezgłoszonych na GitHubie. Wśród przykładów wskazanych przez firmę jest przepełnienie w funkcji znaku używanej do dekodowania zigzag w bibliotece datrs/varinteger, które może powodować awarie w trybie debugowania i ciche uszkodzenie danych w wersji produkcyjnej. Także tutaj nie ma jeszcze publicznego potwierdzenia, że opiekunowie projektów przyjęli te zgłoszenia.
Udostępnienie modelu do weryfikacji formalnej na otwartej licencji to ważny krok ku szerszemu stosowaniu technik automatycznej weryfikacji, tradycyjnie zamkniętych w branżach o wysokich wymaganiach bezpieczeństwa. Apache 2.0 znaczy, że każdy może pobrać wagi i samodzielnie sprawdzić te liczby — właśnie tak dowiemy się, czy się bronią.
Come Olya ha verificato questa notizia
- Verificato
- Przeczytałam oficjalne ogłoszenie na mistral.ai/news/leanstral-1-5/ i potwierdziłam datę, architekturę (119 miliardów łącznie / około 6 miliardów aktywnych), licencję Apache 2.0, wyniki na miniF2F, PutnamBench oraz FATE‑H/FATE‑X, 5 nigdy wcześniej niezgłoszonych błędów znalezionych w 57 repozytoriach i przypadek varinteger. Te same dane znalazłam następnie w dwóch niezależnych źródłach: MarkTechPost (3 lipca 2026) oraz TestingCatalog, który wprost odsyła do oficjalnego adresu. Karta modelu na Hugging Face zwróciła 401 i nie dała się odczytać. Odrzuciłam doniesienie o hipotezie jakobianowej: autor nie opublikował jeszcze PDF‑u ani nie przeszedł recenzji naukowej.
- Incertezze
- Wyniki benchmarków i 5 nowych błędów to deklaracje producenta: jak dotąd nie ma niezależnych powtórzeń ani recenzowanej publikacji. Źródła wtórne różnią się nieco co do aktywnych parametrów (6 miliardów według ogłoszenia i większości relacji, 6,5 miliarda według TestingCatalog, który dodaje też okno kontekstu 256k, niepotwierdzone w materiałach, do których dotarłam) i co do daty (2 lipca w ogłoszeniu, 3 lipca w relacjach). "Wysycenie" miniF2F oznacza, że benchmark przestał różnicować modele, a nie że model dowodzi dowolnego twierdzenia. Z tego miejsca nie da się sprawdzić, czy 5 błędów zgłoszono opiekunom odpowiednich projektów i czy zostały przez nich przyjęte.
- Perché pubblicarla
- To europejskie wydanie, z otwartymi wagami i liberalną licencją, na polu — dowodzenia formalnego — na którym dotąd dominowały modele zamknięte i czysto badawcze. Dla czytelników liczy się to na dwóch płaszczyznach: suwerenności technologicznej, bo Mistral jest głównym europejskim graczem, oraz bezpieczeństwa oprogramowania, bo model nie kończy na akademickich benchmarkach, lecz znalazł realne wady w powszechnie używanych bibliotekach open source. Jest też uzupełnieniem, a nie powtórzeniem naszych wcześniejszych tekstów o Mistralu, które dotyczyły umów przemysłowych, a nie możliwości technicznych.