Mistral szczegółowo zaprezentował 2 lipca 2026 roku Leanstral 1.5, wyspecjalizowany model AI przeznaczony do pracy z Lean 4, formalnego dowodzenia twierdzeń oraz weryfikacji właściwości oprogramowania. To zupełnie inny kierunek niż typowe modele pomagające programiście napisać kolejną funkcję czy znaleźć prosty błąd w kodzie.
Leanstral ma pomagać tworzyć formalne dowody, czyli matematycznie wykazywać, że określone twierdzenie albo właściwość programu jest poprawna. Model został udostępniony na licencji Apache 2.0, a jego wagi można pobrać i uruchamiać poza infrastrukturą Mistrala.
Model ma 119 miliardów parametrów, przy czym dzięki architekturze Mixture-of-Experts podczas przetwarzania wykorzystywane jest około 6,5 miliarda aktywnych parametrów. Obsługuje kontekst do 256 tys. tokenów oraz wejście tekstowe i graficzne. Dokumentacja Mistrala wskazuje 30 czerwca 2026 jako datę public preview modelu, natomiast szczegółowa publikacja prezentująca Leanstral 1.5 ukazała się 2 lipca.
Leanstral 1.5 – o co dokładnie chodzi?
Lean 4 jest językiem programowania i jednocześnie interaktywnym systemem do formalnego dowodzenia twierdzeń. Pozwala zapisać twierdzenie lub właściwość programu w ścisłej formie, a następnie komputerowo sprawdzić poprawność dowodu.
To zasadniczo różni się od zwykłej odpowiedzi modelu językowego. LLM może wygenerować kod wyglądający poprawnie, ale sam fakt wygenerowania odpowiedzi nie dowodzi, że program zachowa się prawidłowo w każdej sytuacji.
Formalna weryfikacja pozwala sprawdzić określone właściwości metodami matematycznymi. Leanstral 1.5 został wytrenowany właśnie pod kątem takich zadań oraz pracy agentowej w rzeczywistych repozytoriach.
Według wyników opublikowanych przez Mistral model rozwiązał 587 z 672 zadań PutnamBench, osiągnął 87% na FATE-H oraz 34% na FATE-X. Producent opisuje także eksperyment obejmujący 57 repozytoriów open source, podczas którego system miał wskazać pięć wcześniej nieznanych błędów. Wyniki są deklaracjami Mistrala i należy traktować je w kontekście użytych benchmarków oraz metod testowania.
Nie tylko matematyka – gdzie taki model ma zastosowanie?
Leanstral jest modelem specjalistycznym. Nie ma zastępować zwykłego asystenta do pisania wiadomości, generowania artykułów czy codziennego programowania. Jego zastosowanie zaczyna się tam, gdzie potrzebne są formalne dowody i możliwość mechanicznego sprawdzenia poprawności.
| Obszar | Potencjalne zastosowanie |
|---|---|
| Matematyka | Budowanie i sprawdzanie formalnych dowodów twierdzeń. |
| Lean 4 | Generowanie, poprawianie i rozwijanie kodu dowodów. |
| Weryfikacja oprogramowania | Sprawdzanie formalnie zapisanych właściwości kodu. |
| Systemy krytyczne | Pomoc przy analizie oprogramowania, w którym błędy są szczególnie kosztowne. |
| Badania naukowe | Automatyzacja części pracy związanej z formalizacją i sprawdzaniem dowodów. |
Szczególnie interesujące jest zastosowanie poza czystą matematyką. Właściwość programu również można zapisać formalnie, a następnie próbować udowodnić, że kod jej nie narusza.
Nie oznacza to, że Leanstral automatycznie „sprawdza cały program i gwarantuje brak błędów”. Formalna weryfikacja dotyczy konkretnie zdefiniowanych własności i wymaga odpowiedniej formalizacji problemu.
AI przechodzi od generowania kodu do sprawdzania jego poprawności
Leanstral 1.5 pokazuje istotny kierunek rozwoju modeli przeznaczonych dla programistów. Pierwsza fala narzędzi AI koncentrowała się głównie na generowaniu kodu. Kolejnym etapem jest wykorzystanie modeli do analizy, testowania i formalnego sprawdzania jego właściwości.
W tym przypadku interesujące jest połączenie modelu językowego z systemem, który potrafi jednoznacznie powiedzieć, czy formalny dowód został zaakceptowany. Odpowiedź nie jest oceniana wyłącznie na podstawie tego, czy brzmi przekonująco – musi przejść przez weryfikator Lean.
Jeśli podobne techniki będą coraz skuteczniejsze w rzeczywistych projektach programistycznych, AI może pełnić nie tylko rolę narzędzia przyspieszającego pisanie kodu, ale również jednego z elementów procesu sprawdzania jego poprawności.
Źródła
