DeepSeek представила модель DeepSeekMath-V2 — специализированный ИИ для решения сложных задач и доказательства теорем, который впервые для открытой модели выходит на "золотой" уровень Международной олимпиады по математике (IMO-2025) и Китайской математической олимпиады CMO-2024. По данным команды, DeepSeekMath-V2 набирает до 118 баллов из 120 в задачах Putnam-2024. Модель распространяется с открытыми весами по лицензии Apache-2.0 и уже доступна на Hugging Face.
DeepSeekMath-V2 построена поверх базовой модели DeepSeek-V3.2-Exp-Base и тренируется в связке "генератор + проверяющий". Отдельный верификатор оценивает корректность шагов доказательства, а генератор получает поощрение за выводы, которые проходят проверку.
Авторы подчеркивают, что в отличие от большинства открытых математических моделей, DeepSeekMath-V2 ориентирована именно на строгие доказательства, а не только на финальный числовой ответ. На практике это позволяет ИИ решать задачи олимпиадного уровня, сопровождая решение подробным обоснованием — раньше такое было доступно только закрытым моделям вроде Gemini 2.5 DeepThink и экспериментального ИИ компании OpenAI. Теперь аналогичного уровня впервые достигла открытая модель.
Размер модели впечатляет: в описании указано 685 млрд параметров, а комплект весов в формате fp8 на Hugging Face занимает порядка 690 ГБ, что делает запуск дома малореалистичным — нужна инфраструктура уровня небольшого исследовательского кластера. Для DeepSeekMath-V2 команда предоставляет открытый доступ к весам и подробное техническое описание, а также тесную интеграцию с формальными доказчиками вроде DeepSeek-Prover-V2, которые переводят доказательство в популярный формат Lean.
P.S. Поддержать меня можно подпиской на канал "сбежавшая нейросеть", где я рассказываю про ИИ с творческой стороны.
