前天晚上，DeepSeek發(fā)布了最新的數(shù)學專用大模型V2。 該模型有兩個版本，分別是671億參數(shù)和7億參數(shù)。在極具挑戰(zhàn)性的數(shù)學評測MiniF2F中，671B版本的通過率高達88.9%。此外，在PutnamBench包含的658道題目中，該模型成功解決了49道，展現(xiàn)出卓越的數(shù)學推理和解題能力。 同時，DeepSeek還公開了一個高質(zhì)量的數(shù)學評測數(shù)據(jù)集ProverBench，為數(shù)學能力測試提供了有力支持。
開源地址：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
評估數(shù)據(jù)集：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
在架構(gòu)方面，V2-671B是在DeepSeek-V3-Base模型的基礎上進一步訓練得到的，而V2-7B則基于DeepSeek-Prover-V1.5-Base構(gòu)建，同時擴展了上下文長度，最大支持32K標記。
V2搭建了一個統(tǒng)一的數(shù)學推理框架，將非形式化推理與形式化證明相結(jié)合。它通過將復雜數(shù)學問題拆解為多個子目標，利用V3的逐步推理能力，實現(xiàn)了從問題拆解到最終證明生成的無縫連接。
在冷啟動數(shù)據(jù)生成階段，V2采用遞歸的定理證明流程。首先，V3被用來將定理拆分成高層次的證明草圖，并在Lean4環(huán)境中對這些證明步驟進行形式化，形成多個子目標。隨后，較小的7B模型專注于每個子目標的證明搜索，這極大地減輕了整體計算壓力。當所有拆分步驟完成后，結(jié)合DeepSeek-V3的鏈式思考技術，系統(tǒng)生成了用于初始訓練的推理數(shù)據(jù)。
基于這些冷啟動數(shù)據(jù)，V2進入強化學習階段。在此階段，重點挑選出那些7B模型無法端到端解決的問題，但其所有子目標均已成功證明。通過整合這些子目標的證明，構(gòu)建出完整形式化的原始問題證明，并將其融合進V3的鏈式思考流程，實現(xiàn)了非形式推理與形式證明的連貫結(jié)合。
在強化學習階段，模型主要依靠二元的正誤反饋作為獎勵信號，進一步提升了將非形式推理與形式證明相結(jié)合的能力。為了更全面地評估模型表現(xiàn)，DeepSeek推出了ProverBench測試集。該數(shù)據(jù)集涵蓋了325道問題，其中15道題目取自近期AIME（第24屆和第25屆）競賽中的數(shù)論和代數(shù)題，體現(xiàn)了真實高中競賽的難度水平。
其余的310道題目來源于精心挑選的教科書案例和教學資料，內(nèi)容涵蓋高中至大學階段的多個數(shù)學領域，如數(shù)論、基礎代數(shù)、線性代數(shù)、抽象代數(shù)、微積分、實分析、復分析、泛函分析以及概率論等，為對模型能力的評估提供了廣泛且多樣化的測試內(nèi)容。
我們相信人工智能為普通人提供了一種“增強工具”，并致力于分享全方位的AI知識。在這里，您可以找到最新的AI科普文章、工具評測、提升效率的秘籍以及行業(yè)洞察。 歡迎關注“福大大架構(gòu)師每日一題”，讓AI助力您的未來發(fā)展。
熱門跟貼