Nyhet
Mistral AI släpper Leanstral 1.5 – öppen AI-modell som bevisar matematik och hittar buggar i kod
Mistral AI har släppt Leanstral 1.5, en öppen modell för formell verifiering och bevisföring i Lean 4. Enligt bolaget, som publicerade nyheten den 2 juli 2026, har modellen 119 miljarder parametrar totalt och 6 miljarder aktiva, och den når toppresultat på flera matematiska testset. Modellen släpps under Apache-2.0-licens och finns som gratis API.
Det viktigaste i korthet
• Leanstral 1.5 är en modell med 119 miljarder parametrar totalt och 6 miljarder aktiva, under licensen Apache-2.0.
• Enligt Mistral AI löser modellen 587 av 672 problem i PutnamBench och når 100 procent på både validerings- och testdelen av miniF2F.
• På de abstrakta algebratesten FATE-H och FATE-X anger Mistral AI nya toppresultat: 87 respektive 34.
• Enligt bolaget kostar modellen cirka 4 dollar per problem i PutnamBench, mot uppskattningsvis 300 dollar eller mer för Seed-Prover 1.5 i högt läge.
• I ett test på 57 kodförråd flaggade modellen 47 brutna egenskaper. Av dem pekade 11 på riktiga buggar, och 5 var tidigare orapporterade på GitHub.
• Vikterna finns på Hugging Face och modellen kan användas gratis via API-ändpunkten leanstral-1-5.
Vad har hänt
Mistral AI beskriver Leanstral 1.5 som en kraftig uppgradering av den tidigare Leanstral-modellen, som sedan lanseringen erbjudit ett öppet och praktiskt angreppssätt för bevisföring i Lean 4. Formell verifiering innebär att man bevisar matematiskt att ett påstående eller en programegenskap stämmer, och att beviset kontrolleras av Lean-kompilatorn.
Modellen har tränats i tre steg: mid-training, övervakad finjustering och förstärkningsinlärning med metoden CISPO. Förstärkningsinlärningen skedde i två miljöer. I den första, en flerstegsmiljö, får modellen ett teorem och ska bevisa eller motbevisa det. Den skickar in ett bevis, får återkoppling från Lean-kompilatorn och förfinar sitt försök tills beviset går igenom eller budgeten är slut. I den andra, en kodagentmiljö, arbetar modellen som en utvecklare i ett rått filsystem. Den redigerar filer, kör bash-kommandon och använder Lean language server för att se mål, fel och typinformation. Därmed kan den slutföra delvisa bevis i ett förråd och bygga hjälpsatser. Slutresultatet kontrolleras med Mistrals egen fork av SafeVerify.
I jämförelserna ställer Mistral AI modellen mot Goedel-Architect utan vägledning på naturligt språk, Seed-Prover 1.5 i högt läge och AxProverBase. På PutnamBench slår Leanstral enligt bolaget Seed-Prover 1.5 med 7 problem, till en bråkdel av kostnaden. Seed-Prover körs med en budget på 10 H20-dagar per problem. De prover som placerar sig högre arbetar enligt Mistral AI under andra villkor: vissa får vägledning på naturligt språk, andra är dyrare, till exempel Aleph Prover på 54–68 dollar per problem.
Mistral AI lyfter också fram att prestandan stiger jämnt när tokenbudgeten per försök höjs från 25 000 till 4 miljoner. För Pass@8 på PutnamBench går det från 44 lösta problem vid 50 000 tokens till 244 vid 200 000, 493 vid 1 miljon och 587 vid 4 miljoner.
Bolaget öppnar samtidigt testsetet FLTEval, som bygger på verkliga pull requests från förrådet för Fermats sista sats. Enligt Mistral AI höjs pass@1 från 21,9 till 28,9 och pass@8 från 31,9 till 43,2. Det går förbi Opus 4.6 på 39,6, till en sjundedel av kostnaden. Bolaget uppger också att försprånget växer mot öppna modeller som är 3–10 gånger större.
Trots att modellen främst tränats på matematik visar den enligt Mistral AI god förmåga i kodverifiering. I ett fall bevisade den att insättning och borttagning i ett AVL-träd har tidskomplexiteten O(log n). Arbetet krävde över 2,7 miljoner tokens och 22 kontextkomprimeringar. I ett annat fall översattes Rust-kod till Lean med Aeneas, varpå modellen själv härledde avsedda egenskaper och försökte bevisa dem, först fyra gånger och därefter fyra gånger för negationen. En av buggarna fanns i teckenfunktionen för zigzag-avkodning i biblioteket datrs/varinteger. Vid indata Std.U64.MAX gav uttrycket (value + 1) överflöde, vilket enligt Mistral AI ger krasch i debugläge och tyst datakorruption i releaseläge.
För att komma igång rekommenderar Mistral AI verktyget Mistral Vibe och en API-nyckel. Där installeras modellen med kommandot /leanstall och agenten startas med vibe --agent lean. Lean LSP MCP rekommenderas som tillval.
Vad det betyder för dig i Sverige
Källan tar inte upp Sverige specifikt. Modellen släpps under en öppen licens, och vikterna kan laddas ned från Hugging Face. API-ändpunkten uppges vara gratis, vilket enligt Mistral AI gör den tillgänglig för forskare, utvecklare och andra som arbetar med Lean 4 eller vill verifiera kod. Det gäller även svenska användare, men källan nämner varken regionala villkor eller begränsningar.
Det här vet vi inte än
Källan anger inte hur länge API-ändpunkten förblir gratis eller om användningsgränser finns. Den uppger inte heller hur resultaten håller i oberoende tester. Siffrorna för FATE-H och FATE-X anges på två sätt: som 87 procent och 34 procent i en del av texten och som 87 respektive 34 lösta problem i en annan. Den exakta betydelsen är därför oklar. Kostnaden för Seed-Prover är en uppskattning från Mistral AI. Hur modellen fungerar i verkliga projekt utanför de 57 testade förråden framgår inte, och inte heller någon svensk tillgänglighet eller svenska priser utöver vad som ovan beskrivits.