Mistral AI 2. jūlijā izlaida Leanstral 1.5 — 119 miljardu parametru atvērtā koda modeli, kas raksta un pārbauda pierādījumus Lean 4 formālās verifikācijas valodā. Pirmajā praktiskajā testā modelis skenēja 57 atvērtā koda repozitorijus un atrada piecas iepriekš nezināmas kļūdas.
Lean 4 ir pierādījumu asistents formālai programmu pareizības pārbaudei. Atšķirībā no parastiem testiem, kas pārbauda konkrētus ievades piemērus, formālie pierādījumi dod matemātisku garantiju par koda darbību visiem iespējamiem ievades gadījumiem. Pierādījumu rakstīšana manuāli prasa laiku un specializētas zināšanas — Leanstral 1.5 ģenerē un aizpilda pierādījuma soļus automātiski. Tādā veidā izstrādātāji var iegūt formālu garantiju, nepavadot dienas Lean 4 sintakses iepazīšanā.
Arhitektūra un pieejamība
Leanstral 1.5 izmanto mixture-of-experts arhitektūru: 119 miljardi kopējo parametru, katrā marķierī aktīvi 6,5 miljardi. Konteksta logs — 256 000 marķieri, kas ļauj strādāt ar gariem pierādījumu failiem un plašiem koda kontekstiem. Svari lejupielādējami no Hugging Face platformas ar Apache 2.0 licenci bez komerciāliem ierobežojumiem. Mistral Labs API modelis darbojas kā labs-leanstral-1-5 un pieejams arī Mistral Vibe interaktīvajā vidē.
Mistral dokumentācijā norādīts, ka Labs API pieejamība beigsies 30. septembrī 2026 — tas ir eksperimentāls izvietojums. Svari paliek publiski pieejami bez noteikta termiņa. Tas nozīmē, ka komandas, kuras vēlas iekļaut modeli savos rīkos, var brīvi lejupielādēt svarus un palaist lokāli vai savā infrastruktūrā.
Soliņu rezultāti
Uz miniF2F soliņa, kas satur standartizētus formālās matemātikas pierādījumu uzdevumus augstskolas līmenī, Leanstral 1.5 sasniedz 100%. Uz PutnamBench, kurā iekļauti 672 uzdevumi no Putnam sacensībām universitātes matemātikā, modelis atrisina 587. Algebras soliņos FATE-H rezultāts — 87%, FATE-X — 34%.
The Decoder norāda, ka miniF2F 100% ir augstāks rādītājs nekā jebkuram iepriekšējam atvērtā koda modelim formālajā matemātikā. PutnamBench 587/672 nozīmē 87% uzdevumu, kurus parasti spēj risināt tikai ar matemātikas konkursu pieredzi un vairāku stundu darbu uz katru.
Piecas kļūdas 57 projektos
Mistral ļāva modelim skenēt 57 populārus atvērtā koda projektus, kas paši izmanto Lean 4 formālai specifikācijai. Rezultāts — piecas kļūdas, ko cilvēku recenzenti un parasti testi bija palaiduši garām. Kādi projekti un kādas konkrētas kļūdas — Mistral to nav publicējis.
Praksē tas nozīmē, ka modelis var skenēt esošos Lean 4 pierādījumus un atrast gadījumus, kur pierādījums nav pilnīgs vai kur koda darbība neatbilst formālajai specifikācijai. Šādi pārskati ir grūti veicami manuāli lielās kodu bāzēs, kur pierādījumi stiepjas tūkstošiem rindu.
Formālie pierādījumi dod matemātisku garantiju, ka kods atbilst specifikācijai. Testiem var pierādīt kļūdu esamību; pierādīt to neesamību testi nevar. Formālā verifikācija to var.
Lean 4 ekosistēma
Lean 4 ir mazāk izplatīts nekā Coq vai Isabelle, bet pēdējos gados audzis. Mathlib — Lean 4 galvenā matemātisko teorēmu bibliotēka — satur vairāk nekā 200 000 formalizētu teorēmu. MLQ AI ziņo, ka pēdējos divos gados Lean 4 formālo bibliotēku kopapjoms trīskāršojies. Lean 4 kā verifikācijas rīku pēdējos gados pieņēmis arī matemātikas formalizācijas projekts Mathlib, kuru izmanto universitātēs un pētniecības grupās.
Formālā verifikācija ir praktiski pieprasīta kriptografijas bibliotēku, kompilatoru un OS kodolu komponentu izstrādē — vietās, kur kļūdu izmaksas ir augstas un kur testiem ar piemēriem nav pietiekami. Leanstral 1.5 var darboties kā automātisks taktikas ģenerators, kas aizstāj manuālu Lean 4 by exact? un by decide izmantošanu, paātrinot pierādījumu rakstīšanu ievērojami.
Kā sākt
Modelis pieejams kā mistralai/Leanstral-1.5 Hugging Face platformā. Labs API piekļuvei nepieciešams Mistral konts ar aktivizētiem Labs eksperimentiem. Mistral Docs modeļa kartē pieejamas integrācijas rekomendācijas — tostarp kā konfigurēt Lean 4 language server, lai Leanstral 1.5 automātiski piedāvātu taktiku pabeigšanu. Modelis pieņem Lean 4 koda kontekstu un atgriež pierādījuma taktiku secības, ko var ielikt tieši .lean failos.
Komentāri
Šim rakstam vēl nav komentāru. Esi pirmais, kurš dalās ar savu viedokli.