Kínai cég újgenerációs matematikai MI modellje segítheti a bizonyítások ellenőrzését
A kínai DeepSeek vállalat szerdán mutatta be matematikai bizonyításokra specializált mesterséges intelligencia modelljének legújabb verzióját. A DeepSeek-Prover-V2 névre keresztelt rendszer kifejezetten matematikai tételek formális bizonyítására készült, és jelentős előrelépést jelent a korábbi verziókhoz képest.
Az új modell különlegessége, hogy a Lean 4 programozási nyelvet használja a matematikai bizonyítások lépéseinek logikai ellenőrzésére. A rendszer képes minden egyes lépést függetlenül elemezni, így biztosítva a teljes bizonyítás helyességét. A hangcsoui székhelyű vállalat a korábbi gyakorlatához hűen ezt a modellt is nyílt forráskóddal tette elérhetővé, így bárki letöltheti a GitHub vagy a Hugging Face platformokról.
Hirdetés:
Kétféle méretben, többféle felhasználási lehetőséggel
A fejlesztők két különböző méretben bocsátották közre az új modellt. A kisebb változat 7 milliárd paraméterrel működik, míg a nagyobb verzió nem kevesebb mint 671 milliárd paramétert tartalmaz. Az első a DeepSeek-Prover-V1.5-Base-re épül, és akár 32 000 token hosszúságú kontextust is képes kezelni, a nagyobbik pedig a 2024 decemberében kiadott DeepSeek-V3-Base modellre támaszkodik.
Ami a felhasználási területeket illeti, a rendszer képes középiskolai és egyetemi szintű matematikai problémák megoldására, bizonyítások hibáinak felkutatására és javítására. Tanítási segédletként is használható, mivel lépésről lépésre képes elmagyarázni a bizonyítási folyamatokat. Nem utolsósorban a kutatók számára is hasznos eszköz lehet új tételek vizsgálatánál és érvényességük bizonyításánál.
Különleges tanítási módszer
A modell fejlesztése során a kutatók egy úgynevezett „cold-start” tanítási rendszert alkalmaztak. Ennek lényege, hogy az alapmodellt arra ösztönözték, hogy komplex problémákat bontson kisebb, kezelhetőbb részfeladatokra. Ezek a részfeladatok egyfajta célsorozatként szolgáltak a tanulási folyamatban. A már megoldott részfeladatok bizonyításait aztán hozzáadták a gondolkodási lánchoz (Chain of Thought, CoT), és az alapmodell érvelésével kombinálva létrehozták a megerősítéses tanulás kezdeti állapotát.
Véleményem szerint ez a specializált modell jól példázza, hogyan lehet a mesterséges intelligencia képességeit célzottan fejleszteni egy konkrét tudományterületen. A matematikai bizonyítások automatizálása régóta a mesterséges intelligencia kutatások egyik fontos célkitűzése, és a DeepSeek-Prover-V2 komoly lépést jelent ebbe az irányba. Különösen értékes, hogy nyílt forráskódú modellként széles körben hozzáférhető, így az oktatásban és a kutatásban is azonnal alkalmazható.
Ahogy a legtöbb nyílt forrású modell esetében, itt sem ismerjük pontosan az alaparchitektúra vagy az adatkészlet minden részletét. Ennek ellenére a modell kiadása jelentős lépés a matematikai MI-alkalmazások területén, és jól mutatja, hogy a specializált modellek fejlesztése milyen gyorsan halad előre a nagy nyelvi modellek árnyékában is.
A borító képet FLUX.1-dev képgenerátor készítette az alábbi prompt alapján: A Chinese AI researcher is working on mathematical theorem proofs with a glowing AI interface showing complex mathematical equations and proof structures, futuristic office setting.
