Nyhet

Mistral AI lanserar Leanstral 1.5 – gratis öppen AI-modell som bevisar matematik och hittar buggar

Mistral AI har släppt Leanstral 1.5, en öppen modell under Apache-2.0-licens för formell verifiering i bevisspråket Lean 4. Enligt bolaget, som publicerade nyheten den 2 juli 2026, löser modellen 587 av 672 problem i PutnamBench och har hittat fem tidigare orapporterade buggar i öppen källkod. Modellen är gratis att använda via Hugging Face och ett API.

Det viktigaste i korthet

• Leanstral 1.5 från Mistral AI har 119 miljarder parametrar totalt, varav 6 miljarder aktiva, och släpps under Apache-2.0-licens.

• Enligt Mistral AI löser modellen 587 av 672 problem i PutnamBench och når 100 procent på miniF2F (validerings- och testmängd).

• Nytt toppresultat enligt bolaget på FATE-H (87) och FATE-X (34).

• Kostnaden på PutnamBench uppges vara cirka 4 dollar per problem, mot uppskattningsvis 300 dollar eller mer för Seed-Prover 1.5 i högsta läget.

• I ett test på 57 kodförråd flaggades 47 brutna egenskaper. 11 pekade på verkliga buggar, och 5 av dem var inte tidigare rapporterade på GitHub.

• Vikterna finns på Hugging Face och modellen nås via ett gratis API under namnet leanstral-1-5.

Vad har hänt

Mistral AI presenterade den 2 juli 2026 Leanstral 1.5. Det är en uppgradering av Leanstral, som enligt bolaget sedan lanseringen erbjudit ett öppet och praktiskt sätt att arbeta med bevis i Lean 4. Bolaget hävdar att uppgraderingen gör formell verifiering kraftfullare och mer tillgänglig.

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 får modellen ett teorem som den ska bevisa eller motbevisa. Den skickar in ett bevis, får återkoppling från Lean-kompilatorn och förbättrar sitt angreppssätt tills beviset kompilerar eller budgeten är slut. I den andra, en kodagentmiljö, arbetar modellen som en utvecklare i ett filsystem: den redigerar filer, kör bash-kommandon och använder Leans språkserver för att inspektera mål, fel och typinformation. Det ska göra det möjligt att klara långa uppgifter som att slutföra delvis färdiga bevis i ett kodförråd och bygga hjälplemman. Resultaten kontrolleras med Mistrals egen förgrening av SafeVerify.

På benchmarkerna jämför Mistral AI sig med Goedel-Architect utan vägledning på naturligt språk, Seed-Prover 1.5 i högsta läget och AxProverBase. På PutnamBench slår Leanstral enligt bolaget Seed-Prover 1.5 med 7 problem. Kostnaden är cirka 4 dollar per problem, medan Seed-Prover uppskattas kosta 300 dollar eller mer med en budget på 10 H20-dagar per problem. De som rankas högre arbetar enligt Mistral under andra villkor: vissa får vägledning på naturligt språk, andra är dyrare, som Aleph Prover med 54–68 dollar per problem. Källan anger FATE-resultaten både som procent och som antal lösta problem.

Mistral AI lyfter också fram att modellen skalar med mer beräkning. När tokenbudgeten per försök höjs från 25 000 till 4 miljoner stiger Pass@8 på PutnamBench jämnt: 44 lösta problem vid 50 000, 244 vid 200 000, 493 vid 1 miljon och 587 vid 4 miljoner.

Bolaget släpper även benchmarken FLTEval som öppen källkod. Den bygger på verkliga pull requests från förrådet för Fermats sista sats. Leanstral 1.5 höjer pass@1 från 21,9 till 28,9 och pass@8 från 31,9 till 43,2. Enligt Mistral slår det därmed Opus 4.6:s 39,6 till en sjundedel av kostnaden, och det ökar försprånget mot öppna modeller som är 3–10 gånger större.

Trots att modellen främst tränats för matematik visar bolaget två kodexempel. I det första bevisade modellen tidskomplexiteten för en verklig implementation av AVL-träd. Arbetet krävde över 2,7 miljoner tokens och 22 kontextkomprimeringar och slutade med bevis för att insättning och borttagning är O(log n). I det andra byggde Mistral en automatisk kedja där verktyget Aeneas översätter Rust till Lean, medan Leanstral härleder avsikten och formulerar korrekthetsegenskaper. Modellen försöker bevisa varje egenskap i fyra försök och därefter motbevisa den i fyra till. En av buggarna fanns i teckenfunktionen för zigzag-avkodning i biblioteket datrs/varinteger. Vid indata Std.U64.MAX svämmar uttrycket (value + 1) över, vilket enligt källan ger krascher i debugläge och tyst datakorruption i releaseläge.

Vad det betyder för dig i Sverige

Källan tar inte upp Sverige eller någon särskild marknad. Modellen är öppen under Apache-2.0, vikterna finns på Hugging Face och API:et är enligt Mistral gratis, så svenska utvecklare och forskare som arbetar med Lean 4 kan i princip prova den. Mistral rekommenderar verktyget Mistral Vibe, som installeras med uv, och nämner även ett valfritt tillägg, Lean LSP MCP. Källan beskriver inga särskilda villkor, begränsningar eller support för svenska användare.

Det här vet vi inte än

Resultaten är Mistral AI:s egna mätningar och har enligt källan inte bekräftats av någon oberoende part. Jämförelserna med andra system gäller under olika villkor, och Seed-Provers kostnad är en uppskattning. Det framgår inte hur länge API:et förblir gratis eller om det finns användningsgränser. Källan anger inte heller hur många av de 47 flaggade egenskaperna som var falska larm utöver de 11 som pekade på verkliga buggar, eller hur modellen presterar utanför de redovisade testerna. Tillgänglighet, priser eller support specifikt i Sverige är inte kända.