人工智能領(lǐng)域又迎來一項重大突破。DeepSeek在知名的Hugging Face平臺上開源了一款專注于數(shù)學定理證明的大語言模型——DeepSeek – Prover – V2 – 671B。這一模型的參數(shù)規(guī)模高達 6710億，采用了混合專家（MoE, Mixture – of – Experts）模式，最大位置嵌入達到了16.38萬，展現(xiàn)出處理極其復雜數(shù)學證明問題的卓越能力。?

DeepSeek – Prover – V2 – 671B并非普通的通用聊天機器人，而是一個高度專業(yè)化的系統(tǒng)，主要用于正式的定理證明，特別是使用Lean 4證明輔助語言。Lean 4是一種交互式工具，可用于將數(shù)學定義和證明形式化，并通過計算檢查其正確性。DeepSeek – Prover – V2 – 671B與該框架相互配合，可能會以Lean 4語法生成或建議證明步驟，然后由Lean 4環(huán)境本身檢查，以確保邏輯的合理性，旨在讓復雜的形式驗證任務(wù)變得更加易于處理。?

在架構(gòu)設(shè)計上，雖然該模型擁有龐大 6710 億個參數(shù)，并以安全的safetensors格式分布存儲，但由于采用了混合專家（MoE）架構(gòu)，在推理過程中，只有一部分參數(shù)會被激活，有效平衡了模型規(guī)模與計算成本。這一創(chuàng)新設(shè)計不僅提升了模型的運行效率，也使得其在處理大規(guī)模數(shù)學問題時能夠保持高效與準確。?

這款模型的潛在應(yīng)用場景十分廣泛。它可以自動生成詳細的證明步驟，幫助研究人員探索新的定理，為數(shù)學研究提供有力支持；能夠檢測現(xiàn)有證明中的錯誤，提升數(shù)學證明的準確性和可靠性；在教育領(lǐng)域，也可以輔助教學，幫助學生更好地理解復雜的數(shù)學證明過程。這一成果建立在DeepSeek之前的工作基礎(chǔ)之上，例如70億參數(shù)的DeepSeek – Prover – V1.5，后者采用了如強化學習與證明輔助反饋（RL PAF, Reinforcement Learning from Proof Assistant Feedback）等技術(shù)，而DeepSeek – Prover – V2 – 671B則在此基礎(chǔ)上進行了大規(guī)模的升級與優(yōu)化。

此次DeepSeek選擇在Hugging Face平臺開源DeepSeek – Prover – V2 – 671B，具有重要意義。Hugging Face作為全球知名的開源人工智能平臺，擁有龐大的開發(fā)者社區(qū)和豐富的資源。通過在此平臺開源，DeepSeek – Prover – V2 – 671B能夠讓全球更多的研究人員、開發(fā)者便捷地獲取和使用該模型，促進數(shù)學定理證明領(lǐng)域的研究進展，推動人工智能與數(shù)學領(lǐng)域的深度融合與創(chuàng)新發(fā)展。