Hvorfor er det vigtigt nu? Fordi formel verifikation længe har været noget, man betragtede på afstand: imponerende, men svært at operationalisere uden et dedikeret forskerhjørne. En åben proof‑agent med til at betale driftsomkostninger gør det pludselig plausibelt at automatisere beviser i rigtige kodebaser. Det er i hvert fald løftet. Om det holder, kræver nogle nøgterne testruns.
Hvad Leanstral 1.5 egentlig er
Leanstral 1.5 er målrettet Lean 4, en moderne bevisassistent, der checker hvert logisk skridt mekanisk. Fokus er ikke hyggesnak, men stringente bevistrin i et sprog, der kan udtrykke alt fra algebraiske strukturer til egenskaber ved små Rust‑kodefragmenter, ifølge udgiverens beskrivelse. Modellen taler altså bevis, ikke smalltalk.
Det er en kode‑agent, ikke bare en LLM med kodesmag. Agenten arbejder i filer, læser fejl fra Lean‑kompilatoren, skriver hjælpesætninger og prøver igen. Rundt og rundt. Forestil dig en junior, der faktisk elsker typefejl og ikke bliver træt. Den slags.
Arkitekturen under motorhjelmen
Mistral beskriver en MoE‑arkitektur med 128 eksperter, hvor 4 er aktive per token. Den samlede kapacitet opgives til 119 milliarder parametre, med 6,5 milliarder aktiveret per token. Pointen i MoE er kendt: høj kapacitet uden at tænde hele modellen ved hvert trin. Det hjælper på omkostningerne, når routing rammer rigtigt.
Kontekstvinduet er 256k tokens, input er multimodalt med tekst og billeder, output er tekst. 256k er stort i praksis: det åbner for lange bevisforløb og tunge projekter, hvor der komprimeres undervejs for at holde tingene i hukommelsen. Udgiver fremhæver netop kontekstkomprimering, så agenten kan bevæge sig igennem meget lange opgaver uden at glemme starten.
Træningen der former adfærden
Træningsregimet beskrives i tre trin: mid‑training, supervised finetuning og derefter reinforcement learning med CISPO. De to RL‑miljøer er vigtige for adfærden. I et multiturn‑miljø får modellen en sætning og skal bevise eller modbevise, læse fejl fra Lean og forfine sine forsøg, indtil budgettet er brugt.
Det andet miljø er mere jordnært: et kode‑agentmiljø i et råt filsystem. Modellen redigerer filer, kører bash‑kommandoer og bruger Lean language server, som leverer mål, fejl og typeinformation i realtid. Simpelt i idé, men det er netop den slidsomme interaktion, der kræves i rigtige repos. Korrekthed tjekkes, ifølge Mistral, via en fork af SafeVerify.
Benchmarks og påstande
På miniF2F rapporterer Mistral, at Leanstral 1.5 “saturerer” benchmarken med 100 procent på både validering og test. På PutnamBench hedder det 587 af 672 opgaver. Derudover nævnes nye topresultater på FATE‑H med 87 procent og FATE‑X med 34 procent. På FLTEval går pass@1 fra 21,9 til 28,9 og pass@8 til 43,2, og skulle efter udgiverens tal slå Opus 4.6’s 39,6 ved omtrent en syvendedel af omkostningen. Alle tal er rapporteret af udgiver og bør reproduceres uafhængigt, før man hænger banneret op i kantinen.
Hvad betyder 587 af 672 konkret? PutnamBench er et hårdt sæt matematisk bevisarbejde struktureret til Lean. At runde 587 med en agent betyder, at modellen ikke kun kan “skrive noget klogt”, men navigerer i Lean‑økosystemets strenge fejl og syntaks. Spørgsmålet er, hvor meget der skyldes test‑time budgetter og god routing. Mere om det om lidt.
Omkostninger, budgetter og test‑time scaling
Mistral estimerer cirka 4 dollars per PutnamBench‑problem for deres opsætning. I samme åndedrag sammenlignes der med Seed‑Prover i en høj indstilling til omkring 300 dollars per problem samt Aleph Prover i lejet 54‑68 dollars. Tilsvarende sammenligninger er udgiverens egne og bør krydstjekkes på projekternes sider og i uafhængige kørselsscenarier. Hardware, tokenbudgetter og timeouts flytter mere, end man tror.
Test‑time scaling er definerende her: hæver man tokenbudgettet ved inferens, stiger succesraten. Der rapporteres eksempelvis 44 løste problemer ved 50k tokens, 244 ved 200k, 493 ved 1M og 587 ved 4M. Det er både en feature og en praktisk hovedpine. For CI‑integration kan latency og pris eksplodere, hvis man altid skruer op, når noget driller. Vælg jeres battle‑modes med omtanke.
Åbenhed og licens
Vægtene frigives under Apache 2.0, og et gratis API‑endpoint med navnet leanstral‑1‑5 er meldt i drift. I praksis sænker det barrieren for evaluering og intern PoC. Det giver også en mere gennemsigtig compliance‑historik end proprietære, lukkede modeller. Men åbenhed kræver stadig due diligence: hvor hostes vægtene, hvilken checksum kan man stole på, leveres der modelkort og træningsmetadata, og hvad siger eksportreglerne i de regioner, der skal bruge værktøjet.
Virksomheder med stramme leverandørkæder bør tegne kortet: hvem driver API’et, hvor kører inference, og hvordan ser ansvar og SLA ud, hvis noget går ned midt i en releasefrys. Åbne weights er ikke det samme som gratis drift eller nul risiko.
Hvad det betyder i praksis
Formel verifikation lyder teoretisk, men anvendelsen er jordnær: sikre at en kernealgoritme holder en invariantegenskab, at en optimering ikke bryder et løfte om tidskompleksitet, eller at en compiler‑pass ikke introducerer en edge‑case. Leanstral er trænet til netop den slags bevisarbejde, hvor en sprogserver reagerer kontant på fejl og mål.
Nogle lavpraktiske skridt for teams, der vil prøve det af: vælg et ikke‑kritisk modul, sæt et konservativt tokenbudget, log alt, og behold menneskelig review. Mål ikke kun pass@N, men også tid, antal forsøg og hvor ofte agenten giver “pænt forkerte” svar, som først falder fra ved sidste verifikation. Man ser hurtigt, hvor integrationen klemmer.
Tre konkrete scenarier
Safety‑kritisk software: små, isolerede lemmas omkring kernelogik kan få automatiseret regressionsbeviser. Det er ikke hele flycomputeren på én gang, men en begyndelse, der kan reducere manuelt slid. Compliance‑checks: kontrakter for API’er eller politikker for ressourcetildeling kan beskrives i Lean og tjekkes automatisk, hvis sproget dækker domænet. Forskning og R&D: høj score på miniF2F og PutnamBench kan accelerere jagten på hjælpesætninger og proof‑skabeloner, men kør egne re‑runs for at undgå benchmark‑overfit.
Devops‑vinklen fortjener et ekstra ord. En agent, der kører bash og rører filer, skal i sandbox. Isolering, ressourcegrænser og logging er ikke tilvalg. Uden det ender man med en lovende PoC og et produktionsstop en tirsdag kl. 16.12. Set det før. Eller, næsten set.
Risici og begrænsninger
Overfit til benchmarks er en reel risiko. Når en udgiver melder 100 procent på miniF2F, er det flot, men også et rødt flag for datalækager, promptlæk eller utilsigtet overlap mellem træning og test. Der er ikke bevis for det her, bare et sundt forbehold. Kør jeres egne kopier af datasættene, eller brug afledte tests, som ikke findes i træningshistorikken.
Silent failures er den anden djævel. En model kan gå i stå fem trin fra målet og stadig aflevere tekst, der ligner en retning. SafeVerify‑forken skal efter udgiverens beskrivelse fange korrekthed mod målsætningerne, men i praksis bør man supplere med uafhængige verifikatorer, når det gælder produktion. To låse på døren er bedre end én.
Hvad man bør tjekke nu
Due diligence starter med kilder. Bekræft API‑endpointet, licensen og modelkortet fra udgiver. Tjek checksums for vægte og noter hosting‑placering. Kør PutnamBench og miniF2F lokalt med låste seed‑værdier. Mål variationen i pass@1 og pass@8, når tokenbudgetter ændres. Sammenlign resultater med og uden kontekstkomprimering.
Dernæst performance: profilér hukommelsesforbrug og latenstid ved 50k, 200k og 1M tokens. Log hvor mange filsystem‑operationer agenten bruger, og om sprogserveren bliver flaskehals. Slutteligt sikkerhed: sandbox‑politik, begrænsede privilegier, netværk off, samt fuld auditlog af bash‑kørsler. Kedeligt, ja. Nødvendigt, også ja.
Konkurrencebilledet lige nu
Markedet for specialiserede kode‑ og bevisagenter bevæger sig hurtigt. Samtidig ruller større udbydere generelle modeller ud og ind igen afhængigt af regulatoriske forhold. VentureBeats dækning af genaktiveringen af Anthropic‑modeller efter midlertidige eksportkontroller viser, hvor flydende adgangsforhold kan være for enterprise‑kunder. Det er ikke æbler mod æbler teknisk set, men det påvirker beslutningen om at lægge kritisk kapacitet hos et eksternt API.
I den åbne ende konkurrerer Leanstral dermed både mod andre specialiserede provers og mod generelle kode‑assistenter, som kan udstyres med tools og længere vinduer. Den afgørende forskel bliver, om agentadfærden i Lean‑miljøet faktisk giver mere stabile og billigere beviser i praksis. Ikke kun i benchmarks.
Hovedpointen og næste skridt
Hvis tallene holder, er Leanstral 1.5 et skridt mod praktisk, automatiseret formel verifikation i almindelige udviklingsforløb. Åbne weights og et gratis API sænker tærsklen for at teste, og MoE‑designet med stort kontekstvindue gør lange beviser realistiske. Bagsiden er test‑time scaling, der kan æde budget og tid, samt behovet for omhyggelig verifikation med uafhængige værktøjer.
Hvad kan man gøre i næste uge? Vælg et lille mål i koden, definér succeskriterier, sæt konservative budgetter og kør en kontrolleret PoC. Mål alt. Når tallene er på bordet, kan man beslutte, om proof‑agenterne skal ind i CI for alvor, eller om det bliver et internt forskningsspor lidt endnu. Ingen skam i det sidste.
Hurtig tjekliste til tekniske audits
- Kilder og licens: bekræft Apache 2.0, modelkort, checksums og hostingsted
- API‑stabilitet: load‑ og latens‑test af leanstral‑1‑5 ved varierende tokenbudgetter
- Reproduktion: kør miniF2F og PutnamBench selv, log pass@1 og pass@8 med faste seeds
- Test‑time scaling: mål omkostning og latenstid ved 50k, 200k, 1M og 4M tokens
- Sandbox: isolér filsystem og bash, slå netværk fra, og aktiver fuld auditlog
- Verifikation: suppler SafeVerify‑forken med en uafhængig verifikator inden produktion
- Data‑governance: dokumentér artefakter, prompts og versionsstyring af beviser
- Fallbacks: definer timeouts, budgetloft og menneskelig review‑sti i CI
