Leanstral 1.5 bewijst dat AI verborgen codeerfouten feilloos opspoort

Autonome AI-agenten in de codeomgeving

Leanstral 1.5 is getraind via een driestappenproces bestaande uit mid-training, supervised fine-tuning en reinforcement learning (RL) via de zogeheten CISPO-methode. Het model is hierbij blootgesteld aan twee specifieke RL-omgevingen.

In de 'multiturn'-omgeving krijgt het model een wiskundige stelling die het moet bewijzen of weerleggen. De AI dient een bewijs in, ontvangt real-time feedback van de Lean-compiler en past zijn strategie aan tot het bewijs sluitend is.

Nog opvallender is de 'code agent'-omgeving. Hierin acteert de AI als een volwaardige software-engineer in een kaal bestandssysteem. Het model opent en bewerkt bestanden, voert bash-commando's uit en gebruikt de Lean-taalserver om foutmeldingen en datatypen te inspecteren. Hierdoor kan de AI complexe, langdurige taken uitvoeren, zoals het afmaken van incomplete bewijzen in bestaande software-repositories.

Nieuwe standaarden op academische benchmarks

De prestaties van het compacte model op wiskundige benchmarks zijn spectaculair. Leanstral 1.5 wist de miniF2F-benchmark (met wiskundeproblemen op het niveau van de Internationale Wiskunde Olympiade) volledig te satureren met een score van 100 procent op zowel de validatie- als de testset.

Op PutnamBench, een prestigieuze universitaire wiskundewedstrijd, loste het model 587 van de 672 extreem complexe vraagstukken op. Daarmee versloeg het concurrerende modellen zoals Seed-Prover 1.5. Wat deze prestatie extra indrukwekkend maakt, zijn de kosten: Leanstral 1.5 lost een probleem op voor ongeveer 4 dollar, terwijl de concurrentie daar honderden dollars aan rekenkracht voor nodig heeft. Ook op FATE-H (87%) en FATE-X (34%), twee benchmarks voor abstracte algebra op PhD-niveau, vestigde het model nieuwe records.

Het model vertoont bovendien een ongekende schaalbaarheid tijdens de testfase ('test-time scaling'). Waar traditionele AI-modellen vastlopen als een antwoord te lang op zich laat wachten, blijft Leanstral 1.5 doorredeneren. Zelfs bij een token-budget van 4 miljoen tokens per poging blijft de prestatiecurve lineair stijgen. De AI blijft urenlang code aanpassen en logische stappen verifiëren in plaats van op te geven.

Praktijktest: Verborgen softwarebugs blootgelegd

Hoewel Leanstral 1.5 primair is getraind voor theoretische wiskunde, blijkt het in de praktijk uit te blinken in het verifiëren van softwarecode. De ontwikkelaars demonstreerden dit aan de hand van twee praktijkcases.

Ten eerste slaagde het model erin om de exacte tijdscomplexiteit — de wiskundige garantie dat acties verlopen in een tijdsbestek van O(log n) — volledig formeel te bewijzen voor een zogeheten 'AVL-boom' (een zelf-balancerende datastructuur). Dit proces vereiste een diepe logische keten van 2,7 miljoen tokens en 22 context-comparties om alle mogelijke scenario's door te rekenen.

Daarnaast zette Mistral AI het model in voor een automatische bugjacht. Via een speciale pipeline werd bestaande Rust-code vertaald naar Lean, waarna Leanstral 1.5 moest bewijzen of de code deed wat de programmeur bedoelde. Het model testte 57 open-source software-repositories op GitHub en vlagde 47 schendingen van logische eigenschappen. In 11 gevallen bleek er sprake van een daadwerkelijke bug, waarvan er 5 nog nooit eerder door menselijke ontwikkelaars waren ontdekt.

Een van de gevonden fouten betrof een kritieke 'integer overflow' in de populaire databibliotheek datrs/varinteger. De fout zorgde voor crashes in debug-modus en onzichtbare datacorruptie in productiesystemen bij specifieke extreme input (Std.U64.MAX). Dit soort zeldzame randgevallen (edge cases) glipt bij traditionele softwaretests en 'fuzzing' vrijwel altijd door de mazen van de wet, maar werd door de AI feilloos gedetecteerd.

Met deze release toont Mistral AI aan dat formele verificatiemethoden, die tot nog toe als te duur en te complex werden beschouwd voor alledaags gebruik, dankzij agentic AI nu klaar zijn voor grootschalige adoptie in de software-industrie.