DeepSeek выпустили новую модель с фокусом на математике и логике разбираем что за зверь
С утра на HuggingFace появилась новая моделька от китайцев. Пока все ждали R2, в свет вышла модель DeepSeek Prover V2.
Что это за модель и почему раньше о ней не говорили?
Как можно видеть из названия, это вторая версия модели, а не говорили о них лишь потому, что до R1 за DeepSeek следили только гики. Моделька предназначена для решения логических и математических задач на языке формальных доказательств Lean 4. В целом, сфера формальной логики у LLM сейчас довольно сильно страдает, и цель этой модели – как раз исправить это.
Модельку специально тренировали на имитацию процесса рассуждения, но без традиционных сворачиваемых “мыслей”, которые мы видим у других моделей. Попробуйте дать ей задачку на логику - поймете, о чем я.
Как они этого добились?
Если коротко, то применили хитрый подход:
1. Разбивка и синтез: Использовали DeepSeek-V3, чтобы та разложила сложные теоремы на шаги и сгенерировала "черновики" доказательств, соединяя неформальные рассуждения с формальным кодом.
2. Оптимизация: Для решения подзадач использовали модель поменьше (7B), чтобы сэкономить ресурсы.
3. Дообучение: Полученную модель-прувер докрутили с помощью обучения с подкреплением (RL), поощряя за верные формальные шаги.
Идея в том, чтобы научить модель не просто генерировать текст, похожий на математический, а именно строить формальные доказательства, связывая их с логикой рассуждения.
Результаты и бенчмарк
Флагманская 671B модель показала себя очень неплохо: 88.9% успеха на стандартном тесте MiniF2F и решила почти полсотни задач из сложного университетского PutnamBench.
Чтобы лучше тестировать такие модели, DeepSeek даже создали свой бенчмарк – ProverBench, куда включили задачи с реальных олимпиад (AIME) и из учебников. Это важно для оценки на разнообразных и практически значимых примерах.
Доступные модели
Выпустили две версии:
DeepSeek-Prover-V2-7B: Младшая, с увеличенным до 32K токенов контекстом.
DeepSeek-Prover-V2-671B: Старшая, на базе новейшей DeepSeek-V3, показывающая топовые результаты.
Что в итоге?
Появление DeepSeek Prover V2 – интересный шаг к тому, чтобы LLM стали лучше справляться с логикой и математикой. Их подход к обучению, имитирующий процесс доказательства, выглядит многообещающе. Но есть и свои минусы, например, нам уже известно, что RL часто ведет к тому, что модели ВРУТ, что показали нам OpenAI. + я немного потыкал модель, с моими задачками на логику она не справилась 🙂
Модель доступна на OpenRouter HuggingFace https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B поменьше (7B) https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B OpenRouter https://openrouter.ai/deepseek/deepseek-prover-v2:free We’re on a journey to advance and democratize artificial intelligence through open source and open science. deepseek-ai/DeepSeek-Prover-V2-671B · Hugging Face