DeepSeek Prover V2 — новая китайская LLM для математических задач

30 апреля 2025 года китайская компания DeepSeek без каких-либо предварительных заявлений выпустила свою новую языковую модель — Prover V2 671b, которая предназначена для решения математических и логических задач. Компания заявляет, что Prover V2 базируется на нейросети DeepSeek V3 с 671 миллиардов параметров на архитектуре MoE, которая получила крупное обновление в прошлом месяце для улучшения возможностей кодинга и решения математических задач.

DeepSeek Prover V2 является преемником нейросети Prover V1.5, которая вышла в августе 2024 года и показала неплохие результаты в решении математических и логических задач. Новая версия Prover V2 основана на конвейере доказательства теорем на языке программирования Lean4, который использовался в нейросети DeepSeek V3. Конвейер старшей нейросети DeepSeek V3 разбивает комплексные задачи на несколько более простых подзадач, которые впоследствии выстраиваются в логическую цепочку для формирования более точных, релевантных результатов. Это позволяет автоматизировать проверку доказательств, находить ошибки в рассуждениях и генерировать пошаговые решения для задач от школьного уровня до олимпиадных, обеспечивая 100% логическую точность.  Также при обучении DeepSeek Prover V2 использовался так называемый “холодный старт”, то есть обучение на уже готовом наборе синтетических данных из 8 миллиардов примеров, который дополнен новой информацией для достижения наибольшей производительности. По всей видимости, набор данных модель Prover V2 также унаследовала у более старшего собрата DeepSeek V3. Для еще большей оптимизации производительности, для обучения DeepSeek Prover V2 применялся метод подкрепления, при котором нейросеть получает дополнительную мотивацию в виде бинарной схемы “верно/неверно”. 

Также стоит отметить, что помимо старшей модели DeepSeek Prover V2 671b, разработчики также представили облегченную версию Prover V2 7b, которая базируется на модели DeepSeek-Prover-V1.5-Base и имеет расширенный контекст длиной до 32 тысяч токенов. В данный момент обе нейросети доступны для скачивания только в репозитории Hugging Face. Для оценки DeepSeek Prover V2 компания также разработала специальный тест ProverBench, который состоит из 325 задач, из которых 15 задач формализованы на основе вопросов по теории чисел и алгебре, представленных на недавних соревнованиях AIME (AIME 24 и 25), и представляют собой задачи, соответствующие уровню соревнований для старшеклассников. Остальные 310 задач взяты из тщательно отобранных примеров в учебниках и учебных пособий, например, комплексный анализ, линейная и абстрактная алгебра, теория вероятности и так далее. Этот тест разработан для более всесторонней оценки как задач для школьных олимпиад, так и математических задач для студентов. Prover-V2 успешно решает задачи из бенчмарка PutnamBench и демонстрирует точность в 88.9% при решении теста MiniF2F.

Примечательно, что модели DeepSeek Prover V2 вышли на следующий день после релиза передового семейства нейросетей Qwen 3 от Alibaba. Этот релиз еще больше усиливает влияние китайских LLM на мировую индустрию искусственного интеллекта и, возможно, готовит сообщество к релизу новой, мультимодальной нейросети DeepSeek R2, слухи о которой начали курсировать в сети на этой неделе.