DeepSeek-Prover-V2: новый инструмент для автоматизации математических доказательств

Компания DeepSeek открыла исходный код инструмента для доказательства математических теорем — DeepSeek-Prover-V2.

Что представляет собой новая модель

DeepSeek-Prover-V2 — это специализированная языковая модель, разработанная для автоматического вывода и проверки математических теорем. Модель способна формализовать математические доказательства, что требует высокого уровня логического мышления, абстракции и точности.

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

Ключевая особенность Prover-V2 — использование обучения с подкреплением (RL) для математических доказательств. Процесс работы модели включает несколько этапов:

• DeepSeek-V3 разбивает сложные проблемы на серию подцелей, формируя структуру доказательства
• Вспомогательная модель формализует доказательство каждой подцели с использованием языка Lean 4
• DeepSeek-V3 интегрирует формализованные подцели в полное доказательство

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

Результаты тестирования

По данным разработчиков, DeepSeek-Prover-V2 демонстрирует следующие показатели:

• Решает около 90% математических задач из набора miniF2F
• Справляется с 49 из 658 проблем на PutnamBench
• Способна решать задачи уровня AIME (Американская математическая олимпиада)

Доступные версии

Выпущены две версии модели:

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

Обе модели доступны на Hugging Face и GitHub с соответствующей лицензией.

Значение для научного сообщества

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

#DeepSeek #МатематическиеДоказательства #ИскусственныйИнтеллект