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

Задача формального математического рассуждения в ИИ

Формальное математическое рассуждение требует строгой логической последовательности, где каждый шаг доказательства должен быть точным, полностью описанным и проверяемым вычислительными системами. В отличие от неформального решения задач, допускающего интуицию и эвристики, формальное доказательство строится в рамках таких систем, как Lean, Coq и Isabelle, которые обеспечивают отсутствие пропусков и двусмысленностей. Это создаёт серьёзную сложность для моделей ИИ, особенно для больших языковых моделей, которые хорошо формируют связный текст, но обычно не способны создавать формально проверяемые доказательства.

Преодоление разрыва между неформальным и формальным рассуждением

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

Существующие подходы и их ограничения

Некоторые методы предлагают сначала создавать наброски доказательств на естественном языке, которые затем вручную или полуавтоматически переводятся в формальные доказательства, часто разбивая сложные теоремы на подцели — леммы. Такие подходы, как «Draft, Sketch, and Prove», используют языковые модели для создания контуров доказательств, которые затем формализуются. Иерархическое обучение с подкреплением применяется для разбиения задач на уровни. Однако эти методы часто не дают полностью проверяемых формальных доказательств в Lean или Coq из-за ограниченного объёма обучающих данных и слабых сигналов обучения при неудачных попытках.

Представляем DeepSeek-Prover-V2

Исследователи DeepSeek-AI разработали DeepSeek-Prover-V2, модель, которая генерирует формальные доказательства, используя разложение по подцелям и обучение с подкреплением. Процесс начинается с DeepSeek-V3, который разбивает сложную теорему на подцели, каждая из которых оформляется в виде оператора «have» в Lean 4 с заполнителем для незавершённого доказательства. Затем 7-миллиардная модель prover пытается завершить каждую подцель. После решения всех подцелей система синтезирует полное формальное доказательство и сопоставляет его с исходным естественным языком, создавая богатый синтетический датасет для обучения без использования аннотированных человеком доказательств.

Технические инновации

Cold-start pipeline: DeepSeek-V3 генерирует наброски доказательств на естественном языке, которые превращаются в формальные теоремы с незавершёнными частями.
Рекурсивное решение подцелей: 7B-модель prover рекурсивно решает подцели, снижая вычислительные затраты при сохранении формальной строгости.
Обучение с учебной программой: задачи усложняются постепенно, используя два типа подцелей — с зависимыми и независимыми предпосылками.
Награда на основе согласованности: обучение с подкреплением улучшает точность, обеспечивая соответствие между наброском и решением.

Результаты

Достигнута точность 88.9% на бенчмарке MiniF2F-test (Pass@8192), превзойдя Kimina-Prover (82.0%) и Geodel-Prover (64.7%).
Решено 49 из 658 сложных задач PutnamBench.
Решено 6 из 15 задач AIME 2024–2025 на новом датасете ProverBench из 325 формализованных задач.
Модель демонстрирует высокую обобщаемость и формальную проверяемость, сравнимую с DeepSeek-V3.

Основные выводы

DeepSeek-Prover-V2 объединяет создание набросков доказательств на естественном языке с формальным построением доказательств. Обучение с подкреплением по учебной программе и использование синтетических данных позволяют масштабировать разработку формально проверяемых ИИ-доказательств. Это важный шаг к интеграции языковой интуиции ИИ с требованиями формальной верификации.

Подробности в исследовательской статье и на GitHub. Следите за DeepSeek-AI в Twitter, Telegram и LinkedIn.