五一凌晨，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"