DeepSeekMath-V2: Rumo ao Raciocínio Matemático Auto-Verificável
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
November 27, 2025
Autores: Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang
cs.AI
Resumo
Os grandes modelos de linguagem têm feito progressos significativos no raciocínio matemático, que serve como um importante campo de teste para a IA e poderia impactar a pesquisa científica se avançado ainda mais. Ao escalar o raciocínio com aprendizado por reforço que recompensa respostas finais corretas, os LLMs evoluíram de um desempenho fraco para saturar competições de raciocínio quantitativo como AIME e HMMT em um ano. No entanto, essa abordagem enfrenta limitações fundamentais. Buscar maior precisão na resposta final não resolve um problema-chave: respostas corretas não garantem um raciocínio correto. Além disso, muitas tarefas matemáticas, como a prova de teoremas, exigem derivação rigorosa passo a passo em vez de respostas numéricas, tornando as recompensas por resposta final inaplicáveis. Para ampliar os limites do raciocínio profundo, acreditamos ser necessário verificar a abrangência e o rigor do raciocínio matemático. A autoverificação é particularmente importante para escalar o cálculo em tempo de teste, especialmente para problemas em aberto sem soluções conhecidas. Rumo a um raciocínio matemático autoverificável, investigamos como treinar um verificador preciso e fiel baseado em LLM para prova de teoremas. Em seguida, treinamos um gerador de provas usando o verificador como modelo de recompensa, incentivando o gerador a identificar e resolver tantos problemas quanto possível em suas próprias provas antes de finalizá-las. Para manter a lacuna geração-verificação à medida que o gerador se torna mais forte, propomos escalar o cálculo de verificação para rotular automaticamente novas provas difíceis de verificar, criando dados de treinamento para melhorar ainda mais o verificador. Nosso modelo resultante, DeepSeekMath-V2, demonstra fortes capacidades de prova de teoremas, alcançando pontuações de nível ouro na IMO 2025 e CMO 2024 e um quase perfeito 118/120 na Putnam 2024 com cálculo escalonado em tempo de teste.
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.