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

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

- 顯著提高 PutnamBench 上的 SoTA 性能

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

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

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

miniF2F 是什么？

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

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

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

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

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

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

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

DS如何做到的？

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

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

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