A DeepSeek, uma empresa chinesa focada em inteligência artificial, lançou discretamente o DeepSeek-Prover V2, um modelo de linguagem open-source que combina raciocínio matemático informal com a prova formal de teoremas, alcançando resultados notáveis em benchmarks de matemática de alto nível.
O modelo, com 671 bilhões de parâmetros, resolveu 88,9% dos problemas do benchmark MiniF2F, 49% dos problemas do PutnamBench e obteve um desempenho significativo no ProverBench-AIME 24 e 25, com 8 problemas resolvidos de um total de 15. Esses números posicionam o DeepSeek-Prover V2 como um marco no campo da prova de teoremas automatizada, superando modelos anteriores e concorrentes.
Como funciona o DeepSeek-Prover V2
O DeepSeek-Prover V2 utiliza uma abordagem inovadora chamada “cold-start”, que começa com o modelo DeepSeek-V3 decompondo problemas complexos em subobjetivos. Esses subobjetivos são então resolvidos e sintetizados em um processo de raciocínio em cadeia, criando uma base para aprendizado por reforço. Segundo informações do GitHub da IA, o modelo foi treinado com supervisão binária de recompensa (certo ou errado), o que otimizou sua capacidade de resolver problemas matemáticos desafiadores.
No MiniF2F, um benchmark de nível olímpico, o DeepSeek-Prover V2-671B alcançou uma taxa de sucesso de 88,9%. Assim superando versões menores do mesmo modelo (82% para o 7B) e outros concorrentes como Kinima-Prover-72B (80,7%) e BFS-Prover-7B (73%).
No PutnamBench, voltado para competições universitárias, o modelo resolveu 49 problemas, contra 23 do DeepSeek-Prover V2-7B. Enquanto no ProverBench-AIME 24 e 25, voltado para provas formais de nível escolar avançado, ele resolveu 8 problemas, contra 6 de sua versão informal, DeepSeek-V3-0324.
A relevância do DeepSeek-Prover V2 vai além dos números impressionantes. Como destacado por Zhihong Shao no X, o modelo é open-source e está disponível no GitHub. Assim, permitindo que pesquisadores e desenvolvedores de todo o mundo o utilizem e contribuam para seu desenvolvimento.
Apesar de seu sucesso, o novo modelo ainda enfrenta desafios em problemas mais complexos. Mas sua abordagem inovadora e desempenho já o colocam como uma referência no avanço da IA para matemática.
