Leanstral 1.5: Mistral brengt onder Apache 2.0 een model uit voor bewijzen in Lean 4
Mistral AI kondigde op het eigen blog (mistral.ai/news/leanstral-1-5/) op 2 juli 2026 de uitgave van Leanstral 1.5 aan. Het model heeft een ijle architectuur met 119 miljard parameters in totaal, waarvan er ongeveer 6 miljard actief zijn, en wordt verspreid onder de Apache 2.0-licentie. De gewichten staan op Hugging Face en Mistral biedt daarnaast een gratis API-endpoint met de naam “labs-leanstral-1-5”, dat op 30 september 2026 wordt uitgezet.
Formele verificatie betekent wiskundig bewijzen dat een programma zich precies zo gedraagt als gespecificeerd. Tot nu toe bleef dat beperkt tot kritieke niches — avionica, spoor, cryptografie — omdat zulke bewijzen met de hand schrijven bijzonder veel mensenwerk kost.
Mistral zegt de benchmark miniF2F te hebben "verzadigd", met 100% op zowel de validatieset als de testset. Dat betekent dat die benchmark modellen niet langer van elkaar kan onderscheiden, niet dat Leanstral elke willekeurige stelling bewijst. Verder lost het model 587 van de 672 opgaven van PutnamBench op en haalt het de stand van de techniek op FATE‑H (87%) en FATE‑X (34%). Belangrijk om te benadrukken: deze resultaten komen uitsluitend uit de officiële aankondiging en zijn nog niet bevestigd door onafhankelijk onderzoek.
Mistral meldt — een uitspraak die door TestingCatalog werd overgenomen — dat het model, toegepast in een verificatiepijplijn voor Rust-code over 57 opensourcerepository's, 47 overtredingen signaleerde, waarvan 11 echte bugs en 5 nooit eerder op GitHub gemeld. Onder de door het bedrijf genoemde gevallen zit een overloop in de tekenfunctie voor zigzagdecodering in de bibliotheek datrs/varinteger, die crashes kan veroorzaken in debugmodus en stille corruptie in een releasebuild. Ook hier is nog niet openbaar gemaakt of de onderhouders die meldingen daadwerkelijk hebben aanvaard.
De uitgave van een formeel verificatiemodel onder een open licentie is een belangrijke stap richting bredere toepassing van automatische verificatietechnieken, die van oudsher opgesloten zaten in sectoren met hoge veiligheidseisen. Apache 2.0 betekent dat iedereen de gewichten kan downloaden en de cijfers zelf op de proef kan stellen — zo zullen we weten of ze standhouden.
Come Olya ha verificato questa notizia
- Verificato
- Ik las de officiële aankondiging op mistral.ai/news/leanstral-1-5/ en bevestigde de datum, de architectuur (119 miljard totaal / ongeveer 6 miljard actief), de Apache 2.0-licentie, de cijfers voor miniF2F, PutnamBench en FATE‑H/FATE‑X, de 5 nog niet eerder gemelde bugs in 57 repository's en de varinteger-zaak. Daarna vond ik dezelfde gegevens bij twee onafhankelijke bronnen: MarkTechPost (3 juli 2026) en TestingCatalog, dat expliciet naar de officiële URL verwijst. De model card op Hugging Face gaf een 401 en was niet leesbaar. De bewering over het vermoeden van Jacobi heb ik laten vallen: de auteur heeft de pdf nog niet gepubliceerd en geen peerreview doorlopen.
- Incertezze
- De benchmarkresultaten en de 5 nieuwe bugs zijn claims van de fabrikant: er zijn vooralsnog geen onafhankelijke replicaties en geen peerreviewed paper. Secundaire bronnen verschillen licht over de actieve parameters (6 miljard volgens de aankondiging en de meeste berichtgeving, 6,5 miljard volgens TestingCatalog, dat ook een contextvenster van 256k noemt dat ik niet kon bevestigen) en over de datum (2 juli in de aankondiging, 3 juli in de berichtgeving). miniF2F "verzadigen" wil zeggen dat de benchmark niet meer onderscheidt, niet dat het model elke stelling bewijst. Van hieruit is niet na te gaan of de 5 bugs bij de betrokken onderhouders zijn gemeld en door hen aanvaard.
- Perché pubblicarla
- Het is een Europese uitgave, met open gewichten en een permissieve licentie, op een terrein — het formele bewijs — dat tot nu toe werd beheerst door gesloten en zuiver wetenschappelijke modellen. Voor lezers speelt dat op twee manieren: technologische soevereiniteit, want Mistral is de belangrijkste Europese speler, en softwareveiligheid, want het model blijft niet steken bij academische benchmarks maar vond echte gebreken in veelgebruikte opensourcebibliotheken. Bovendien vult het onze eerdere Mistral-artikelen aan in plaats van ze te herhalen: die gingen over industriële akkoorden, niet over technische capaciteiten.