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