DeepSeek выпускает DeepSeek-Prover-V2-671B: новая модель автодоказательства теорем с 671 млрд параметров на архитектуре MoE 61

小编 · 2025-04-30

DeepSeek AI 30 апреля 2025 года выпустила DeepSeek-Prover-V2-671B — модель автодоказательства теорем нового поколения с 671 млрд параметров на архитектуре MoE, генерирующую и проверяющую доказательства в рамках Lean 4. Преимущества: вывод формальной математики на уровень GPT-4, повышение эффективности за счёт MoE, открытый исходный код и коммерческое использование. По сравнению с V1.5 значительно увеличено число параметров

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

DeepSeek ai 30 апреля 2025 года выпустила DeepSeek-Prover-V2-671B — модель автоматического доказательства теорем нового поколения, построенную на архитектуре MoE с 671 миллиардом параметров, которая генерирует и проверяет доказательства в рамках Lean 4. Её преимущества включают вывод формальной математики на «уровень GPT-4», повышение эффективности благодаря MoE, открытый исходный код и возможность коммерческого использования. По сравнению с версией V1.5 она демонстрирует значительные улучшения в количестве параметров, длине контекста, проценте успешных прохождений и других показателях. Ожидается, что модель покажет отличные результаты в бенчмарках, таких как miniF2F, и может использоваться в таких областях, как формальная верификация и ускорение математических исследований. Для использования необходимо загрузить веса с Hugging Face и выполнить соответствующие настройки.

DeepSeek发布DeepSeek-Prover-V2-671B：基于6710亿参数MoE架构的下一代自动定理证明模型.webp

Технические особенности

Количество параметров и архитектура: общий объём параметров модели составляет 671 миллиард, используется архитектура MoE, при этом для каждого токена активируется около 37 миллиардов параметров. Такая архитектура значительно снижает потребление памяти при сохранении мощных возможностей рассуждения.
Длина контекста: поддерживается сверхдлинный контекст, максимальное позиционное вложение достигает 163840, что позволяет обрабатывать сложные математические доказательства.
Вычислительная точность: поддерживаются多种 вычислительных точностей, такие как BF16, FP8, F32, что ускоряет и делает более ресурсоэффективным обучение и развёртывание модели.
Формат файлов: используется более эффективный формат файлов safetensors.
Технология квантования: применяется квантование FP8, уменьшающее размер модели и повышающее эффективность вывода за счёт технологий квантования.

技术特点.webp

Ключевые преимущества

Масштаб и сложность: огромное количество параметров и длинное окно контекста (около 128k токенов) позволяют обрабатывать более длинные и сложные цепочки логики математических доказательств.
Оптимизация эффективности: архитектура MoE значительно снижает потребление памяти и повышает скорость вывода по сравнению с полносвязной моделью с 671 миллиардом параметров.
Открытый исходный код и лицензия: модель имеет открытый исходный код, веса доступны на Hugging Face, и предполагается разрешение коммерческого использования.

Сценарии применения

Формальная верификация: проведение строгих проверок при доказательстве криптографической безопасности или корректности проектирования микросхем.
Ускорение математических исследований: помощь математикам в формализации существующих теорем, исследовании новых гипотез и решении олимпиадных математических задач.
Продвинутые образовательные инструменты: создание интерактивных систем обучения, направляющих студентов в выполнении формальных доказательств.
Системы с высокими требованиями к безопасности: проверка критических свойств и инвариантов программного обеспечения через интеграцию с Lean перед развёртыванием кода.

Шаги для быстрого старта

Получение модели: загрузите веса с Hugging Face: deepseek-ai/DeepSeek-Prover-V2-671B.
Настройка Lean: установите Lean 4 (рекомендуется версия ≥ 4.5) и библиотеку mathlib4.
Проверка оборудования: убедитесь, что конфигурация оборудования соответствует минимальным требованиям (рекомендуется высокопроизводительная конфигурация).
Установка движка вывода: настройте, например, vLLM или другой фреймворк, совместимый с MoE.
Изучение примеров: проверьте скрипты оценки или примеры блокнотов в репозитории модели.

Часто задаваемые вопросы

Является ли модель открытой? Можно ли использовать её в коммерческих целях?

Да, DeepSeek-Prover-V2-671B имеет открытый исходный код (веса доступны на Hugging Face), и предполагается, что её лицензия разрешает как академическое, так и коммерческое использование.

Можно ли запустить модель на NVIDIA 4090?

Согласно предварительным отчётам, благодаря таким оптимизациям, как MoE, MLA и квантование, модель может работать на одном GPU NVIDIA 4090, особенно при достаточном объёме оперативной памяти и быстром NVMe SSD для динамической загрузки. Производительность будет зависеть от конкретной конфигурации.