五一凌晨，DeepSeek終于更新了新開源的 DeepSeek-Prover V2的自述文件。速覽一下：

- 解決近 90% 的 miniF2F 問題（88.9%）

- 顯著提高 PutnamBench 上的 SoTA 性能

- 在正式版本中對 AIME 24 和 25 問題取得了驚艷的通過率

點評：亮點上來看，DeepSeek-Prove V2模型在死磕LLM在推理數(shù)學問題上能給出答案但卻給不出嚴格正確的推理步驟的問題。而且在一中先進模型中達到了SoTA的水平，圖四是前十榜單。

AIME這個測試集大家很清楚了，這里不再贅述。這里重點科普下miniF2F測試。

miniF2F 是什么？

miniF2F 是一個面向大型語言模型（LLM）數(shù)學推理能力評測的基準數(shù)據(jù)集，全名是 mini Formal to Formal。它源自更早的 F2F（Formal-to-Formal） 項目，但體量更小，便于在不同模型上快速評測。

它是一組高中及大學初等數(shù)學題目，覆蓋以下領域：代數(shù)、數(shù)論、微積分、幾何、離散數(shù)學等等。這些題目用自然語言表述（類似“證明對于任意正整數(shù)n，有…”），目標是評測 LLM 能否像人類數(shù)學家一樣，通過推理過程得出正式的數(shù)學證明。

舉個簡化版的例子，miniF2F的題目是這樣的——

證明：對于任意正整數(shù) n，2n + 1 是奇數(shù)。

LLM 要能輸出嚴謹證明，比如：

對于任意正整數(shù) n，有 2n 是偶數(shù)，偶數(shù)加 1 是奇數(shù)，因此 2n + 1 是奇數(shù)。

如果你做 LLM 評測、數(shù)學任務微調或者學術方向，這個數(shù)據(jù)集是很重要的 benchmark。

DS如何做到的？

DS開發(fā)了一種簡單而高效的遞歸定理證明流程，利用V3模型作為統(tǒng)一工具，既用于子目標分解，也用于形式化處理，并引導V3 將定理分解為高層次的證明草圖，同時在 Lean 4 中形式化這些證明步驟，從而生成一系列子目標。

使用較小的 7B 模型來處理每個子目標的證明搜索，以降低相關的計算負擔。一旦復雜問題的分解步驟被解決，將完整的逐步形式化證明與 DeepSeek-V3 的相應思維鏈配對，創(chuàng)建冷啟動推理數(shù)據(jù)。

想要測評或者試用的朋友可以跑起來了，當然建議跑7B模型了，671B不是一般設備能跑的。model_id = "DeepSeek-Prover-V2-7B"