正當(dāng)大家紛紛進(jìn)入“五一”假期模式時，AI 界的 “勞?！?DeepSeek 再次證明：放假？不存在的。他們就在這個節(jié)骨眼上，悄然向開源社區(qū)投喂了一款重量級新模型——DeepSeek-Prover-V2-671B。
模型現(xiàn)已登陸 Hugging Face (鏈接: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B)，光看這 6710 億（671B）的參數(shù)量，就足以讓不少機(jī)器瑟瑟發(fā)抖。
這并非一款通用大模型，而是 DeepSeek 專為高難度數(shù)學(xué)領(lǐng)域，特別是使用 Lean 4 進(jìn)行形式化定理證明而打造的“專業(yè)選手”。
作為 DeepSeek-Prover 系列的第二代產(chǎn)品，大家自然對其能力充滿期待。要知道，其前身 V1.5（雖然只有 7B 參數(shù)）在去年的高中數(shù)學(xué)測試 (miniF2F) 中已能達(dá)到 63.5% 的成功率，在大學(xué)級別測試 (ProofNet) 中也有 25.3% 的準(zhǔn)確率。如今參數(shù)量暴漲近百倍的 V2，潛力顯然不可同日而語，但具體實(shí)力如何，還有待驗(yàn)證。
然而，DeepSeek 這次的操作頗有“先把孩子生下來，名字和體檢報告稍后補(bǔ)上”的風(fēng)格。模型權(quán)重已經(jīng)大方開源，但至關(guān)重要的 Model Card (模型詳細(xì)說明書) 和 Benchmark (官方性能成績單) 卻暫時缺席。
這不禁讓人猜測，是團(tuán)隊為了趕在假期前“交卷”過于匆忙，還是有意讓社區(qū)進(jìn)行一輪“盲測”和探索？
總之，勞動節(jié)是得繼續(xù)勞動了。
熱門跟貼