Mistral prezanton Leanstral 1.5 me kod të hapur, i cili arrin rezultate të shkëlqyera në testet e matematikës formale dhe zbulon gabime reale në kod

Mistral AI publikoi Leanstral 1.5, një model falas me burim të hapur (licencë Apache 2.0) i ndërtuar për verifikim formal në gjuhën e programimit Lean 4. Lean 4 është projektuar për të verifikuar formalisht provat matematikore dhe saktësinë e softuerit.

Mistral thotë se modeli arrin 100 përqind në miniF2F, një test formal matematikor që mbulon probleme nga niveli i shkollës së mesme deri në vështirësinë e olimpiadës së matematikës. Në PutnamBench, i cili përfshin 672 probleme nga konkursi i matematikës Putnam, ai zgjidh 587. Në testet e algjebrës FATE-H dhe FATE-X, të cilat testojnë detyrat e nivelit master dhe doktoraturë në fusha si teoria e grupeve dhe teoria e unazave, ai shënon rezultate maksimale prej 87 dhe 34 përqind.

Modeli u trajnua kryesisht për matematikë, por Mistral thotë se performon mirë edhe në verifikimin e kodit. Në një test praktik, ai skanoi 57 depo me burim të hapur dhe kapi pesë gabime të panjohura më parë, duke përfshirë një gabim mbingarkese në varinteger të bibliotekës Rust. Modeli është i disponueshëm përmes Hugging Face dhe një API falas. Trajnimi përfshinte trajnim të mesëm, rregullim të imët të mbikëqyrur dhe mësim përforcues.