Согласно PANews, DeepSeek выпустил новую модель с открытым исходным кодом, DeepSeek-Prover-V2-671B, сосредоточенную на задачах доказательства математических теорем. Модель построена на архитектуре смешанных экспертов (MoE) и использует фреймворк Lean 4 для обучения формальному рассуждению. С масштабом параметров в 671 миллиард, она сочетает в себе обучение с подкреплением и крупномасштабные синтетические данные, чтобы значительно улучшить возможности автоматического доказательства. Модель теперь доступна на Hugging Face, поддерживая как локальное развертывание, так и коммерческое использование.