A empresa chinesa de inteligência artificial DeepSeek revelou seu mais recente modelo de linguagem de grande porte (LLM) de código aberto, o Prover V2, projetado para aprimorar o raciocínio matemático formal. Lançado em 30 de abril de 2025 e hospedado no Hugging Face sob a licença permissiva do MIT, o Prover V2 representa um avanço significativo na demonstração de teoremas orientada por IA.
O Prover V2 possui impressionantes 671 bilhões de parâmetros, tornando-o um dos maiores modelos do gênero. Baseado em seus antecessores, Prover V1 e V1.5, lançados em agosto de 2024, o Prover V2 é treinado para traduzir problemas matemáticos complexos em lógica formal usando a linguagem de programação Lean 4. Essa capacidade permite que o modelo gere e verifique provas matemáticas, servindo potencialmente como uma ferramenta valiosa tanto em ambientes educacionais quanto de pesquisa.
O desenvolvimento do Prover V2 envolveu uma abordagem inovadora, na qual o modelo foi treinado usando um pipeline recursivo de prova de teoremas alimentado pelo DeepSeek-V3. Esse método permitiu que o modelo decompusesse problemas complexos em subobjetivos, sintetizasse provas para esses subobjetivos e os integrasse em um processo coerente de cadeia de pensamento.
Como resultado, o Prover V2 alcançou um desempenho de ponta na prova de teoremas neurais, atingindo uma taxa de aprovação de 88,9% no teste MiniF2F e resolvendo 49 dos 658 problemas do PutnamBench.
Apesar de seu tamanho enorme, o Prover V2 foi otimizado para acessibilidade. Os pesos do modelo foram quantizados para uma precisão de ponto flutuante de 8 bits, reduzindo efetivamente os requisitos de armazenamento e tornando-o viável para execução em hardware de consumo de ponta. O modelo pesa aproximadamente 650 gigabytes e pode ser executado a partir de RAM ou VRAM, dependendo da capacidade do sistema.
Quantização e destilação de modelos são técnicas-chave empregadas para aumentar a eficiência do modelo. A quantização reduz a precisão numérica dos pesos e ativações de um modelo, reduzindo seu tamanho e aumentando a velocidade de inferência com perda mínima de precisão. A destilação de modelos envolve o treinamento de uma rede compacta de “alunos” para replicar o comportamento de um modelo maior de “professor”, mantendo a maior parte do desempenho e reduzindo o número de parâmetros. Essas técnicas permitiram que a DeepSeek tornasse modelos de IA poderosos mais acessíveis a um público mais amplo.
O compromisso da empresa com o desenvolvimento de código aberto a diferencia na indústria de IA. Ao lançar o Prover V2 sob a licença do MIT, a empresa permite que pesquisadores e desenvolvedores em todo o mundo acessem, modifiquem e desenvolvam seu trabalho. Essa abordagem promove a colaboração e acelera a inovação na área de IA.
O modelo anterior da empresa, o DeepSeek R1, também atraiu atenção significativa por sua natureza de código aberto e desenvolvimento econômico. Treinado com um orçamento de apenas US$5,6 milhões, o R1 demonstrou que modelos de IA de alto desempenho poderiam ser desenvolvidos sem os extensos recursos normalmente exigidos por gigantes do setor. Essa conquista foi comparada a um “momento Sputnik” para a IA, sinalizando uma mudança no cenário global da IA.
O lançamento do Prover V2 destaca a crescente capacidade da China no desenvolvimento de IA, particularmente diante das restrições de exportação dos EUA para semicondutores avançados. O sucesso da DeepSeek demonstra que técnicas inovadoras de otimização de software podem superar as limitações de hardware, desafiando a noção de que o desenvolvimento de IA de ponta é exclusivo para empresas com acesso aos chips mais avançados.
Além disso, os avanços da DeepSeek têm suscitado discussões sobre a democratização da IA. Ao disponibilizar modelos poderosos como o Prover V2, a empresa capacita uma gama mais ampla de pesquisadores e desenvolvedores a contribuir para a área, potencialmente acelerando o progresso e promovendo um ecossistema de IA mais inclusivo.
O Prover V2 da DeepSeek representa um marco significativo no desenvolvimento da IA. Seus recursos impressionantes, combinados com a filosofia de código aberto da empresa, destacam o potencial de abordagens inovadoras para remodelar o cenário da IA.
