Lançamento do DeepSeekMath-V2 - Rumo ao raciocínio matemático auto-verificável

• Com o objetivo de melhorar a capacidade de raciocínio matemático de grandes modelos de linguagem, foi desenvolvido um modelo que fortalece a verificabilidade do processo de raciocínio além da simples precisão da resposta correta
• Melhorando a limitação de abordagens anteriores baseadas em aprendizado por reforço focadas na recompensa da resposta final, foi introduzido um mecanismo de auto-verificação (self-verification)
• Em problemas que exigem raciocínio lógico passo a passo, como theorem proving (prova de teoremas), o modelo gerador foi projetado para encontrar e corrigir seus próprios erros
• Utiliza-se o verificador (verifier) como modelo de recompensa e, ao escalar o cálculo de verificação, rotulam-se automaticamente dados de prova difíceis para obter melhoria contínua de desempenho
• O modelo registrou pontuações de ponta em IMO 2025, CMO 2024, Putnam 2024, comprovando a viabilidade da IA matemática auto-verificável

---

1. Introdução (Introduction)

• Os grandes modelos de linguagem (LLM) fizeram grande progresso em raciocínio matemático e desempenham um papel central como benchmark de pesquisa em IA
  • Com aprendizado por reforço por recompensa baseada em resposta correta, alcançou-se desempenho de ponta em competições como AIME, HMMT em apenas um ano
• No entanto, há limitações em focar apenas em elevar a precisão da resposta final
  • Mesmo com resposta correta, a validade do processo de raciocínio não é garantida, e é inviável para problemas que exigem desenvolvimento lógico em etapas, como prova de teoremas
• Para resolver isso, foi introduzido o conceito de auto-verificação (self-verification), desenhado para avaliar a abrangência e a rigorosidade do raciocínio
  • Especialmente em testes de problemas de resposta desconhecida (open problems), foi apresentado como componente essencial para expandir os cálculos
• A equipe treinou um verificador (verifier) confiável e preciso baseado em LLM e o utilizou como modelo de recompensa para treinar o gerador de provas (generator)
  • Incentivando o gerador a identificar e corrigir erros por conta própria dentro das provas
• Conforme o desempenho do gerador melhora, a dificuldade da verificação também aumenta; assim, escalou-se o cálculo de verificação (scale verification compute) para rotular automaticamente novas provas difíceis
  • Isso melhora continuamente o desempenho do verificador
• O modelo resultante, DeepSeekMath-V2, alcançou desempenho de nível de medalha de ouro em IMO 2025 e CMO 2024, e 118/120 pontos em Putnam 2024
  • Esses resultados mostram que raciocínio matemático auto-verificável é uma direção de pesquisa viável

2. Resultados de avaliação (Evaluation Results)

• A avaliação utilizou IMO-ProofBench desenvolvido pela equipe DeepThink IMO-Gold da DeepMind, além de concursos matemáticos recentes (IMO 2025, CMO 2024, Putnam 2024)
  • Valores numéricos específicos e detalhes dos resultados não são fornecidos no texto

3. Arquitetura do modelo (Model Architecture)

• DeepSeekMath-V2 foi construído com base no modelo DeepSeek-V3.2-Exp-Base
  • O suporte relacionado à inferência (inference) está no repositório GitHub DeepSeek-V3.2-Exp

4. Licença (License)

• O modelo e os pesos são distribuídos sob a Apache License 2.0

5. Citação (Citation)

• Os nomes dos autores e as informações do paper estão informados, com o título
  “DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning” (2025)

6. Informações adicionais

• O número de downloads no último mês foi de 4,434
• Ao montar a árvore do modelo, o modelo-base forma um loop de autorreferência e aparece marcado como impossível de gerar árvore

[GN⁺]

Comentários no Hacker News

• O modelo lançado desta vez abriu os pesos como open source sob a licença Apache 2.0
  Os modelos medalhistas de ouro da IMO da OpenAI e da DeepMind continuam fechados

  • Assim como as empresas de IA lidam com os direitos autorais dos dados de treinamento, acho que também deveríamos tratar dessa forma os direitos autorais dos pesos
  • Mas, se só os pesos forem divulgados e o código de treinamento ou os dados não forem abertos, ele ainda continua sendo um modelo fechado

• A discussão anterior está neste link

  • Eu tinha perdido esse link, obrigado por compartilhar

• É impressionante como os modelos de pesos abertos estão alcançando rapidamente áreas especializadas como matemática e raciocínio
  Fico curioso se alguém também testou avaliações relacionadas a lógica complexa ou programação. Modelos bons em matemática muitas vezes também são fortes em debugging ou geração de algoritmos

  • Modelos especializados em domínios específicos têm menor valor comercial, e o treinamento de LLMs em larga escala prefere a generalidade, então isso é algo natural
  • O kimi-k2 é bem decente para programação, mas não chega ao nível dos modelos SOTA da Anthropic, OpenAI ou Google

• Acho que também é preciso ter uma visão cética sobre os resultados desse modelo
  Foi declarado que ele treinou diretamente com problemas coletados da internet, mas não houve menção à remoção de contaminação de benchmark nem à exclusão de problemas de 2024/2025
  OpenAI e Google testaram modelos experimentais sem acesso prévio aos problemas de 2025

• Fico me perguntando por que o modelo medalhista de ouro da OpenAI ainda não foi divulgado

  • Aquilo foi simplesmente publicidade. A ideia é incorporar as lições aprendidas ali no próximo modelo de uso geral

• É importante notar que este não é um modelo de uso geral. Os modelos do Google e da OpenAI usaram modelos de uso geral

  • Na prática, tanto a OpenAI quanto o Google usaram modelos de pesquisa especializados para a IMO
    • A OpenAI, neste tweet, antecipou o lançamento do GPT-5 e afirmou que o modelo da IMO é experimental e não há plano de divulgá-lo tão cedo
    • A DeepMind explicou em seu blog oficial que treinou o Gemini com raciocínio em múltiplas etapas baseado em aprendizado por reforço e dados de prova de teoremas
  • O post oficial da DeepSeek também foi compartilhado

• Fico curioso sobre como rodar um modelo desses em casa
  A dúvida é se seria possível em CPU com algo como 1 TB de RAM

  • Só os dados para download têm 690 GB, então parece que seria preciso 1 TB de RAM. Nem com minhas duas máquinas Strix Halo isso dá
  • Com ik_llama.cpp, RAM suficiente e uma GPU, dá para rodar, ainda que lentamente. O llama.cpp normal também funciona, mas o fork ik é mais eficiente
  • Disseram que também daria com dois Mac Studio de 512 GB ligados por Thunderbolt 5

• Há suspeita de que esse modelo talvez tenha sido destilado (distill) diretamente a partir das saídas da OpenAI ou do Google

• Fico curioso se há planos de colocar esse modelo no OpenRouter

• Será que, se a OpenAI colocar anúncios no ChatGPT, as pessoas não migrariam imediatamente para outros modelos?

  • Acho que o ideal seria vários provedores oferecerem modelos de uso geral competindo a preço de mercado
  • Com ou sem anúncios, eu não confio na OpenAI. Antes de mudar o nome para CloseAI, fica difícil confiar
  • O ChatGPT é só um site. Não é estranho um site ter anúncios. O Instagram é igual
  • Eles já têm uma estrutura de receita por meio de datacenters de GPU e APIs. Mesmo com concorrência, devem continuar sendo a primeira opção por algum tempo
  • O Google também exibiu anúncios por décadas, e ninguém migrou para outro buscador