DeepSeek-Prover-V2-671B Agora Disponível na Novita AI

A DeepSeek atualizou silenciosamente o Prover, seu modelo de IA projetado para resolver provas e teoremas matemáticos. O modelo DeepSeek-Prover-V2-671B já está disponível na plataforma de API de Modelos da Novita AI! Por tempo limitado, todos os novos usuários podem receber $10 em créditos grátis para explorar e construir com este modelo de prova automatizada de teoremas de última geração.

Aqui está o preço atual do DeepSeek-Prover-V2-671B na Novita AI:

DeepSeek-Prover-V2-671B: 0,7 $ / M tokens de entrada, 2,5 $ / M tokens de saída

Potencialize seus fluxos de trabalho matemáticos, pesquisas e ferramentas educacionais com um dos modelos de prova formal de teoremas mais avançados já lançados — agora a apenas uma chamada de API de distância.

O que é a Série de Modelos DeepSeek-Prover?

A série de modelos DeepSeek-Prover é uma família de ponta de grandes modelos de linguagem (LLMs) projetada para enfrentar o desafio da prova automatizada de teoremas em matemática. Desenvolvidos pela DeepSeek-AI, esses modelos são especificamente otimizados para gerar, verificar e raciocinar sobre provas matemáticas formais — especialmente dentro do ambiente do assistente de prova Lean 4.

Por que o DeepSeek-Prover foi Criado?

Embora LLMs modernos como o GPT-4 sejam impressionantes em raciocínio matemático, eles têm dificuldades com tarefas de prova formal devido à falta de dados de treinamento em larga escala e de alta qualidade em linguagens formais. O DeepSeek-Prover resolve isso gerando automaticamente milhões de provas sintéticas em Lean 4 a partir de problemas de competições de matemática e ajustando os modelos nesse conjunto de dados único.

Como Funciona o DeepSeek-Prover?

O pipeline do DeepSeek-Prover inclui:

• Autoformalização: Traduzir problemas matemáticos em linguagem natural para afirmações formais em Lean 4 usando um LLM.
• Filtragem de Qualidade: Filtrar afirmações quanto à correção lógica e interesse matemático por meio de pontuação do modelo e rejeição de hipóteses.
• Geração e Verificação de Provas: Tentar provar as afirmações filtradas e manter apenas aquelas com provas corretas e verificáveis.
• Treinamento Iterativo: Repetir esse processo, usando a cada vez os novos dados de prova de alta qualidade para melhorar ainda mais o modelo.

Por meio dessa abordagem, a série DeepSeek-Prover produz modelos que melhoram continuamente e são apoiados por uma das maiores coleções mundiais de provas matemáticas formais.

Destaques e Marcos dos Modelos Anteriores DeepSeek-Prover

• Escala: Mais de 8 milhões de afirmações formais em Lean 4 com provas foram geradas.
• Base Técnica: Baseado em grandes modelos transformer, como o DeepSeekMath 7B, pré-treinado em extensos dados matemáticos e posteriormente ajustado em provas sintéticas.
• Desempenho de Ponta: Alcança os melhores resultados em benchmarks de prova formal de teoremas (ex.: miniF2F, FIMO), superando GPT-4 e outros modelos especializados.

O que é o DeepSeek-Prover-V2-671B?

DeepSeek-Prover-V2-671B é um modelo carro-chefe da série DeepSeek-Prover. Aqui está o que o diferencia:

• Escala Massiva: Com cerca de 671 bilhões de parâmetros, este é um dos maiores modelos projetados para matemática formal e prova de teoremas.
• Precisão FP8: O DeepSeek-Prover-V2-671B é originalmente treinado e lançado em precisão FP8 (ponto flutuante de 8 bits), um formato moderno que permite computação eficiente e inferência de modelo mais rápida com menor uso de memória, mantendo alto desempenho.
• Capacidade Avançada: O modelo usa arquitetura transformer de última geração e suporta tipos de tensor modernos como BF16, FP8_E4M3 e F32, tornando-o adequado para ambientes de pesquisa e produção de alto desempenho.
• Projetado para Prova de Teoremas: Treinado em dados massivos e de alta qualidade de provas sintéticas, este modelo se destaca em raciocínio matemático complexo e geração de provas formais em Lean 4.

Como Acessar o DeepSeek-Prover-V2-671B na Novita AI

Começar com o DeepSeek-Prover-V2-671B é rápido, simples e sem riscos na Novita AI. Graças ao Programa de Indicação, você receberá $10 em créditos grátis — o suficiente para explorar completamente o poder do DeepSeek-Prover-V2-671B, construir protótipos e até lançar seu primeiro caso de uso sem nenhum custo inicial.

