看不懂新開(kāi)源的DS-Prover V2版本?解讀來(lái)了,攻克像人類一樣數(shù)學(xué)證明,達(dá)到SoTA水平,不知道如何測(cè)?樣題來(lái)了
原創(chuàng)五一凌晨,DeepSeek終于更新了新開(kāi)源的 DeepSeek-Prover V2的自述文件。速覽一下:
- 解決近 90% 的 miniF2F 問(wèn)題(88.9%)
- 顯著提高 PutnamBench 上的 SoTA 性能
- 在正式版本中對(duì) AIME 24 和 25 問(wèn)題取得了驚艷的通過(guò)率
點(diǎn)評(píng):亮點(diǎn)上來(lái)看,DeepSeek-Prove V2模型在死磕LLM在推理數(shù)學(xué)問(wèn)題上能給出答案但卻給不出嚴(yán)格正確的推理步驟的問(wèn)題。而且在一中先進(jìn)模型中達(dá)到了SoTA的水平,圖四是前十榜單。
AIME這個(gè)測(cè)試集大家很清楚了,這里不再贅述。這里重點(diǎn)科普下miniF2F測(cè)試。
miniF2F 是什么?
miniF2F 是一個(gè)面向大型語(yǔ)言模型(LLM)數(shù)學(xué)推理能力評(píng)測(cè)的基準(zhǔn)數(shù)據(jù)集,全名是 mini Formal to Formal。它源自更早的 F2F(Formal-to-Formal) 項(xiàng)目,但體量更小,便于在不同模型上快速評(píng)測(cè)。
它是一組高中及大學(xué)初等數(shù)學(xué)題目,覆蓋以下領(lǐng)域:代數(shù)、數(shù)論、微積分、幾何、離散數(shù)學(xué)等等。這些題目用自然語(yǔ)言表述(類似“證明對(duì)于任意正整數(shù)n,有…”),目標(biāo)是評(píng)測(cè) LLM 能否像人類數(shù)學(xué)家一樣,通過(guò)推理過(guò)程得出正式的數(shù)學(xué)證明。
舉個(gè)簡(jiǎn)化版的例子,miniF2F的題目是這樣的——
證明:對(duì)于任意正整數(shù) n,2n + 1 是奇數(shù)。
LLM 要能輸出嚴(yán)謹(jǐn)證明,比如:
對(duì)于任意正整數(shù) n,有 2n 是偶數(shù),偶數(shù)加 1 是奇數(shù),因此 2n + 1 是奇數(shù)。
如果你做 LLM 評(píng)測(cè)、數(shù)學(xué)任務(wù)微調(diào)或者學(xué)術(shù)方向,這個(gè)數(shù)據(jù)集是很重要的 benchmark。
DS如何做到的?
DS開(kāi)發(fā)了一種簡(jiǎn)單而高效的遞歸定理證明流程,利用V3模型作為統(tǒng)一工具,既用于子目標(biāo)分解,也用于形式化處理,并引導(dǎo)V3 將定理分解為高層次的證明草圖,同時(shí)在 Lean 4 中形式化這些證明步驟,從而生成一系列子目標(biāo)。
使用較小的 7B 模型來(lái)處理每個(gè)子目標(biāo)的證明搜索,以降低相關(guān)的計(jì)算負(fù)擔(dān)。一旦復(fù)雜問(wèn)題的分解步驟被解決,將完整的逐步形式化證明與 DeepSeek-V3 的相應(yīng)思維鏈配對(duì),創(chuàng)建冷啟動(dòng)推理數(shù)據(jù)。
想要測(cè)評(píng)或者試用的朋友可以跑起來(lái)了,當(dāng)然建議跑7B模型了,671B不是一般設(shè)備能跑的。model_id = "DeepSeek-Prover-V2-7B"