Mistral AI új modellje 100%-os a matek teszteken, hibákat is talál kódban

A Mistral AI bemutatta a Leanstral 1.5-öt, egy ingyenes, nyílt forráskódú (Apache 2.0 licenc) modellt, amelyet a Lean 4 programozási nyelvben történő formális verifikációra fejlesztettek ki. A Lean 4 célja matematikai bizonyítások és szoftverek helyességének formális igazolása. A modell 100%-os eredményt ért el a miniF2F teszten, amely középiskolától egészen a matek-olimpiai nehézségű problémákig terjed. A PutnamBench-en, amely a Putnam matematikai verseny 672 feladatát tartalmazza, 587-et oldott meg — közölte a Mistral AI Blog.

Az algebrai benchmarkokon, a FATE-H és FATE-X teszteken, amelyek csoportelméleti és gyűrűelméleti mester- és doktori szintű feladatokat vizsgálnak, a modell 87, illetve 34 százalékos eredményt ért el. A Leanstral 1.5 ezzel a nyílt forráskódú mezőnyben a PutnamBench, a FATE-H és a FATE-X teszteken is a legjobbnak bizonyult. Csak a zárt forráskódú Aleph Prover előzi meg a PutnamBench-en — írja a The Decoder.

Kapcsolódó: OCR-modell strukturált kimenettel

Bár a modellt elsősorban matematikai feladatokra képezték, a Mistral szerint a kódverifikációban is jól teljesít. Egy gyakorlati teszt során 57 nyílt forráskódú repozitóriumot vizsgált át, és öt korábban ismeretlen hibát talált, köztük egy túlcsordulási hibát a Rust `varinteger` könyvtárában. A modell a Hugging Face-en és egy ingyenes API-n keresztül érhető el.

Kapcsolódó: Mistral Large 3 nyílt forráskóddal

A képzés során mid-training, felügyelt finomhangolás és megerősítéses tanulás módszereit alkalmazták. A Leanstral 1.5 folyamat-ja automatikusan észlelte a hibákat, demonstrálva, hogy a formális verifikáció már valós kódbázisokra is alkalmazható, és olyan bugokat találhat, amelyeket más módszerek figyelmen kívül hagynak.

Kapcsolódó: Unsloth javította a Mistral Medium 3.5-et