A DeepSeek csendben frissítette matematikai bizonyítási modelljét, a Prover-V2-t

A kínai DeepSeek AI startup észrevétlenül kiadta a Prover-V2-t, egy speciális, 671 milliárd paraméteres modellt, amelyet matematikai bizonyítások és tételek megoldására fejlesztettek.

A bejelentés mindössze egy nappal azután történt, hogy az Alibaba bemutatta Qwen3 AI modellcsaládját, miközben egyre nagyobb figyelem övezi a DeepSeek közelgő R2 érvelő modelljét.

A Prover-V2 fő jellemzői

A DeepSeek V3 keretrendszerére épülő Prover-V2 Mixture-of-Experts (MoE) architektúrát használ, amely a bonyolult matematikai feladatokat részfeladatokra bontja, és ezeket dedikált „szakértő” modulok oldják meg. A modell így csak a releváns egységeket aktiválja, biztosítva az optimális számítási hatékonyságot. A rendszer FP8 kvantálást alkalmaz, amely csökkenti a számítási igényt, miközben megőrzi a matematikai pontosságot, így a modell erőforrás-korlátozott hardvereken is könnyebben elérhető.

A nyílt forráskódú megjelenés a Hugging Face platformján széles körű elismerést kapott, mivel demokratizálja a fejlett matematikai eszközökhöz való hozzáférést. Korai felhasználók – köztük matematikai diákolimpikonok – kiemelték lenyűgöző képességeit a formális tételbizonyítás terén. A modell egyik kiemelkedő újítása az egyedi „cold-start” tanítási eljárás, amely lehetővé teszi, hogy Lean 4-ben – egy széles körben használt matematikai bizonyítássegéd rendszerben – generáljon formális bizonyításokat. Ez hidat képez az informális matematikai intuíció és a formális szigor között.

Iparági környezet és versenyhelyzet

A Prover-V2 megjelenésének időzítése stratégiai jelentőségű az MI-piacon, mivel közvetlenül az Alibaba Qwen3 modellcsaládja után érkezett, amely szintén hangsúlyt fektet az érvelési és matematikai problémamegoldó képességekre. Míg a Qwen3 legnagyobb nyilvános modellje 235 milliárd paraméterrel rendelkezik, a DeepSeek 671 milliárd paraméteres speciális architektúrája kiemelkedő teljesítményt nyújt optimalizált erőforrás-használat mellett. Ez a hatékonyság a DeepSeek MoE tervezési megközelítéséből fakad, amely lehetővé teszi a magas szintű eredmények elérését alacsonyabb működési költségek mellett.

A kínai MI-vállalatok egyre komolyabb kihívást jelentenek nyugati versenytársaik számára: a DeepSeek korábbi, R1 érvelő modellje már az OpenAI o1 teljesítményét is megközelítette, töredéknyi tanítási költséggel. A matematikai MI egyre fontosabb versenyterületté válik, különösen mióta a Xiaomi is belépett a mezőnybe MiMo-7B érvelő modellcsaládjával. Ez a fokozódó versengés rávilágít arra, milyen jelentőséggel bírnak a specializált MI-modellek, amelyek képesek kezelni az összetett matematikai érvelést és formális bizonyításokat, miközben nyílt forráskódú kiadásaikkal a fejlett technológiákhoz való hozzáférést is szélesítik a globális MI-közösség számára.

A DeepSeek MI-fejlesztései

Fokozódik az érdeklődés a DeepSeek közelgő R2 modellje iránt is, amelyről azt híresztelik, hogy fejlettebb érvelési és vizuális képességekkel, valamint körülbelül 1,2 billió paraméterrel rendelkezik majd. Mindezt úgy, hogy jelentősen költséghatékonyabb marad, mint nyugati versenytársai, például az OpenAI GPT-4o. Bár eredetileg 2025 márciusára tervezték a megjelenést, a vállalat hivatalosan még nem erősítette meg az indulás időpontját. A Prover-V2 csendes megjelenése azonban sok iparági szakértő szerint stratégiai előfutára az R2 zászlóshajónak, demonstrálva a DeepSeek technikai érettségét.

A vállalat specializált MI-fejlesztési megközelítése jól tükröződik a DeepSeekMath 7B modelljükben is, amely 51,7%-os eredményt ért el a versenyszintű MATH benchmarkon anélkül, hogy külső eszközöket vagy szavazási technikákat alkalmazott volna. Ez a fókuszált szakterületi kiválóság – szemben az általános célú funkcionalitással – egyedi stratégiát jelent az MI-piacon, lehetővé téve, hogy a DeepSeek kifejezetten hatékony modelleket hozzon létre speciális felhasználási esetekre, miközben fejleszti átfogó érvelési képességeit is.

Jövőbeli kilátások és az R2 modell

A Prover-V2 csendes megjelenése komoly hatással lehet a mesterséges intelligenciával támogatott matematikai kutatás jövőjére, és potenciálisan újradefiniálhatja, miként közelítenek a matematikusok a bonyolult bizonyításokhoz és tételekhez. Ez a specializált modell egyre erősödő trendet képvisel a szakterület-specifikus MI-megoldások felé, amelyek kiválóan teljesítenek szűk, de kritikus fontosságú területeken – ahelyett, hogy kizárólag általános intelligenciára törekednének.

A kutatók immár kihasználhatják a Prover-V2 kettős működési módját, amely egyszerre alkalmas gyors matematikai feltérképezésre és magas megbízhatóságú formális bizonyítások generálására, így áthidalva az informális intuíció és a formális szigor közötti szakadékot.

Közben a technológiai közösség izgatottan várja a DeepSeek R2 modelljét, amelynek megjelenését eredetileg 2025 márciusára várták. Iparági pletykák szerint az R2 felülmúlhatja az OpenAI, az Anthropic és más versenytársak vezető modelljeit is, miközben megőrzi a DeepSeek költséghatékonysági előnyét. Egy márciusi Reuters-jelentés alapján a vállalat „akár már ebben a hónapban” is elindíthatja az R2-t, bár hivatalos megerősítés eddig még nem történt. A modell érkezése várhatóan jelentős átalakulást hoz majd a globális MI-piacon fejlettebb érvelési, kódolási és többnyelvű képességeivel.

FORRÁS: TechCrunch

(Nethuszár)