Use o Playground (Sem Necessidade de Codificação)

• Acesso Instantâneo: Cadastre-se, receba seus créditos grátis e comece a experimentar o DeepSeek-Prover-V2-671B e outros modelos de ponta em segundos.
• Interface Interativa: Teste prompts, raciocínio em cadeia de pensamento e visualize resultados em tempo real.
• Comparação de Modelos: Alterne facilmente entre DeepSeek-Prover-V2-671B, Llama 4, DeepSeek e mais para encontrar o ajuste perfeito para suas necessidades.

Integre via API (Para Desenvolvedores)

Conecte perfeitamente o DeepSeek-Prover-V2-671B a seus aplicativos, fluxos de trabalho ou chatbots com a API REST unificada da Novita AI — sem necessidade de gerenciar pesos de modelo ou infraestrutura. A Novita AI oferece SDKs em várias linguagens (Python, Node.js, cURL e mais) e controles avançados de parâmetros para usuários avançados.

Opção 1: Integração Direta com API (Exemplo em Python)

Para começar, basta usar o trecho de código abaixo:

from openai import OpenAI
  
client = OpenAI(
    base_url="https://api.novita.ai/v3/openai",
    api_key="<YOUR Novita AI API Key>",
)

model = "deepseek/deepseek-prover-v2-671b"
stream = True # or False
max_tokens = 2048
system_content = """Be a helpful assistant"""
temperature = 1
top_p = 1
min_p = 0
top_k = 50
presence_penalty = 0
frequency_penalty = 0
repetition_penalty = 1
response_format = { "type": "text" }

chat_completion_res = client.chat.completions.create(
    model=model,
    messages=[
        {
            "role": "system",
            "content": system_content,
        },
        {
            "role": "user",
            "content": "Hi there!",
        }
    ],
    stream=stream,
    max_tokens=max_tokens,
    temperature=temperature,
    top_p=top_p,
    presence_penalty=presence_penalty,
    frequency_penalty=frequency_penalty,
    response_format=response_format,
    extra_body={
      "top_k": top_k,
      "repetition_penalty": repetition_penalty,
      "min_p": min_p
    }
  )

if stream:
    for chunk in chat_completion_res:
        print(chunk.choices[0].delta.content or "", end="")
else:
    print(chat_completion_res.choices[0].message.content)
  
  

Principais Recursos:

• Endpoint unificado:/v3/openai suporta o formato da API Chat Completions da OpenAI.
• Controles flexíveis: Ajuste temperatura, top-p, penalidades e mais para obter resultados personalizados.
• Streaming e lotes: Escolha o modo de resposta preferido.

Opção 2: Fluxos de Trabalho Multiagente com o SDK de Agentes da OpenAI

Construa sistemas multiagente avançados integrando a Novita AI ao SDK de Agentes da OpenAI:

• Pronto para uso: Use os LLMs da Novita AI em qualquer fluxo de trabalho dos Agentes OpenAI.
• Suporte a handoffs, roteamento e uso de ferramentas: Projete agentes que possam delegar, triar ou executar funções, todos alimentados pelos modelos da Novita AI.
• Integração Python: Basta apontar o SDK para o endpoint da Novita (https://api.novita.ai/v3/openai) e usar sua chave de API.

Conecte a API DeepSeek-Prover-V2-671B em Plataformas de Terceiros

• Hugging Face: Use o DeepSeek-Prover-V2-671B em Spaces, pipelines ou com a biblioteca Transformers por meio de endpoints da Novita AI.
• Estruturas de Agentes e Orquestração: Conecte facilmente a Novita AI com plataformas parceiras como Continue, AnythingLLM, LangChain, Dify e Langflow por meio de conectores oficiais e guias de integração passo a passo.
• API Compatível com OpenAI: Desfrute de migração e integração sem complicações com ferramentas como Cline e Cursor, projetadas para o padrão da API OpenAI.

Conclusão

O DeepSeek-Prover-V2-671B traz prova automatizada de teoremas de classe mundial diretamente para suas mãos — seja você pesquisador, desenvolvedor ou educador. Pronto para experimentar? Cadastre-se na Novita AI, receba seus créditos grátis e experimente o futuro da matemática formal e da geração de provas impulsionada por IA hoje mesmo!

Sobre a Novita AI

Novita AI é uma plataforma de nuvem de IA que oferece aos desenvolvedores uma maneira fácil de implantar modelos de IA usando nossa API simples, além de fornecer uma nuvem de GPU acessível e confiável para construir e escalar.