跳到主要內容

開放程式碼數學 AI 模型 DeepSeek Prover V2 發布


總部位於中國杭州的人工智慧 (AI) 公司DeepSeek週三發布了其 Prover 模型的更新版本。它被稱為 DeepSeek-Prover-V2，是一個高度專業化的模型，專注於證明形式數學定理。大型語言模型（LLM）使用Lean 4程式語言，透過獨立分析每個步驟來檢查數學證明是否邏輯一致。與中國公司先前發布的版本類似，DeepSeek-Prover-V2 是一個開源模型，可以從 GitHub 和 Hugging Face 等流行的儲存庫下載。

DeepSeek 推出以數學為中心的全新 AI 模型
該人工智慧公司在其 GitHub列表頁面上詳細介紹了新模型。它本質上是一個以推理為中心的模型，具有可見的思路鏈（CoT），在數學領域中發揮作用。它是基於 2024 年 12 月發布的 DeepSeek-V3 AI 模型構建並提煉的。

DeepSeek-Prover-V2 可以以多種方式使用。它可以解決高中到大學程度的數學問題，並發現和修復數學定理證明中的錯誤。它還可以用作教學輔助工具，對證明進行逐步解釋，並幫助數學家和研究人員探索新的定理並證明其有效性。

它有兩種模型大小——70 億參數大小和更大的 6,710 億參數大小。後者是在 DeepSeek-V3-Base 上進行訓練的，而前者則建立在 DeepSeek-Prover-V1.5-Base 之上，上下文長度高達 32,000 個標記。

在預訓練過程中，研究人員透過促使基礎模型分解複雜問題實現了冷啟動訓練系統。這些問題構成了一系列子目標。然後，將已解決子目標的證明添加到 CoT 中，並與基礎模型的推理相結合，為強化學習創建初始冷啟動。

值得注意的是，除了 GitHub 之外，該 AI 型號還可以從 DeepSeek 的 Hugging Face 清單中下載。 Prover-V2 模型強調了 AI 模型訓練過程的迭代變化如何顯著提高其專業能力。與其他開源模型發布類似，有關核心架構或更大資料集的細節尚不清楚。

https://kopyai.com/zh-tw/latest/view/type.news/0/28

Picture Source
tldv.io

標籤：

留言

張貼留言

這個網誌中的熱門文章

標普 500 指數和那斯達克指數結束兩週連漲勢頭，人工智慧引發的動盪令科技股承壓

週五美國股市波動劇烈，半導體股在有關 OpenAI ( OPAI.PVT ) IPO 可能推遲的報道出現後回落，這加劇了本週令市場劇烈震蕩的不利因素。 科技股為主的那斯達克指數（^IXIC）下跌 0.2%，而標準普爾 500 指數（^GSPC）小幅下跌，這兩個指數本週分別下跌 超過 4% 和近 2%。 道瓊工業指數（^DJI）科技股佔比較低，跌破橫盤整理線，但周漲幅不到 1%。 蘋果公司（ AAPL）上調 MacBook 和 iPad 價格後，人們越來越擔心記憶體和儲存組件成本飆升可能會衝擊設備製造商。內存晶片製造商美光科技（ MU）亮眼的財報表明，這種成本壓力還將繼續。 同時，《紐約時報》報道稱，OpenAI 正在考慮將其巨額 IPO 推遲到 2027 年，這也抑制了人們對科技股的興趣。 由於市場預期聯準會今年將升息，人工智慧交易已承壓。聯準會首選的通膨指標—個人消費支出指數— —5月份的強勁表現，進一步鞏固了這一預期。 https://kopyai.com/zh-tw/markets/view/type.stock.us/0/165 Picture Source unsplash
張貼留言
閱讀完整內容

西班牙監管機構表示，歐盟數位貨幣監管截止日期不會延長，幣安仍未獲得許可

