Андрей Щербаков 
Новая эра в области искусственного интеллекта для математических исследований наступает с появлением DeepSeek-Prover-V2, модели ИИ с открытым исходным кодом, разработанной специалистами DeepSeek-AI. Эта система способна преобразовывать интуитивные математические идеи в строгие, проверяемые доказательства, решая одну из сложнейших задач для ИИ – формальное математическое мышление. Создание проверяемого математического доказательства требует не только глубокого концептуального понимания, но и способности выстраивать точные, пошаговые логические аргументы, что до недавнего времени оставалось серьезным препятствием для машин.
Математики в своей работе часто опираются на интуицию, эвристики и рассуждения высокого уровня, что позволяет им пропускать очевидные шаги или использовать приближения. Однако формальное доказательство теорем требует абсолютной точности: каждый шаг должен быть четко сформулирован и логически обоснован без какой-либо двусмысленности. Современные большие языковые модели (LLM) демонстрируют способность решать сложные математические задачи олимпиадного уровня, используя рассуждения на естественном языке. Тем не менее, преобразование таких интуитивных рассуждений в формальные доказательства, которые могут быть верифицированы машиной, остается для них проблемой, поскольку неформальные методы часто содержат сокращения и пропущенные шаги, неприемлемые для формальных систем. DeepSeek-Prover-V2 решает эту проблему, объединяя сильные стороны неформального и формального мышления, разбивая сложные задачи на более мелкие, управляемые части, сохраняя при этом точность, необходимую для формальной проверки. Это позволяет эффективно преодолеть разрыв между человеческой интуицией и машинно-проверяемыми доказательствами.
В основе DeepSeek-Prover-V2 лежит уникальный конвейер обработки данных, включающий как неформальное, так и формальное мышление. Процесс начинается с общей LLM, DeepSeek-V3, которая анализирует математические задачи на естественном языке, разбивает их на более мелкие шаги и переводит эти шаги на формальный язык, понятный машинам. Вместо того чтобы пытаться решить всю проблему сразу, система декомпозирует ее на ряд «подцелей» – промежуточных лемм, служащих ступеньками на пути к окончательному доказательству. Такой подход имитирует то, как математики-люди справляются со сложными задачами, прорабатывая их посильными частями. Особую новизну этому подходу придает способ синтеза обучающих данных: когда все подцели сложной проблемы успешно решены, система объединяет эти решения в полное формальное доказательство. Затем это доказательство сопоставляется с исходной цепочкой рассуждений DeepSeek-V3 для создания высококачественных данных для «холодного старта» обучения модели.
После первоначального обучения на синтетических данных DeepSeek-Prover-V2 использует обучение с подкреплением для дальнейшего совершенствования своих возможностей. Модель получает обратную связь о корректности своих решений и использует эту информацию, чтобы научиться выбирать наиболее эффективные подходы. Одной из проблем на этом этапе было то, что структура генерируемых доказательств не всегда совпадала с декомпозицией на леммы, предложенной цепочкой рассуждений. Для устранения этого несоответствия исследователи ввели на этапах обучения «вознаграждение за согласованность», чтобы уменьшить структурные расхождения и обеспечить включение всех декомпозированных лемм в окончательные доказательства. Такой подход к выравниванию оказался особенно эффективным для сложных теорем, требующих многоэтапных рассуждений.
Производительность DeepSeek-Prover-V2 на признанных эталонных тестах демонстрирует ее исключительные возможности. Модель достигает впечатляющих результатов на наборе тестов MiniF2F-test и успешно решает 49 из 658 задач из PutnamBench – сборника задач престижного математического конкурса Уильяма Лоуэлла Патнэма. Еще более показательно, что при оценке на 15 избранных задачах из недавних соревнований American Invitational Mathematics Examination (AIME) модель успешно решила 6 из них. Интересно отметить, что для сравнения, DeepSeek-V3, используя метод «голосования большинством» (majority voting), решила 8 из этих же задач AIME. Это говорит о том, что разрыв между формальным и неформальным математическим мышлением в LLM стремительно сокращается. Тем не менее, производительность модели при решении комбинаторных задач все еще требует улучшения, указывая на область для будущих исследований.
Исследователи DeepSeek также представили новый эталонный набор данных для оценки возможностей LLM в решении математических задач, названный ProverBench. Этот набор состоит из 325 формализованных математических проблем, включая 15 задач из недавних соревнований AIME, а также задачи из учебников и образовательных пособий. Эти задачи охватывают такие области, как теория чисел, алгебра, математический анализ, действительный анализ и другие. Включение задач AIME особенно важно, поскольку оно позволяет оценить модель на задачах, требующих не только воспроизведения знаний, но и творческого подхода к решению.
Благодаря открытому исходному коду DeepSeek-Prover-V2 открывает захватывающие возможности. Модель размещена на таких платформах, как Hugging Face, и доступна широкому кругу пользователей, включая исследователей, преподавателей и разработчиков. Исследователи DeepSeek предлагают как более легкую версию с 7 миллиардами параметров, так и мощную версию с 671 миллиардом параметров, обеспечивая возможность использования модели пользователями с различными вычислительными ресурсами. Такой открытый доступ поощряет эксперименты и позволяет разработчикам создавать передовые инструменты ИИ для решения математических задач. В результате эта модель способна стимулировать инновации в математических исследованиях, помогая ученым решать сложные проблемы и открывать новые горизонты в этой области.
Разработка DeepSeek-Prover-V2 имеет значительные последствия не только для математических исследований, но и для развития ИИ в целом. Способность модели генерировать формальные доказательства может помочь математикам в решении сложных теорем, автоматизации процессов верификации и даже в выдвижении новых гипотез. Более того, методы, использованные при создании DeepSeek-Prover-V2, могут повлиять на разработку будущих моделей ИИ в других областях, требующих строгих логических рассуждений, таких как разработка программного и аппаратного обеспечения. Разработчики стремятся масштабировать модель для решения еще более сложных задач, например, уровня Международной математической олимпиады (IMO), что может еще больше расширить возможности ИИ в доказательстве математических теорем. По мере развития таких моделей, как DeepSeek-Prover-V2, они могут переопределить будущее как математики, так и искусственного интеллекта, стимулируя прогресс в областях от теоретических исследований до практических технологических приложений.
DeepSeek-Prover-V2 представляет собой значительный прорыв в области математического мышления, управляемого искусственным интеллектом. Модель сочетает неформальную интуицию с формальной логикой для декомпозиции сложных проблем и генерации проверяемых доказательств. Ее впечатляющая производительность на эталонных тестах демонстрирует потенциал для поддержки математиков, автоматизации проверки доказательств и даже стимулирования новых открытий в этой области. Будучи моделью с открытым исходным кодом, она широко доступна, открывая захватывающие перспективы для инноваций и новых приложений как в сфере ИИ, так и в математике.
