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

Проблема формального математического рассуждения

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

Как работает DeepSeek-Prover-V2

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

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

Улучшения с помощью обучения с подкреплением

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

Результаты работы

DeepSeek-Prover-V2 показала высокие результаты на таких тестах, как MiniF2F-test и PutnamBench, решив 49 из 658 задач конкурса Путнама. Также модель успешно решила 6 из 15 задач последних соревнований AIME, демонстрируя прогресс в сближении неформальных и формальных методов. Однако комбинаторные задачи остаются проблемой, открывая направления для будущих исследований.

Новый эталон ProverBench

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

Открытый доступ и перспективы

DeepSeek-Prover-V2 доступен с открытым исходным кодом на платформах вроде Hugging Face, с вариантами от 7 до 671 миллиарда параметров, что позволяет использовать модель с разными вычислительными ресурсами. Это способствует развитию исследований, образовательных проектов и созданию продвинутых инструментов на базе ИИ для математики.

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