A empresa chinesa de desenvolvimento de inteligência artificial DeepSeek lançou um novo modelo de linguagem de grande porte (LLM) com pesos abertos.
A DeepSeek enviou seu modelo mais recente, o Prover V2, para a plataforma de hospedagem Hugging Face em 30 de abril. O modelo, lançado sob a licença permissiva de código aberto MIT, tem como objetivo lidar com a verificação de provas matemáticas.
O Prover V2 possui 671 bilhões de parâmetros, sendo significativamente maior do que seus predecessores, o Prover V1 e o Prover V1.5, lançados em agosto de 2024. O artigo que acompanhava a primeira versão explicava que o modelo foi treinado para traduzir problemas de competições matemáticas em lógica formal usando a linguagem de programação Lean 4 — uma ferramenta amplamente utilizada na demonstração de teoremas.
Os desenvolvedores afirmam que o Prover V2 comprime o conhecimento matemático em um formato que permite gerar e verificar provas, com potencial para auxiliar pesquisas e a educação.
O que tudo isso significa?
Um modelo — frequentemente chamado de forma informal e incorreta de "pesos" no universo da IA — é o arquivo (ou conjunto de arquivos) que permite executar localmente uma inteligência artificial sem depender de servidores externos. Ainda assim, é importante destacar que os LLMs mais avançados exigem hardware que a maioria das pessoas não possui.
Isso porque esses modelos costumam ter um número muito alto de parâmetros, resultando em arquivos grandes que demandam muita RAM ou VRAM (memória da GPU) e poder de processamento para funcionar. O novo modelo Prover V2 pesa aproximadamente 650 gigabytes e espera-se que seja executado diretamente da RAM ou da VRAM.
Para atingir esse tamanho, os pesos do Prover V2 foram quantizados para precisão de ponto flutuante de 8 bits, o que significa que cada parâmetro foi aproximado para ocupar metade do espaço usual de 16 bits (sendo 1 bit uma unidade binária). Isso reduz efetivamente o tamanho total do modelo pela metade.
O Prover V1 foi baseado no modelo DeepSeekMath, de sete bilhões de parâmetros, e ajustado com dados sintéticos. Dados sintéticos são aqueles usados no treinamento de modelos de IA e que também foram gerados por outros modelos de IA, sendo os dados humanos cada vez mais vistos como uma fonte escassa, porém de maior qualidade.
O Prover V1.5 teria apresentado melhorias em relação à versão anterior ao otimizar tanto o treinamento quanto a execução, além de alcançar maior precisão em testes comparativos. Até o momento, as melhorias introduzidas pelo Prover V2 ainda não estão claras, já que nenhum artigo técnico ou outra informação foi publicada até a data desta redação.
A quantidade de parâmetros do Prover V2 sugere que ele possivelmente é baseado no modelo R1 anterior da empresa. Quando foi lançado, o R1 chamou a atenção no setor de IA por apresentar desempenho comparável ao modelo o1 da OpenAI, então considerado o mais avançado.
A importância dos pesos abertos
Divulgar publicamente os pesos de LLMs é um tema controverso. De um lado, é uma força democratizadora, permitindo que o público acesse a IA por conta própria, sem depender da infraestrutura de empresas privadas.
Por outro lado, isso impede que a empresa intervenha para evitar abusos do modelo, já que não pode impor limitações a comandos potencialmente perigosos. O lançamento do R1 nesses termos gerou preocupações de segurança, sendo descrito por alguns como o “momento Sputnik” da China.
Defensores do código aberto celebraram o fato de que a DeepSeek deu continuidade ao trabalho que a Meta iniciou com o lançamento da série LLaMA de modelos de IA open-source, provando que IAs abertas são concorrentes reais para modelos fechados como os da OpenAI. A acessibilidade desses modelos continua a melhorar.
Modelos de linguagem acessíveis
Hoje, mesmo usuários que não possuem um supercomputador — que pode custar mais do que a média das casas em muitos países — já conseguem rodar LLMs localmente. Isso é possível principalmente por duas técnicas de desenvolvimento de IA: destilação de modelos e quantização.
A distilação consiste em treinar uma rede neural “aluna”, mais compacta, para replicar o comportamento de um modelo “professor” maior, preservando boa parte do desempenho ao mesmo tempo que reduz os parâmetros para torná-lo viável em hardware mais modesto. A quantização, por sua vez, reduz a precisão numérica dos pesos e ativações do modelo, diminuindo seu tamanho e acelerando a inferência com perdas mínimas de precisão.
Um exemplo disso é a redução do Prover V2 de números em ponto flutuante de 16 para 8 bits, mas reduções ainda maiores também são possíveis. Ambas as técnicas afetam o desempenho do modelo, mas geralmente mantêm sua funcionalidade.
O R1 da DeepSeek foi destilado em versões ajustadas com os modelos LLaMA e Qwen, variando de 70 bilhões a apenas 1,5 bilhão de parâmetros. Os modelos menores dessa linha já podem ser executados de forma confiável até mesmo em alguns dispositivos móveis.