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