DeepSeek представила Proofver V2 для формальных математических доказательств

1. Введение

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

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

2. Обзор модели

Для создания начального набора данных мы разработали систему рекурсивного доказательства теорем, используя DeepSeek-V3 в качестве универсального инструмента. Процесс начинается с декомпозиции теорем в высокоуровневые схему доказательства, при этом каждый шаг формализуется в Lean 4, что приводит к последовательности подцелей. Модель с 7 миллиардов параметров обрабатывает поиск доказательств для этих подцелей, что снижает вычислительную нагрузку. Когда все подцели решены, мы объединяем пошаговое формальное доказательство с цепочкой рассуждений от DeepSeek-V3. Этот синтез создает основу для обучения с подкреплением, где соңča конструкции модели происходит на основе бинарной обратной связи. В результате, модель DeepSeek-Prover-V2-671B демонстрирует выдающиеся результаты, достигая 88,9% на тесте MiniF2F и успешно решая множество задач из PutnamBench.

3. ProverBench: Формализация задач AIME и из учебников

ProverBench — это новый эталонный набор данных, содержащий 325 тщательно отобранных задач, которые представляют собой сочетание проблем из школьных олимпиад и университетских математических курсов. Из всего количества задач 15 формализованы на основе вопросов по теории чисел и алгебре, которые были представлены на последних соревнованиях AIME (AIME 24 и 25). Эти задачи призваны отразить уровень математической подготовки, ожидаемый на олимпиадах для старшеклассников, предоставляя возможность проверить навыки учащихся в условиях реальных соревнований. Остальные 310 задач составляют разнообразные учебные примеры, заимствованные из образовательных материалов и учебников, что обеспечивает большую педагогическую ценность и универсальность набора. ProverBench нацелен на более глубокую и всебічную оценку моделей, позволяя проверять как навыки решения задач на уровне школьных олимпиад, так и более сложные задачи, характерные для бакалавриата.

4. Загрузка моделей и наборов данных

DeepSeek-Prover-V2 представляется в двух вариантах, что позволяет исследователям и разработчикам выбрать модель, соответствующую их требованиям. Версия с 7 млрд параметров основана на более ранней модели DeepSeek-Prover-V1.5-Base, что обеспечивает ее стабильность и эффективность для решения задач формального доказательства. Она также обладает увеличенной длиной контекста до 32 тыс. токенов, что дает возможность обрабатывать более сложные запросы и обеспечивать лучшую детализацию решений.

Второй вариант, DeepSeek-Prover-V2-671B, основан на архитектуре DeepSeek-V3-Base и представляет собой более мощное решение для нейронного доказательства теорем, способное справляться с большими объемами данных и сложными математическими объектами. Это позволяет пользователям гибко подходить к выбору модели в зависимости от сложности задач, которые они планируют решать, и объема данных, с которыми работают.