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

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

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

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

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