久久精品人妻电影,亚洲精品va在线,亚洲一区二区三区四区在线乐播 ,欧美一区成人网,日本在线视频可以看

機器之心報道

編輯：大盤雞、澤南

DeepSeek R2 的前奏？

五一勞動節(jié)到了，DeepSeek 的新消息可沒停下來。

前些天到處都在流傳著 DeepSeek-R2 即將發(fā)布的傳言，DeepSeek 確實有新動作，不過大家沒等來 R2，等來的是 DeepSeek-Prover-V2，它當然也是開源的。

Prover-V2 在定理證明賽道上實現(xiàn)了業(yè)內(nèi)最佳性能，在 MiniF2F 測試中達到了 88.9% 的通過率，在 AIME 24、25 上也有不錯的分數(shù)。

在 4 月 30 日晚，機器學習協(xié)作平臺 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技術細節(jié)。

這次 DeepSeek 團隊發(fā)布了兩個版本的 DeepSeek-Prover-V2 模型，參數(shù)規(guī)模分別為 7B 和 671B。

其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基礎上訓練而成，而 DeepSeek-Prover-V2-7B 則基于 DeepSeek-Prover-V1.5-Base 構建，并支持最長 32K tokens 的上下文長度擴展。

DeepSeek-Prover-V2-7B 鏈接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
DeepSeek-Prover-V2-671B 鏈接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

要一句話總結 DeepSeek-Prover-V2 到底是什么？它是一款專為「數(shù)學 AI 編程語言」Lean 4 打造的開源大語言模型，專注于形式化定理證明。

它的初始化數(shù)據(jù)通過一個由 DeepSeek-V3 驅(qū)動的遞歸定理證明流程收集而來。在冷啟動訓練階段，首先通過提示 DeepSeek-V3 將復雜問題分解成一系列可以解決的子目標。每解決一個子目標就會將這些證明整合成「思維鏈」。并融合 DeepSeek-V3 的逐步推理軌跡，共同構建出用于強化學習的初始訓練數(shù)據(jù)。

這一策略的精妙之處在于：它能夠?qū)⒎切问交托问交臄?shù)學推理融合到一個統(tǒng)一的模型中，讓模型既能像人一樣靈活思考，也能像機器一樣嚴謹論證，真正實現(xiàn)了數(shù)學推理的一體化融合。

具體是如何實現(xiàn)的呢？DeepSeek 也發(fā)布了 DeepSeek-Prover-V2 的技術報告，讓我們看看其中是怎么說的：

技術概述

通過遞歸式證明搜索生成冷啟動推理數(shù)據(jù)

為了構建冷啟動數(shù)據(jù)集，DeepSeek 團隊設計了一條簡潔高效的遞歸定理證明流程，使用 DeepSeek-V3 作為統(tǒng)一工具，既負責子目標的拆解，也負責推理步驟的形式化表達。其中具體的過程則是通過提示引導 DeepSeek-V3 將定理拆解為高層次的證明草圖，并在此過程中同時將這些推理步驟用 Lean 4 語言形式化，最終生成一系列結構清晰、邏輯嚴密的子目標。

DeepSeek-Prover-V2 使用冷啟動數(shù)據(jù)收集過程概覽。

降低計算開銷一直是 DeepSeek 團隊的強項，這次也不例外。他們使用一個更小的 7B 模型來完成每個子目標的證明搜索，從而降低計算負擔。當復雜問題被拆解的各個步驟都成功解決后，他們將完整的形式化逐步證明與 DeepSeek-V3 生成的思維鏈相對應，組合成冷啟動推理數(shù)據(jù)。

何將分解的子目標轉(zhuǎn)化為一系列引理陳述的一個示例。

基于合成冷啟動數(shù)據(jù)的強化學習

DeepSeek 團隊挑選了一部分具有挑戰(zhàn)性的定理問題。7B 證明模型沒法雖然沒法兒將它們端到端的解決，但是能夠拿捏拆解出來的一系列子目標。

整合所有子目標的證明就可以構建出原始問題的完整形式化證明。隨后，將該正式證明附加到 DeepSeek-V3 所生成的思維鏈，這條思維鏈展示了對應的引理拆解過程，從而形成了一份將非形式化推理與后續(xù)形式化過程緊密融合的訓練數(shù)據(jù)。

在對證明模型進行合成冷啟動數(shù)據(jù)的微調(diào)后，研究團隊進一步引入強化學習階段，進一步提升模型將非形式化推理轉(zhuǎn)化為形式化證明的能力。在訓練過程中，遵循推理模型的通用目標，采用「對 / 錯」二值反饋作為主要的獎勵信號。

最終得到的模型 DeepSeek-Prover-V2-671B 在神經(jīng)定理證明任務中達到了當前最先進的性能，在 MiniF2F-test 上的通過率達到 88.9%，并成功解決了 PutnamBench 數(shù)據(jù)集中 658 道題中的 49 道。DeepSeek-Prover-V2 在 miniF2F 數(shù)據(jù)集上生成的所有證明已整理為 ZIP 文件，開放下載。

下載鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

訓練細節(jié)、實驗結果

DeepSeek-Prover-V2 經(jīng)歷了兩階段訓練，這一過程建立了兩種互補的證明生成模式：

1. 高效非思維鏈（non-CoT）模式：此模式針對快速生成正式的 Lean 證明代碼進行優(yōu)化，專注于生成簡潔的證明，沒有顯式的中間推理步驟。

