DeepSeek-Prover-V2: мост между неформальной и формальной математической логикой

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

Проблема формальной математической логики

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

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

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

Новый подход к доказательству теорем

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

Вместо того, чтобы пытаться решить всю проблему сразу, система разбивает ее на серию “подцелей” – промежуточных лемм, которые служат ступенями к окончательному доказательству. Этот подход повторяет то, как человеческие математики решают сложные проблемы, работая над управляемыми частями, а не пытаясь решить все сразу.

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

Расширение обучения для математической логики

После первоначального обучения на синтетических данных DeepSeek-Prover-V2 использует расширение обучения, чтобы еще больше повысить свои возможности. Модель получает обратную связь о том, правильны ли ее решения или нет, и использует эту обратную связь, чтобы узнать, какие подходы работают лучше всего.

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

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

Производительность DeepSeek-Prover-V2 на установленных бенчмарках демонстрирует его исключительные возможности. Модель достигает впечатляющих результатов на бенчмарке MiniF2F-test и успешно решает 49 из 658 проблем из PutnamBench – коллекции проблем из престижной математической олимпиады Уильяма Лоуэлла Путнэма.

Возможно, еще более впечатляюще то, что при оценке на 15 выбранных проблемах из недавних математических олимпиад США (AIME) модель успешно решила 6 проблем. Также интересно отметить, что по сравнению с DeepSeek-Prover-V2, DeepSeek-V3 решил 8 из этих проблем, используя голосование большинства. Это говорит о том, что разрыв между формальной и неформальной математической логикой быстро сокращается в LLM. Однако производительность модели на комбинаторных проблемах все еще требует улучшения, подчеркивая область, где будущие исследования могли бы сосредоточиться.

ProverBench: новый бенчмарк для ИИ в математике

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

Открытый доступ и будущие последствия

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

Последствия для ИИ и математических исследований

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

Исследователи стремятся масштабировать модель, чтобы решать еще более сложные проблемы, такие как те, что представлены на Международной математической олимпиаде (IMO). Это может еще больше продвинуть возможности ИИ в области доказательства математических теорем. По мере того, как модели, подобные DeepSeek-Prover-V2, продолжают развиваться, они могут переопределить будущее как математики, так и ИИ, стимулируя достижения в областях, от теоретических исследований до практических применений в технологиях.

Итог

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