Mistral AI julkaisi Leanstral 1.5:n, avoimen mallin, joka on rakennettu Lean 4 -todistuskielelle. Malli kirjoittaa ja täydentää matemaattisia todistuksia, jotka kone tarkistaa askel askeleelta. Julkaisu tapahtui 4. heinäkuuta, ja painot ovat ladattavissa Apache 2.0 -lisenssillä.
Leanstral 1.5 ei ole yleiskäyttöinen koodausassistentti. Se keskittyy kapeaan mutta kasvavaan alueeseen: formaaliin verifiointiin ja automaattiseen teoreematodistukseen. Testingcatalogin mukaan malli ratkaisi 587 ongelmaa 672:sta PutnamBench-vertailussa.
Mitä Leanstral 1.5 tekee
Lean 4 on sekä ohjelmointikieli että todistusavustaja. Se tarkistaa jokaisen loogisen askeleen mekaanisesti. Kielellä voi ilmaista niin abstrakteja matemaattisia rakenteita kuin ohjelmakoodin ominaisuuksia.
Leanstral 1.5 toimii koodiagenttina tässä ympäristössä. Se ei tuota vain valmiita vastauksia vaan rakentaa todistuksia monivaiheisesti. Malli osaa myös autoformalisoinnin eli epämuodollisen matematiikan muuntamisen koneellisesti tarkistettavaan muotoon.
Tämä erottaa sen tavallisista kielimalleista. Kun Lean 4 hyväksyy todistuksen, sen oikeellisuudesta ei jää epäilystä. Malli tuottaa todennettua matematiikkaa, ei todennäköisiä arvauksia.
Tekninen rakenne ja saatavuus
Leanstral 1.5 kuuluu Mistralin Small 4 -malliperheeseen. Se on Mixture of Experts (MoE) -malli, jossa on 119 miljardia parametria mutta vain noin 6,5 miljardia aktiivista kerrallaan. Konteksti-ikkuna on 256 000 tokenia.
Mallille on kolme käyttöpolkua. Painot löytyvät Hugging Facesta Apache 2.0 -lisenssillä, ja rajapinta toimii Mistralin Labs-palvelussa nimellä leanstral-1-5. Kolmas vaihtoehto on Mistral Vibe, yhtiön oma agenttikomentorivi.
Labs-listaus antaa mallille ilmaisen hinnan mutta myös aikarajan: se on merkitty poistuvaksi 30. syyskuuta 2026. Kyse on siis kokeellisesta käyttöönotosta. Itse isännöinti onnistuu vLLM:llä neljän näytönohjaimen kokoonpanossa.
Vertailutulokset ja löydetyt bugit
Mistralin raportoimat luvut ovat vahvoja. Malli saturoi miniF2F-vertailun eli saavuttaa sadan prosentin tuloksen sekä validointi- että testijoukossa. PutnamBenchissä se ratkaisi 587 ongelmaa 672:sta.
Muissa mittareissa malli ylsi 87 prosenttiin FATE-H:ssa ja 34 prosenttiin vaikeammassa FATE-X:ssä. FLTEval pass@8 -tulos nousi 31,9:stä 43,2:een. Malli jaksaa myös pitkiä todistusyrityksiä: yhdessä tapauksessa se käsitteli yli 2,7 miljoonaa tokenia 22 kontekstin tiivistyksen aikana.
Käytännön arvoa osoittaa toinen tulos. Leanstral 1.5 löysi viisi aiemmin raportoimatonta bugia avoimen lähdekoodin varastoista. Formaali verifiointi ei ole vain akateeminen harjoitus vaan paljastaa oikeita virheitä.
Miksi tämä on tärkeää kehittäjille
Leanstral 1.5 edustaa mallien erikoistumista. Yleismallien rinnalle syntyy työkaluja, jotka on hiottu yhteen tehtävään. Formaali verifiointi on juuri tällainen alue, sillä se vaatii tarkkuutta, jota yleismalli ei aina tavoita.
Apache 2.0 -lisenssi tekee mallista käyttökelpoisen yrityksille. Painot voi ladata, mallin voi ajaa omassa konesalissa ja sitä voi virittää ilman rajoittavia sopimuksia. Tämä on merkittävää tiimeille, jotka rakentavat verifioitua ohjelmistoa tai tarvitsevat paikallista ajoa tietoturvasyistä.
Malli tukee myös OpenAI-tyylisiä työkalukutsuja. Kehittäjä voi altistaa funktion, joka kääntää koodinpätkiä, ja Mistral suosittelee lean-lsp-mcp-palvelinta tiiviimpään Lean-integraatioon. Näin todistusmalli kytkeytyy osaksi laajempaa kehitystyönkulkua.
Yhteenveto
Leanstral 1.5 on kapea mutta kunnianhimoinen julkaisu. Se vie avoimen mallin formaalin matematiikan ja verifioinnin ytimeen sallivalla lisenssillä. Vahvat vertailutulokset ja viisi löydettyä bugia osoittavat, että kyse ei ole pelkästä demosta.
Aikaraja Labs-palvelussa muistuttaa julkaisun kokeellisuudesta. Ladattavat painot jäävät kuitenkin käyttöön, ja ne nostavat todennetun päättelyn rimaa Lean 4:ssä.