人工智能领域又迎来一项重大突破。DeepSeek在知名的Hugging Face平台上开源了一款专注于数学定理证明的大语言模型——DeepSeek – Prover – V2 – 671B。这一模型的参数规模高达 6710亿，采用了混合专家（MoE, Mixture – of – Experts）模式，最大位置嵌入达到了16.38万，展现出处理极其复杂数学证明问题的卓越能力。
DeepSeek – Prover – V2 – 671B并非普通的通用聊天机器人，而是一个高度专业化的系统，主要用于正式的定理证明，特别是使用Lean 4证明辅助语言。Lean 4是一种交互式工具，可用于将数学定义和证明形式化，并通过计算检查其正确性。DeepSeek – Prover – V2 – 671B与该框架相互配合，可能会以Lean 4语法生成或建议证明步骤，然后由Lean 4环境本身检查，以确保逻辑的合理性，旨在让复杂的形式验证任务变得更加易于处理。
在架构设计上，虽然该模型拥有庞大 6710 亿个参数，并以安全的safetensors格式分布存储，但由于采用了混合专家（MoE）架构，在推理过程中，只有一部分参数会被激活，有效平衡了模型规模与计算成本。这一创新设计不仅提升了模型的运行效率，也使得其在处理大规模数学问题时能够保持高效与准确。
这款模型的潜在应用场景十分广泛。它可以自动生成详细的证明步骤，帮助研究人员探索新的定理，为数学研究提供有力支持；能够检测现有证明中的错误，提升数学证明的准确性和可靠性；在教育领域，也可以辅助教学，帮助学生更好地理解复杂的数学证明过程。这一成果建立在DeepSeek之前的工作基础之上，例如70亿参数的DeepSeek – Prover – V1.5，后者采用了如强化学习与证明辅助反馈（RL PAF, Reinforcement Learning from Proof Assistant Feedback）等技术，而DeepSeek – Prover – V2 – 671B则在此基础上进行了大规模的升级与优化。
此次DeepSeek选择在Hugging Face平台开源DeepSeek – Prover – V2 – 671B，具有重要意义。Hugging Face作为全球知名的开源人工智能平台，拥有庞大的开发者社区和丰富的资源。通过在此平台开源，DeepSeek – Prover – V2 – 671B能够让全球更多的研究人员、开发者便捷地获取和使用该模型，促进数学定理证明领域的研究进展，推动人工智能与数学领域的深度融合与创新发展。
