DeepSeek lança novo modelo de IA Math‑V2 capaz de resolver e auto‐verificar teoremas complexos
DeepSeek‑Math‑V2 equipara-se aos modelos da OpenAI e Google DeepMind em desafios da Olimpíada Internacional de Matemática 2025
A startup chinesa DeepSeek apresentou, em 27 de novembro, um novo modelo de IA de código aberto, desenvolvido para gerar e auto‑verificar teoremas matemáticos utilizando habilidades avançadas de raciocínio, criadas especificamente para essa finalidade.
Denominado DeepSeek‑Math‑V2, este modelo de linguagem focado em raciocínio matemático possui notáveis capacidades de demonstração de teoremas. Seus pesos estão disponíveis para download sob a licença de código aberto Apache 2.0 em plataformas como Hugging Face e GitHub.
Construído sobre o modelo experimental DeepSeek‑V3.2‑Exp, lançado em setembro deste ano, o Math‑V2 concentra-se no raciocínio matemático auto‑verificável. Ele integra dois componentes fundamentais: um verificador que confere passo a passo as provas matemáticas e um gerador de teoremas capaz de corrigir seus próprios erros.
Conforme descrito em um artigo técnico publicado pela DeepSeek, “ao escalar o raciocínio com aprendizado por reforço que recompensa as respostas finais corretas, os modelos de linguagem melhoraram de uma performance medíocre para alcançar resultados saturados em competições quantitativas como AIME e HMMT em apenas um ano. Contudo, essa abordagem apresenta limitações fundamentais.” Para tarefas que exigem uma derivação rigorosa, como a demonstração de teoremas, o DeepSeek‑Math‑V2 foi desenvolvido para resolver problemas abertos sem soluções pré‑definidas, utilizando a auto‑verificação para ampliar a capacidade de raciocínio durante a execução.
Em termos de desempenho, a DeepSeek afirmou que o Math‑V2 alcançou pontuações dignas de medalha de ouro ao ser testado em problemas da Olimpíada Internacional de Matemática (IMO) 2025 e da Olimpíada de Matemática CREST (CMO) 2024, além de atingir uma elevada pontuação de 118 em 120 na competição matemática Putnam 2024.
Embora ainda haja muito a ser aprimorado, esses resultados indicam que o raciocínio matemático auto‑verificável é uma direção de pesquisa viável para o desenvolvimento de sistemas de IA mais robustos. O desempenho do Math‑V2 posiciona a DeepSeek entre gigantes como OpenAI e Google DeepMind, cujos modelos não divulgados apresentaram resultados semelhantes na renomada competição realizada este ano. Vale ressaltar que, embora este tenha sido o primeiro ano em que os organizadores da IMO permitiram a participação de modelos de IA, somente o Google integrou esse grupo inaugural, com a OpenAI e a DeepSeek permanecendo de fora.
Além de demonstrar a eficácia dos modelos de linguagem em gerar grandes volumes de texto, os avanços recentes em modelos de raciocínio matemático podem auxiliar pesquisadores a solucionar problemas antigos em áreas como criptografia e exploração espacial. O lançamento do Math‑V2 também representa um avanço significativo para o ecossistema de código aberto, dominado atualmente pela China. Um estudo recente do MIT, em parceria com a Hugging Face, revelou que a participação dos modelos abertos desenvolvidos na China aumentou para 17% no último ano, o que pode conferir ao país uma vantagem crucial no mercado global de IA.