2. 高精度思維鏈（CoT）模式：此模式系統(tǒng)地闡述中間推理步驟，強調(diào)透明度和邏輯進展，然后構建最終的正式證明。

與 DeepSeek-Prover-V1.5 一致，這兩種生成模式由兩個不同的引導提示控制。在第一階段采用專家迭代，在課程學習框架內(nèi)訓練一個非 CoT 證明模型，同時通過基于子目標的遞歸證明合成難題的證明。選擇非 CoT 生成模式是為了加速迭代訓練和數(shù)據(jù)收集過程。

在此基礎上，第二階段利用了冷啟動鏈式思維（CoT）數(shù)據(jù)，通過將 DeepSeek-V3 復雜的數(shù)學推理模式與合成形式證明相結合而生成。CoT 模式通過進一步的強化學習階段得到增強，遵循了通常用于推理模型的標準訓練流程。

DeepSeek-Prover-V2 的非 CoT 模式訓練過程遵循專家迭代的范式，這是開發(fā)形式化定理證明器廣泛采用的框架。在每次訓練迭代中，當前最佳證明策略用于生成那些在先前迭代中未解決的難題的證明嘗試。這些成功的嘗試經(jīng)由 Lean 證明助手驗證后，被納入 SFT 數(shù)據(jù)集以訓練改進的模型。這一迭代循環(huán)不僅確保模型能夠從初始演示數(shù)據(jù)集中學習，還能提煉出自己的成功推理軌跡，逐步提高其解決更難問題的能力?？傮w訓練過程與 DeepSeek-Prover-V1 的訓練過程大致一致，僅對訓練問題的分布進行了兩項修改。

首先，Prover-V2 引入了來自自動形式化和各種開源數(shù)據(jù)集的額外問題，擴大了訓練問題領域的覆蓋范圍。其次，新模型通過子目標分解生成的問題來擴充數(shù)據(jù)集，旨在解決 MiniF2F 基準測試有效劃分中的更多挑戰(zhàn)性實例。

研究人員在 DeepSeek-V3-Base-671B 上使用恒定的學習率 5e-6，在 16384 個 token 的上下文中進行監(jiān)督微調(diào)。訓練語料庫由兩個互補來源組成：1）通過專家迭代收集的非 CoT 數(shù)據(jù)，生成無需中間推理步驟的 Lean 代碼；2）第 2.2 節(jié)中描述的冷啟動 CoT 數(shù)據(jù)，將 DeepSeek-V3 的高級數(shù)學推理過程提煉為結構化的證明路徑。非 CoT 組件強調(diào)精益定理證明器生態(tài)系統(tǒng)中的形式驗證技能，而 CoT 示例明確地建模了將數(shù)學直覺轉(zhuǎn)化為形式證明結構的認知過程。

Prover-V2 采用 GRPO 強化學習算法，與 PPO 不同，GRPO 通過為每個定理提示采樣一組候選證明并根據(jù)它們的相對獎勵優(yōu)化策略，消除了對單獨批評模型的需求。訓練使用二元獎勵，每個生成的 Lean 證明如果被驗證為正確則獲得 1 個獎勵，否則為 0。為了確保有效學習，研究人員精心挑選訓練提示，僅包括那些對監(jiān)督微調(diào)模型具有足夠挑戰(zhàn)性但可解決的問題。模型在每次迭代中采樣 256 個不同的問題，為每個定理生成 32 個候選證明，最大序列長度為 32768 個 token。

最后是模型的蒸餾。研究人員把 DeepSeek-Prover-V1.5-Base-7B 的最大上下文長度從 4096 個 token 擴展到了 32768 個，并使用 DeepSeek-Prover-V2-671B 強化學習階段收集的 rollout 數(shù)據(jù)對這個擴展上下文模型進行微調(diào)。除了 CoT 推理模式外，研究人員還整合了專家迭代過程中收集的非 CoT 證明數(shù)據(jù)，以實現(xiàn)一種成本效益高的證明選項，該選項能夠生成簡潔的形式化輸出，并且模型規(guī)模較小。此外，7B 模型也采用了與 671B 模型訓練相同的強化學習階段以提升性能。

研究人員對 DeepSeek-Prover-V2 在形式定理證明的各種基準數(shù)據(jù)集上進行了系統(tǒng)評估，涵蓋了高中競賽題目和本科水平的數(shù)學問題。實驗表明，671B 版的模型實現(xiàn)了前所未有的準確率，且與業(yè)內(nèi)其他先進模型相比效率也更高。

在 miniF2F 測試數(shù)據(jù)集上與最先進模型的比較。

DeepSeek-Prover-V2-671B 在 miniF2F 基準上解決的問題。

ProofNet - 測試和 PutnamBench 的實驗結果。

ProverBench：AIME 與教材題目的形式化基準數(shù)據(jù)集

這次，DeepSeek 還發(fā)布了 ProverBench，這是一個包含 325 道題目的基準數(shù)據(jù)集。其中，15 道題來自最近兩屆 AIME 數(shù)學競賽（AIME 24 和 25）中的數(shù)論與代數(shù)題目，經(jīng)過形式化處理，具備真實的高中競賽難度。其余 310 道題則精選自教材示例和教學教程，覆蓋內(nèi)容多樣，具有良好的教學基礎。

ProverBench 鏈接：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

該數(shù)據(jù)集旨在支持對模型在高中競賽題和本科數(shù)學題兩個層面的綜合評估。