開放程式碼數學 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

留言

這個網誌中的熱門文章

美國公布 2025 年六月非農就業人數

美國勞工統計局今天報告稱，6 月非農業就業總人數增加了 14.7 萬人，失業率基本持平於 4.1%。州政府和醫療保健領域的就業機會增加。聯邦政府部門的就業機會持續減少。本新聞稿提供的統計數據來自兩項月度調查。家庭調查以人口統計特徵衡量勞動力狀況，包括失業率。機構調查以行業衡量非農業就業人數、工時和收入。家庭調查數據 6月份，失業率為 4.1%，失業人數為 700 萬，兩者皆變化不大。自2024年5月以來，失業率一直維持在 4.0% 至 4.2% 的窄幅區間內。在主要勞動族群中，非裔美國人（6.8%）的失業率在6月有所上升，而成年女性（3.6%）和白人（3.6%）的失業率則下降。成年男性（3.9%）、青少年（14.4%）、亞裔（3.5%）和西班牙裔（4.8%）的失業率在當月幾乎沒有變化。 6 月份，長期失業人數（失業 27 週或以上）增加了 19 萬，達到 160 萬，基本上抵消了上個月的降幅。長期失業者佔所有失業人口的 23.3%。 6 月份，勞動參與率基本維持不變，為 62.3%，就業人口比率維持在 59.7%。 6 月份，因經濟原因從事兼職工作的人數為 450 萬，基本維持不變。這些人原本更傾向於全職工作，但由於工作時間減少或無法找到全職工作，他們只能從事兼職工作。 6 月份，目前希望就業但未加入勞動力的人數基本保持不變，為 600 萬人。這些人未被計入失業人數，因為他們在調查前 4 週內沒有積極尋找工作，或無法接受工作。在希望就業但未加入勞動力隊伍的人數中，6 月處於邊緣就業狀態的人數增加了 23.4 萬人，達到 180 萬人。這些人希望工作，並且能夠工作，在過去 12 個月的某個時間點尋找工作，但在調查前 4 週內沒有尋找工作。灰心喪志的工人（邊緣就業人群中的一部分，他們認為沒有工作機會）的人數在 6 月增加了 25.6 萬人，達到 63.7 萬人。機構調查數據 6月份非農業就業總人數增加了 14.7 萬個，與過去 12 個月平均每月增加 14.6 萬個的水平持平。6月份，州政府和醫療保健領域的就業機會增加。聯邦政府的就業機會持續減少。 6月政府就業機會增加了 7.3 萬個。州政府就業機會增加了4.7萬個，主要集中在教育領域（增加了4萬個）。地方政府教育領域的就業機會持續增加（增加了2.3萬個）。聯邦政府就業機會持續減少（減少了7千個），自1月...

閱讀完整內容

Kyutai Labs 發布最新文字轉語音 AI 模型 - Kyutai TTS

法國 AI 研究機構 Kyutai Labs 發布最新文字轉語音 AI 模型 - Kyutai TTS，這是一個即時低延遲，並擁有 16 億參數的模型，包含多項創新。 Kyutai TTS 引領了文字轉語音領域的新潮流。詞錯率(WER) 衡量的是 TTS 未能遵循腳本的頻率。說話人相似度是語音複製時衡量產生的音訊與原始樣本的接近程度的指標。 Kyutai Labs 將 Kyutai TTS 與其他模型在 NTREX 的 15 篇英文新聞和 15 篇法文新聞上進行了比較。除 Kyutai TTS 和 ElevenLabs 外，所有模型都被要求逐句生成，因為我們觀察到這種方式效果最佳。 Kyutai TTS 無需提前了解整個文本，從接收第一個文本標記到生成第一個音頻區塊的延遲為 220 毫秒。在Unmute.sh部署中，我們使用批次功能同時處理最多 32 個請求，使用 L40S GPU 時觀察到延遲為 350 毫秒。 Kyutai STT 模型針對即時使用進行了最佳化，可以批量處理以提高效率，並返回單字級時間戳記。我們提供兩種模型： kyutai/stt-1b-en_fr，一個具有約 1B 個參數、0.5 秒延遲和語義 VAD 的英語和法語模型。 kyutai/stt-2.6b-en，一個僅支援英語的模型，具有約 26 億個參數和 2.5 秒的延遲。這些語音轉文字模型有幾個優點：流式推理：模型可以分塊處理音頻，從而實現即時轉錄，非常適合互動式應用程式。輕鬆批次處理以實現最高效率：H100 可以即時處理 400 個串流。它們傳回單字級時間戳。 1B 模型具有語義語音活動偵測 (VAD) 元件，可用於偵測使用者何時說話。這對於建立語音代理尤其有用。 https://kopyai.com/zh-tw/latest/view/type.news/0/39 Picture Source: kyutai.org

閱讀完整內容

微軟發布輕量級推理模型 Phi-4-mini-flash-reasoning

微軟推出 Phi 模型系列的新版本 - Phi-4-mini-flash-reasoning，此新模型專為運算、記憶體和延遲受到嚴格約束的場景而設計，旨在為邊緣設備、行動應用程式和其他資源受限的環境帶來高級推理能力。新模型沿用 Phi-4-mini，但建立在一種新的混合架構上，吞吐量提高了 10 倍，延遲平均降低了 2 到 3 倍，在不犧牲推理性能的情況下實現了顯著加快的推理速度。 Phi-4-mini-flash-reasoning 在數學推理能力和效率之間取得平衡，使其可能適用於教育應用、基於即時邏輯的應用等。與前代產品類似，Phi-4-mini-flash-reasoning 是一個擁有 38 億個參數的開放模型，並針對高階數學推理進行了最佳化。它支援 64K 的 token 上下文長度，並基於高品質合成資料進行了微調，以提供可靠的邏輯密集型效能部署。 Phi-4-mini-flash-reasoning 的核心是全新引入的解碼器-混合解碼器架構 SambaY，其核心創新在於門控記憶單元 (GMU)，這是一種簡單而有效的跨層共享表徵機制。該架構包含一個自解碼器，它結合了 Mamba（狀態空間模型）和滑動視窗注意力 (SWA)，以及一個單層全注意力機制。此外，該架構還包含一個交叉解碼器，它將昂貴的交叉注意力層與全新的高效 GMU 交錯排列。這種具有 GMU 模組的新架構顯著提升了解碼效率，增強了長上下文檢索效能，並使該架構能夠在各種任務中提供卓越的效能。 SambaY 架構的主要優勢包括：增強解碼效率。保留線性預歸檔時間複雜度。提高了可擴展性並增強了長上下文效能。吞吐量提高高達 10 倍。與 Phi 系列的所有模型一樣，Phi-4-mini-flash-reasoning 可部署在單 GPU 上，從而適用於廣泛的用例。然而，它的獨特之處在於其架構優勢。與 Phi-4-mini-reasoning 相比，這個新模型實現了顯著更低的延遲和更高的吞吐量，尤其是在長上下文生成和延遲敏感型推理任務中。這使得 Phi-4-mini-flash-reasoning 成為希望部署需要快速、可擴展和高效推理的智慧型系統的開發人員和企業的引人注目的選擇——無論是在本地還是在設備上。 h...

閱讀完整內容

Kopy AI Blog

搜尋此網誌