Dette er en agent som er utviklet for å bistå med formell verifisering av programvare. Når Ai agenter genererer kode, kan manuell gjennomgang og verifisering av denne koden være en tidkrevende prosess, spesielt i applikasjoner som matematisk forskning og kritisk programvare. Leanstral er utviklet for å adressere dette ved å integrere formell verifisering i kode genereringsprosessen.
Hva er Leanstral?
Leanstral er den første åpne kildekode agenten spesifikt utviklet for Lean 4, et så kalt bevisassistent system. Leanstral er bygget for å være effektiv med 6 milliarder aktive parametere, og er trent for å operere i formelle arkiver.
Kort om Mistral AI og Lean 4:
- Mistral AI: Et fransk teknologiselskap som utvikler kunstig intelligens, inkludert store språkmodeller. Selskapet fokuserer på åpen kildekode og effektive modeller.
- Lean 4: Et verktøy som fungerer som et programmeringsspråk og en bevisassistent. Det tillater brukere å formulere matematiske påstander eller programregler, og Lean 4 sjekker automatisk logikkens korrekthet. Dette bidrar til å sikre at kode eller bevis er matematisk korrekte.
Nøkkelegenskaper ved Leanstral:
- Åpen og tilgjengelig: Leanstral er utgitt under en Apache 2.0 lisens. Den er tilgjengelig som en agent modus innenfor Mistral Vibe og via et gratis API endepunkt. Mistral AI vil også publisere en teknisk rapport som beskriver treningsmetoden og en evalueringssuite kalt FLTEval.
- Effektiv og kraftig: Modellen benytter en sparsom optimalisert arkitektur. Ved å utnytte parallell inferens med Lean som en verifikator, er Leanstral ytelsessterk og kostnadseffektiv sammenlignet med eksisterende lukkede kildekode alternativer.
- Oppgraderbar via MCP: Leanstral støtter vilkårlige MCP-er (Model Context Protocols) gjennom Vibe, og er spesifikt trent for å oppnå maksimal ytelse med den ofte brukte lean-lsp-mcp.
Ytelse og kostnadseffektivitet
I evalueringer som reflekterer bruken i bevisscenarier, ble Leanstral testet for å fullføre formelle bevis og definere nye matematiske konsepter. Leanstral demonstrerer en effektivitetsfordel over større modeller. For eksempel, mens modeller som GLM5-744B-A40B og Kimi-K2.5-1T-32B har begrensninger i skalering, overgår Leanstral dem begge med en enkelt gjennomkjøring.
Sammenlignet med Claude sine modeller, tilbyr Leanstral konkurransedyktig ytelse, for mye lavere pris. Leanstral oppnår en score på 26.3 med to gjennomkjøringer, noe som slår Sonnet med 2.6 poeng. Claude Opus 4.6 leder i kvalitet, men har en høyere kostnad.
| Modell | Kostnad ($) | Score |
|---|---|---|
| Haiku | 184 | 23.0 |
| Sonnet | 549 | 23.7 |
| Opus | 1,650 | 39.6 |
| Leanstral | 18 | 21.9 |
| Leanstral pass@2 | 36 | 26.3 |
| Leanstral pass@4 | 72 | 29.3 |
| Leanstral pass@8 | 145 | 31.0 |
| Leanstral pass@16 | 290 | 31.9 |
Konklusjon
Leanstral tilbyr en åpen kildekode løsning for formell verifisering av maskin generert kode, og gjør avansert kode verifisering mer tilgjengelig for utviklere. Bra alternativ til Claude Sonnet og Opus, til en brøkdel av prisen.
Du kan lese mer på Mistrals nettsider:
https://mistral.ai/news/leanstral