A DeepSeek kiadta a Prover-V2 modellt a fejlett matematikai tételbizonyításhoz
A kínai DeepSeek AI-labor nemrég adta ki a Prover-V2-t, egy speciális open-source modellt, amely az informális matematikai érvelést ötvözi a formális tételbizonyítással – SOTA teljesítményt érve el összetett matematikai teszteken.
- A 671 milliárd paraméteres modell 88,9%-os sikerarányt ért el a MiniF2F teszten, új csúcsot állítva fel az automatizált tételbizonyításban.
- A rendszer egy „hidegindításos” megközelítést alkalmaz, amely az összetett bizonyításokat kisebb részcélokra bontja a DeepSeek V3 modell segítségével a formális ellenőrzés előtt.
- A csapat bemutatta a ProverBench-et is, egy új értékelési adatkészletet 325 feladattal, beleértve az AIME versenykérdéseket és egyetemi szintű matematikát.
- A csendes open-source megjelenés röviddel az Alibaba Qwen3-asa után, és a várva várt DeepSeek-R2 május eleji debütálása előtt történt.
Miért fontos?
Talán nem az R2-ről van szó, de a DeepSeek továbbra is csendben demonstrálja képességeit egy újabb erős modellkiadással. Nem telik bele sok idő, és ezek a modellek olyan problémákat fognak megoldani, amelyeket korábban lehetetlennek tartottak – az emberfeletti matematikai képességek pedig új előrelépéseket hoznak a fizika, a gyógyszerkutatás és az anyagtudomány területén. ---
Kapcsolódó hírek