szemlebeta AI hírek. tömören.

2026. július 5., vasárnap · Modellek

A Mistral nyílt forráskódú Leanstral 1.5 modellje 100%-ot ért el a miniF2F formális matematikai benchmarkon

A Mistral AI kiadta a Leanstral 1.5-öt, egy Apache 2.0 licencű, nyílt forráskódú modellt, amelyet a Lean 4 programozási nyelvben végzett formális verifikációra terveztek. A Mistral állítása szerint a modell 100%-os eredményt ér el a miniF2F benchmarkon, amely középiskolai szinttől matematikai olimpiai nehézségig terjedő feladatokat tartalmaz, míg a Putnam-versenyek 672 feladatából 587-et old meg. A cég szerint a modell az algebrai FATE-H és FATE-X benchmarkokon is csúcseredményeket produkál, 87, illetve 34 százalékkal. Bár elsősorban matematikai feladatokra képezték ki, a Mistral közlése alapján kódverifikációra is alkalmas: 57 nyílt forráskódú kódtár átvizsgálása során öt korábban ismeretlen hibát talált, köztük egy túlcsordulási hibát a varinteger nevű Rust könyvtárban. A modell a Hugging Face platformon és ingyenes API-n keresztül érhető el.

Miért fontos?

A formális matematikai verifikáció területén nyílt forráskódú modellként kiemelkedő benchmark-eredményeket mutat, és valós kódbázisokban is hibákat talált.

Források

The Decoder Nemzetközi sajtó

Kapcsolódó témák

Napi összefoglalók AI kutatás #Mistral AI#formális verifikáció

Napi összefoglaló

Ez a hír a 2026. július 5., vasárnap napi AI összefoglaló része.

Kapcsolódó hírek

Ausztrál startup az AI-csoportgondolkodás ellen: a Springboards Flint modellje változatosabb válaszokat ígér

A legtöbb nagy nyelvi modell – köztük a ChatGPT, Claude és Gemini – meglepően kiszámítható válaszokat ad nyitott kérdésekre: ha véletlenszámot kérünk 1 és 10 között, szinte mindig a 7-et kapjuk. A MIT Technology Review beszámolója szerint az ausztrál Springboards startup erre a problémára fejlesztette ki Flint nevű nagy nyelvi modelljét, amelyet kifejezetten arra tanítottak, hogy nyitott végű kérdéseknél – például úticél-ajánlásoknál – szélesebb válaszskálát kínáljon a mainstream modellekénél. A jelenség azért fontos, mert bár a kiszámíthatóság kódolási vagy kutatási feladatoknál elfogadható, az ötletelés és kreatív tervezés területén az AI-csoportgondolkodás komoly korlátot jelent. A Flint pontos teljesítményéről és összehasonlító teszteredményeiről a forrás nem közöl részleteket.

Az LLM-ek csoportgondolkodásba ragadtak – egy ausztrál startup változatosabb válaszokat ígér

A nagy nyelvi modellek meglepően kiszámítható válaszokat adnak nyitott kérdésekre: ha véletlenszámot kérünk 1 és 10 között, szinte mindig 7-et mondanak, autómárkánál pedig Toyotát vagy Hondát – mutatja be a jelenséget a MIT Technology Review. Az ausztrál Springboards startup Flint nevű modellje kifejezetten arra lett betanítva, hogy változatosabb, kevésbé sztereotip válaszokat generáljon. A cég társalapítója, Pip Bingemann szerint a fősodorbeli modellek pontosan ugyanazokra az eredményekre konvergálnak, ami kutatásnál vagy kódolásnál elfogadható, de ötletgyártásnál és kreatív feladatoknál komoly korlát. A Flint a hagyományos modellekkel ellentétben a hallucinációkat sem ellenségnek tekinti, hanem a változatosság forrásának. A jelenség szélesebb tudományos figyelmet is kap: novemberben kutatók is vizsgálták az LLM-ek válaszainak szűk eloszlását.

A Google bemutatta a Nano Banana 2 Lite képgeneráló modellt: gyors és olcsó, de kompromisszumokkal

A Google DeepMind elérhetővé tette a Gemini 3.1 Flash Lite Image modellt, amelyet Nano Banana 2 Lite néven ismernek: a cég állítása szerint ez a leggyorsabb és legolcsóbb képgeneráló modelljük. Alapértelmezett módban körülbelül 4 másodperc alatt készít képet, míg a standard Nano Banana-nak ehhez mintegy 20 másodpercre van szüksége. Az API-ár átlagosan 0,034 dollár 1000 képenként, a kimeneti tokenár pedig a Nano Banana 2 felének felel meg. Az Ars Technica szerint az Arena.ai felhasználói értékelései közel azonosak a nem-Lite változatéval, ugyanakkor a Google maga is elismeri, hogy a modell gyengébben kezeli a szövegeket – különösen a kis betűméretűeket –, az infografikákon pontatlan adatok jelenhetnek meg, és a személyek megjelenítése kevésbé konzisztens. A modell tehát gyors prototípuskészítésre és ötletelésre alkalmas, de a részletgazdagság terén elmarad a nagyobb változatoktól.