O laboratório chinês de inteligência artificial (IA) DeepSeek acaba de lançar o Prover-V2, um modelo especializado de código aberto que combina raciocínio matemático informal com prova formal de teoremas – alcançando desempenho SOTA (state-of-the-art) em benchmarks de matemática complexa.
PUBLICIDADE
Detalhes do Prover-V2
- O modelo de 671 bilhões de parâmetros alcança uma taxa de sucesso de 88,9% no benchmark de teste MiniF2F, estabelecendo novos patamares para a prova automatizada de teoremas.
- O sistema utiliza uma abordagem de “cold-start” (partida fria) que decompõe provas complexas em sub-objetivos menores usando o modelo V3 da DeepSeek antes da verificação formal.
- A equipe também introduziu o ProverBench, um novo conjunto de dados de avaliação com 325 problemas, incluindo questões da competição AIME e matemática de nível de graduação.
- O lançamento discreto de código aberto ocorre pouco depois do Qwen3 da Alibaba e antes do altamente aguardado DeepSeek-R2, esperado para o início de maio.
Por que isso é importante
Embora não seja o R2, a DeepSeek continua a demonstrar discretamente suas habilidades com mais um lançamento de modelo robusto. Não demorará muito para que esses modelos resolvam problemas antes considerados impossíveis – levando a capacidades matemáticas sobre-humanas que trarão novos avanços em áreas como física, descoberta de medicamentos e ciência dos materiais.
Leia também:
