Во время первомайских праздников компания DeepSeek в очередной раз принесла в сферу ИИ тяжелую новость - открыла доступ к новой модели DeepSeek-Prover-V2. Несмотря на слухи о скором выходе DeepSeek-R2, DeepSeek выпустила эту мощную модель, ориентированную на математическое доказательство теорем, и продолжает придерживаться своего обычного духа открытого кода.

Две мощные модели, синхронизированные с открытым исходным кодом

На этот раз DeepSeek выложила в открытый доступ две версии модели DeepSeek-Prover-V2.

• DeepSeek-Prover-V2-671B: Построенный на базе DeepSeek-V3-Base с 671 миллиардом параметров, он на данный момент является королем производительности в доказательстве теорем.
• DeepSeek-Prover-V2-7B: Построен на базе DeepSeek-Prover-V1.5-Base, имеет 7 миллиардов параметров и поддерживает длину контекста до 32K токенов

Обе модели были официально выпущены на сайте Hugging Face:

• DeepSeek-Prover-V2-7B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
• DeepSeek-Prover-V2-671B. https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

Что такое DeepSeek-Prover-V2?

DeepSeek-Prover-V2 - это модель большого языка с открытым исходным кодом для "математического языка программирования ИИ" Lean 4, ориентированная на формальное доказательство теорем. Проще говоря, он может преобразовывать абстрактные математические теоремы в строгие доказательства, проверяемые на компьютере, что является революционным инструментом для математических исследований.

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

Потрясающая производительность: установление множества рекордов

DeepSeek-Prover-V2-671B демонстрирует беспрецедентную силу в различных бенчмарках по доказательству теорем:

• Достигнут рекордный показатель прохождения теста MiniF2F - 88,9%
• Успешно решено 49 из 658 вопросов в наборе данных PutnamBench
• Также хорошо справляется с трудными конкурсными задачами по математике, такими как AIME 24 и 25.

Многие нетизены протестировали модель и заявили, что она способна решать сложные математические задачи даже лучше, чем такие топовые модели, как o4-mini от OpenAI и Grok-3 от XAI. Некоторые студенты, участвовавшие в олимпиаде по математике, воскликнули: "Никогда еще олимпиада не была такой легкой!"

Технологические инновации: сочетание рекурсивного обучения и обучения с подкреплением

В техническом отчете команда DeepSeek раскрывает основную методологию обучения Prover-V2, которая основана на инновационной комбинации рекурсивного обучения + обучения с подкреплением. Процесс обучения модели разделен на несколько ключевых этапов:

1. Рекурсивный поиск доказательств с помощью декомпозиции подцелей

DeepSeek-Prover-V2 использует способ мышления, схожий с мышлением человека-математика - разбиение сложных теорем на ряд более мелких лемм для доказательства. Конкретный процесс реализации включает в себя:

• Сначала DeepSeek-V3 предлагается сгенерировать наброски доказательств на естественном языке и формализовать их в виде утверждений теорем на языке Lean.
• Декомпозированные подцели затем решаются рекурсивно с использованием модели доказательства 7B
• Наконец, доказательства этих подцелей объединяются для построения полного формального доказательства исходной сложной задачи

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

2. гармонизация неформальных рассуждений с формальными доказательствами

Команда DeepSeek умело сочетает высокоуровневые рассуждения на естественном языке с низкоуровневыми процессами точного доказательства:

• Выберите проблемы, которые особенно трудно решить, и разбейте их на более мелкие цели
• Когда каждая из мини-целей доказана, они объединяются в полное строгое доказательство
• Добавьте это полное доказательство к "цепочке мыслей", созданной DeepSeek-V3, чтобы сформировать обучающие данные, сочетающие человеческое мышление и машинную проверку.

Таким образом, команда собрала сотни высококачественных обучающих данных, обеспечив прочную основу для обучения модели.

3. Расширенное обучение для улучшения навыков рассуждения

После первоначальной настройки команда внедрила алгоритм подкрепляющего обучения Group Relative Policy Optimization (GRPO):

• Выборка нескольких доказательств кандидатов для каждого вопроса и оптимизация стратегии по относительным вознаграждениям
• Использование бинарного механизма вознаграждения: за успешную проверку Lean получает 1 балл, за неудачную - 0.
• Бонус структурной согласованности специально разработан для того, чтобы гарантировать, что доказательства, генерируемые моделью, согласуются с идеями декомпозиции цепочки мыслей.

Этот метод обучения значительно повышает точность модели при доказательстве сложных теорем.

ProverBench: новый набор математических эталонов

Помимо самой модели, DeepSeek выпустила ProverBench - эталонный набор данных из 325 вопросов:

• 15 вопросов по теории чисел и алгебре из последних математических конкурсов, таких как AIME 24 и 25
• 310 вопросов, отобранных из примеров учебника и учебных пособий, охватывающих широкий спектр уровней сложности и областей.

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

ProverBench Link:https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

Экспериментальные результаты и основные выводы

В ходе исследования команда обнаружила несколько интересных явлений:

Модели CoT и модели без CoT

DeepSeek-Prover-V2 поддерживает два взаимодополняющих режима генерации доказательств:

• Высокоэффективная модель без цепочки мыслей (non-CoT): Быстрая генерация бережливого кода Lean без промежуточных шагов вывода
• Высокоточная модель цепи мышления (CoT): систематическое представление процесса рассуждений и постепенное построение логически ясных доказательств

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

Неожиданные возможности маленьких моделей

Удивительно, но DeepSeek-Prover-V2-7B превзошел все ожидания при использовании не-CoT-модели в наборе данных PutnamBench. Она даже решила 13 вопросов, которые не смогла решить модель 671B!

Анализ показал, что модель 7B приобрела уникальную технику - частое использование Cardinal.toNat и Cardinal.natCast_inj для решения задач с конечными основаниями, - которая редко встречается в модели 671B. Этот вывод говорит о том, что обучение с подкреплением не только улучшает общую производительность, но и позволяет модели развивать специализированные методы решения задач.

Краткое руководство пользователя

Хотите попробовать DeepSeek-Prover-V2? Вот простой пример, показывающий, как использовать библиотеку Hugging Face's Transformers для вывода модели:

from transformers import AutoModelForCausalLM, AutoTokenizer
импортировать факел

torch.manual_seed(30)
model_id = "deepseek-ai/DeepSeek-Prover-V2-7B" # или deepseek-ai/DeepSeek-Prover-V2-671B
tokenizer = AutoTokenizer.from_pretrained(model_id)

formal_statement = """
import Mathlib
import Aesop
set_option maxHeartbeats 0
open BigOperators Real Nat Topology Rat
/-- Какова положительная разность между $120\%$ из 30 и $130\%$ из 20? Покажите, что она равна 10.-/
Теорема mathd_algebra_10 : abs ((120 : ℝ) / 100 * 30 - 130 / 100 * 20) = 10 := by
    извините
""".strip()

prompt = """
Выполните следующий код Lean 4.
 ``lean4
{}

прогноз на будущее

Команда DeepSeek утверждает, что в будущем работа будет сосредоточена на расширении этого фреймворка до AlphaProof-подобных систем. Конечной целью является решение математических головоломок уровня IMO, которые представляют собой передний край области автоматизированного доказательства теорем. С выходом DeepSeek-Prover-V2 мы можем стать свидетелями серьезных изменений в изучении математики. Эта модель представляет собой не просто технологическое достижение, а новую парадигму сотрудничества человека с искусственным интеллектом для решения сложных задач.

Тем временем ожидание DeepSeek-R2 становится все сильнее. Как сказал один из нетизенов: "Тук-тук, этот маленький синий кит, когда же, черт возьми, выйдет R2!".

Если вы хотите использовать официальный платный эксклюзивный аккаунт GPT Plus, Claude Pro, Grok Super, вы можете связаться с нашей профессиональной командой (wx: abch891), если вы не знаете, как пополнить свой счет.