DeepSeekMath-V2: На пути к самопроверяемому математическому рассуждению
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
November 27, 2025
Авторы: Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang
cs.AI
Аннотация
Крупные языковые модели достигли значительного прогресса в математических рассуждениях, которые служат важным полигоном для испытаний ИИ и в случае дальнейшего развития могут оказать влияние на научные исследования. Благодаря масштабированию рассуждений с помощью обучения с подкреплением, поощряющего правильные итоговые ответы, языковые модели всего за год эволюционировали от низких результатов до насыщения количественных соревнований по reasoning, таких как AIME и HMMT. Однако у этого подхода есть фундаментальные ограничения. Стремление к повышению точности итогового ответа не решает ключевую проблему: правильный ответ не гарантирует корректности рассуждений. Более того, многие математические задачи (например, доказательство теорем) требуют строгого пошагового вывода, а не численных ответов, что делает неприменимым вознаграждение за конечный результат. Чтобы раздвинуть границы глубинных рассуждений, мы считаем необходимым проверять полноту и строгость математических выводов. Самопроверка особенно важна для масштабирования вычислительных ресурсов на этапе тестирования, особенно для открытых проблем без известных решений. В направлении самопроверяемых математических рассуждений мы исследуем, как обучить точный и достоверный верификатор на основе языковой модели для доказательства теорем. Затем мы обучаем генератор доказательств, используя верификатор в качестве модели вознаграждения, и стимулируем генератор выявлять и устранять как можно больше проблем в собственных доказательствах перед их финализацией. Чтобы сохранять разрыв между генерацией и проверкой по мере усиления генератора, мы предлагаем масштабировать вычислительные ресурсы верификации для автоматической разметки новых сложных для проверки доказательств, создавая обучающие данные для дальнейшего улучшения верификатора. Наша итоговая модель DeepSeekMath-V2 демонстрирует мощные возможности в доказательстве теорем, достигая золотого уровня на Международной математической олимпиаде 2025 года и Канадской математической олимпиаде 2024 года, а также почти идеального результата 118/120 на конкурсе Путнэма 2024 года при масштабировании тестовых вычислений.
English
Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn't address a key issue: correct answers don't guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute.