DeepSeek Prover-V2: Революция в формальном математическом доказательстве
DeepSeek Prover-V2 — это специализированная языковая модель с 671 миллиардом параметров, разработанная для доказательства математических теорем в системе формальной верификации Lean 4. В отличие от обычных языковых моделей, она не предназначена для общего использования, а является узкоспециализированным инструментом для математиков и исследователей, работающих с формальными доказательствами.
Модель выпущена в двух версиях:
- DeepSeek Prover-V2-671B — большая версия с 671 миллиардом параметров
- DeepSeek Prover-V2-7B — компактная версия с 7 миллиардами параметров
Как это работает?
Ключевая инновация модели заключается в ее методе обучения через декомпозицию подцелей с помощью обучения с подкреплением.
- Декомпозиция сложных проблем: Модель использует DeepSeek-V3 для разбиения сложных теорем на серию подцелей.
- Рекурсивный поиск доказательств: Небольшая модель (7B) используется для обработки доказательств отдельных подцелей, что снижает вычислительную нагрузку.
- Синтез данных холодного старта: Когда все декомпозированные шаги сложной проблемы решены, модель объединяет полное пошаговое формальное доказательство с соответствующим цепочкой рассуждений от DeepSeek-V3.
- Обучение с подкреплением: После тонкой настройки на синтетических данных модель проходит этап обучения с подкреплением для дальнейшего улучшения своей способности связывать неформальные рассуждения с формальным построением доказательств.
Благодаря этому процессу DeepSeek Prover-V2 может эффективно интегрировать как неформальные, так и формальные математические рассуждения в единую модель.
Рекордная производительность
- 88.9% успеха на тестовом наборе MiniF2F (формальные математические задачи олимпиадного уровня)
- 49 из 658 задач решено на PutnamBench (задачи из математического конкурса Путнама)
- Значительный уровень успеха на формальных версиях задач из AIME 24 и 25 (Американский конкурс по математике)
Это делает DeepSeek Prover-V2 передовой моделью в области нейронного доказательства теорем.
ProverBench: Новый бенчмарк для оценки моделей
Вместе с моделью команда DeepSeek представила ProverBench — набор из 325 формализованных математических задач для оценки моделей доказательства теорем. Этот бенчмарк включает:
- 15 задач из конкурсов AIME 24 и 25
- 310 задач из различных областей математики, от элементарной алгебры до функционального анализа
Ключевые показатели эффективности:
Сравнение с другими моделями и бенчмарками
Для чего можно использовать DeepSeek Prover-V2?
- Автоматическое доказательство теорем: Решение математических задач от школьного до университетского уровня с генерацией пошаговых доказательств.
- Поиск ошибок в доказательствах: Обнаружение ошибок в доказательствах, созданных людьми или другими моделями ИИ.
- Обучение и исследования: Помощь студентам и исследователям в понимании формальных доказательств через генерацию объяснений параллельно с кодом Lean 4.
- Математические исследования: Помощь математикам в исследовании новых теорем путем автоматического испробования различных стратегий доказательства.
Что такое Lean 4?
Lean 4 — это система интерактивного доказательства теорем, которая сочетает возможности программирования и формальной верификации. Она позволяет математикам выражать теоремы и доказательства на языке, который может быть строго проверен компьютером. Это обеспечивает 100% логическую точность каждого шага доказательства.
В последние годы Lean 4 набирает популярность среди математиков для формализации сложных математических результатов, обеспечивая их абсолютную надежность.