Команда DeepSeek AI представила DeepSeek-Prover-V2 — открытую модель, предназначенную для формального доказательства теорем в среде Lean 4. Пока классические LLM ограничиваются вероятностным угадыванием следующего токена, эта итерация переводит работу в плоскость строгой верификации. Архитектура DeepSeek-Prover-V2 отказывается от интуитивных «чатовых» ответов в пользу рекурсивного пайплайна (RPS). Сложные задачи здесь не просто решаются, а декомпозируются на подцели, каждую из которых проверяет компьютер. Для бизнеса, где цена ошибки измеряется миллионами, а потребность в точности абсолютна, это прямой сигнал: эра «черных ящиков» подходит к концу.
Синтез данных и рекурсивная архитектура
Главный барьер для специализированного ИИ — дефицит высококачественных данных в высшей математике и системном инжиниринге. В DeepSeek изящно обошли проблему «холодного старта», заставив модель DeepSeek-V3 генерировать обучающую выборку самостоятельно. Процесс выглядит так: «старшая» модель разбивает теоремы на цепочки формализованных шагов в Lean 4, а компактный 7B-проверщик отрабатывает поиск доказательства для каждой подзадачи. Этот рекурсивный цикл связывает логические рассуждения верхнего уровня с жестким, машиночитаемым кодом.
Такой подход позволяет модели учиться на синтетическом датасете, где человеческая математическая интуиция тесно переплетена с бескомпромиссными формальными доказательствами.
На базе этого синтеза команда применила обучение с подкреплением (RL), используя бинарный сигнал: «верно» или «ошибка». Особое внимание уделено граничным случаям: когда 7B-проверщик не осилил задачу целиком, но справился со всеми компонентами. Модель учится связывать удачные фрагменты в единую логическую цепь. Для СТО и владельцев бизнеса это означает переход к системам, которые не просто «предлагают» код, а доказывают его валидность через внешний компилятор еще до этапа развертывания.
Бенчмарки: когда паттернов недостаточно
Чтобы подтвердить жизнеспособность рекурсивной логики, разработчики представили DeepSeek-Prover-V2–671B. Цифры впечатляют: 88,9% прохождения теста MiniF2F и 49 решенных задач из 658 в PutnamBench. Модель начинает уверенно решать олимпиадные задачи университетского уровня — область, где обычные LLM традиционно пасуют из-за длинных цепочек рассуждений. Для чистоты эксперимента был запущен ProverBench — новый стандарт оценки, исключающий простую эксплуатацию заученных паттернов.
ProverBench выступает в роли «детектора лжи», охватывая разные области математики и проверяя именно глубину логического вывода. DeepSeek-Prover-V2 наглядно демонстрирует: путь к сильному ИИ лежит через интеграцию нейросетей с формальными логическими системами вроде Lean 4. Безусловно, вычислительная сложность рекурсивного поиска все еще остается «узким местом» из-за огромного пространства вариантов. Однако мы получили фундамент для автономных агентов, способных на самоаудит. И хотя это еще не универсальное решение для любой офисной задачи, в критически важных средах формальные доказательства уже начинают заменять нестабильный человеческий контроль.