Leanstral 1.5 van Mistral vindt bugs met wiskundig bewijs

Mistral heeft Leanstral 1.5 vrijgegeven, een open model dat wiskundige bewijzen schrijft in de taal Lean 4. Daarmee toont het aan dat een stuk software precies doet wat de specificatie belooft. Het model verscheen op 2 juli onder een Apache 2.0-licentie op Hugging Face, dus ontwikkelaars kunnen de gewichten downloaden en lokaal draaien. In tests vond het vijf onbekende bugs in bestaande open-source projecten.

Wat formele verificatie inhoudt

Formele verificatie gaat een stap verder dan testen. Een proof assistant als Lean 4 controleert stap voor stap of een redenering sluitend is, zonder ruimte voor gaten. Dat werk was jarenlang voorbehouden aan een kleine groep specialisten, omdat je zo’n bewijs met de hand opbouwt. Leanstral 1.5 neemt een deel daarvan over: het genereert de bewijsstappen die Lean vervolgens narekent. Volgens The Decoder controleerde het model zo complexe eigenschappen van code en legde het vijf eerder onbekende fouten bloot in 57 geteste repositories.

Onder de motorkap is Leanstral 1.5 een mixture-of-experts met 119 miljard parameters, waarvan er per token 6 miljard actief zijn. Die opzet houdt de rekenkosten beperkt terwijl het model groot blijft.

Scores op de wiskundebenchmarks

Op miniF2F, een verzameling opgaven van schoolniveau tot olympiadevraagstukken, haalt Leanstral 1.5 volgens MarkTechPost 100 procent op zowel de validatie- als de testset. Op PutnamBench, gebaseerd op de Amerikaanse Putnam-wiskundecompetitie, lost het 587 van de 672 problemen op. De zwaardere algebra-benchmarks FATE-H en FATE-X, met opgaven op master- en doctoraalniveau, blijven met 87 en 34 procent lastiger. Dat taalmodellen serieuze wiskunde aankunnen bleek eerder deze maand ook toen GPT-5.6 Sol Ultra een wiskundevermoeden zei te bewijzen.

Open gewichten verlagen de drempel

Mistral kiest opnieuw voor een open licentie, net als bij eerdere open-weight modellen van het Franse lab. Dat past in de trend waarin ook GLM-5.2 en Kimi K2.7-Code hun gewichten vrijgeven om met gesloten systemen te concurreren. Voor formele verificatie is die openheid extra praktisch: onderzoeksgroepen en bedrijven met veiligheidskritische code draaien het model op eigen infrastructuur, zonder gevoelige broncode naar een externe API te sturen. Wie geen zware hardware heeft, kan Leanstral 1.5 via een gratis API proberen. Mistral, dat onlangs nog 3,5 miljard euro ophaalde bij een waardering van 23 miljard, mikt met zulke gerichte modellen op nichetoepassingen naast de algemene chatmodellen.

Wat betekent dit

Met Leanstral 1.5 schuift formele verificatie op van academische niche naar iets wat een ontwikkelaar er los bij pakt. De vondst van vijf echte bugs laat zien dat het verder reikt dan het oplossen van wiskundeopgaven. Toch blijft de techniek werk vragen: code moet eerst een formele specificatie krijgen voordat een model kan bewijzen dat die klopt, en Lean 4 opzetten kost tijd. Voor sectoren waar een fout duur uitpakt, van betalingsverkeer tot medische software, is een bewijsbaar correcte codebasis een aantrekkelijk vooruitzicht.