西班牙最高證券監管機構週五表示，該國不會延長數位貨幣公司根據新規註冊的最後期限——儘管幣安公司正努力完成註冊。 根據歐盟新實施的 MiCA 數位貨幣框架，企業必須在 7 月 1 日前在成員國註冊並繼續營運。如果未能在下週前完成註冊，則將強制停止營業。下週後，歐洲消費者將無法與未經授權的數位貨幣服務提供者進行交易。 全球最大的數位貨幣交易所幣安曾申請在希臘根據《貨幣與公司法》（MiCA）註冊。但先前有報告指出希臘不太可能批准註冊申請，幣安本周宣布撤回在希臘的申請。目前，幣安正尋求在另一個歐盟成員國註冊，但由於下週三截止日期臨近，幣安很可能被迫至少暫時停止在歐洲的業務運作。 根據路透社報道，西班牙國家證券市場委員會主席卡洛斯·聖巴西利奧週五表示，7 月 1 日的最後期限“不會有任何例外或延期”。 聖巴西利奧對幣安等大型數位貨幣平台表示擔憂，這些平台由於缺乏 MiCA 合規性，可能在幾天內關閉。 他說：“我們擔心的是……過渡期的結束將如何展開，以及人們將如何適應新的環境。” 該監管機構補充說，他和一些人正在與尚未獲得牌照的主要數位貨幣公司聯繫，以確保他們制定計劃將客戶資產轉移到其他提供者，並確保投資者的權利。 一旦數位貨幣公司在歐盟國家註冊，其牌照即可「通行」至其他司法管轄區。歐盟成員國在金融監管方面採取了多種不同的方法，從塞浦路斯和馬耳他等較為寬鬆的監管體系，到法國和德國等以監管嚴格著稱的體系，不一而足。 雖然每個歐盟國家處理申請的方式可能各不相同，但所有國家都將執行同一套更廣泛的數位貨幣相關規則。 https://kopyai.com/zh-tw/markets/view/type.stock.us/0/166 Picture Source unsplash
張貼留言
閱讀完整內容

DeepSeek-V3.1 發布，邁向 AI Agent

DeepSeek-V3.1 在 DeepSeek-V3.1-Base 的基礎上進行後訓練，後者基於原始 V3 基礎檢查點，通過兩階段長上下文擴展方法構建，遵循原始 DeepSeek-V3 報告中概述的方法。 DeepSeek 透過收集更多長文件並大幅擴展兩個訓練階段來擴展資料集。32K 擴展階段的標記數量增加了 10 倍，達到 6,300 億個標記，而 128K 擴展階段的標記數量增加了 3.3 倍，達到 2,090 億個標記。此外，DeepSeek-V3.1 使用 UE8M0 FP8 規模資料格式進行訓練，以確保與微尺度資料格式相容。 DeepSeek-V3.1 是一個同時支持思考模式和非思考模式的混合模型。相較於上一版本，本次升級帶來了多個方面的改進： 混合推理：思考與非思考－一個模型，兩種模式 更快的思考：DeepSeek-V3.1-Think 與 DeepSeek-R1-0528 相比，可以在更短的時間內找到答案 更強大的代理商技能：後製訓練可提高工具使用率和多步驟代理任務 DeepSeek-V3.1 模型提升了工具使用、程式碼生成和推理效率，在高難度基準測試中實現了與 DeepSeek-R1 相當的效能，同時響應速度更快。它支援結構化工具呼叫、代碼代理和搜尋代理，適用於研究、編碼和代理工作流程。 工具和代理程式升級 在 SWE / Terminal-Bench 上獲得更好的結果 針對複雜搜尋任務的更強大的多步驟推理 思考效率大幅提升 模型更新 V3.1 基礎：在 V3 基礎上繼續對 840B 個 token 進行預訓練，以進行長上下文擴展 Tokenizer 和聊天範本已更新 - 新的 tokenizer 設定： https://huggingface.co/deepseek-ai/DeepSeek- V3.1/blob/main/tokenizer_config.json V3.1 基礎開源權重： https://huggingface.co/deepseek-ai/DeepSeek-V3.1-Base V3.1 開源權重： https://huggingface.co/deepseek-ai/DeepSeek-V3.1 價格變動 新定價開始及非高峰折扣結束時間為 2025 年 9 月 5 日 16:00（UTC 時間） 在此之前，API 遵循當前定價 ...
張貼留言
閱讀完整內容