DeepSeek AI представляет DeepSeekMath-V2 для олимпиадных доказательств

Обзор DeepSeekMath-V2

DeepSeek AI запустила DeepSeekMath-V2, модель с открытыми весами, оптимизированную для доказательства теорем на естественном языке с само-проверкой. Эта модель основана на DeepSeek-V3.2-Exp-Base и имеет 685B параметров, доступна для развертывания под лицензией Apache 2.0 на Hugging Face.

Основные результаты оценок

DeepSeekMath-V2 набрала 118 из 120 баллов на Патнаме 2024, достигнув золотых отметок на IMO 2025 и CMO 2024 с использованием масштабируемых вычислений времени тестирования.

Проблема с конечными ответами

Большинство математических моделей используют обучение с подкреплением, награждая только конечный ответ. Однако команда DeepSeek обнаружила важные проблемы с таким подходом:

1. Правильные числовые ответы могут быть получены из неверного рассуждения.
2. Такие задачи, как олимпиадные доказательства, требуют полного аргумента, а не единственного числового решения.

DeepSeekMath-V2 акцентирует внимание на качестве доказательства, а не только на точности ответов. Модель оценивает завершенность и логическую согласованность доказательства как основные сигналы обучения.

Подход с обучением на верификаторе

Система начинается с подхода “верификатор первым”. Команда разработки обучает верификатор на LLM, который оценивает задачу и предложенное доказательство, предоставляя как анализ, так и балл в шкале 1.

Начальные данные для обучения с подкреплением получены из конкурсов Art of Problem Solving, охватывающих 17,503 задачи, требующих доказательства. Эксперты оценивают доказательства по установленным критериям, обеспечивая строгость и полноту.

Введение мета-верификатора

Чтобы предотвратить эксплуатацию процесса верификации, включен мета-верификатор. Он проверяет исходную задачу и анализ верификатора, оценивая правдоподобность и согласованность анализа. Расширенное обучение с GRPO позволяет мета-верификатору значительно повысить средние оценки качества.

Генератор самопроверяемых доказательств

После усиления верификатора команда обучает генератор доказательств, который создает решения вместе с самоанализом, награждая производительность на основе нескольких критериев, включая согласие с оценкой верификатора.

Масштабирование верификации с автоэтикетированием

Чтобы сделать процесс оценки трудоемких задач эффективным, разработана автоматическая система этикетирования, использующая методы масштабированной верификации, позволяющие проверять кандидатные доказательства на основании многократной независимой оценки.

Результаты производительности на соревнованиях

На различных конкурсных фронтах DeepSeekMath-V2 последовательно превосходит показатели:

• Решилось 5 из 6 задач IMO 2025 на уровне золотой медали.
• Получено 4 полных решения и частичный балл на CMO 2024.
• Рекордный результат 118 из 120 на Патнаме 2024, опережая лучший результат человека в 90.

Итоги новшеств

• Модель с 685B параметрами акцентирует внимание как на само-проверке, так и на качестве доказательства, выпущена в качестве открытых весов.
• Нейросеть совмещает верификатор и мета-верификатор, чтобы подчеркивать логическую полноту, а не только правильность.
• Этот подход позволяет DeepSeekMath-V2 преуспеть на олимпиадах, укрепляя свою позицию как ведущей модели в решении математических задач.

Редакционная перспектива

DeepSeekMath-V2 представляет собой важный шаг к само-проверяемому математическому мышлению, преодолевая разрыв между правильными ответами и строгой логикой. Его развертывание демонстрирует практический подход к решению задач в соревнованиях.