Testando DeepSeek-Prover-V2-671B: Uma Análise Rápida

O desenvolvimento da IA trouxe uma nova onda de modelos especializados projetados para lidar com tarefas complexas com precisão sem precedentes. Entre eles, o DeepSeek Prover V2 surgiu como um destaque, particularmente no domínio da matemática formal e prova de teoremas. Este artigo investiga o que é o DeepSeek Prover V2, como acessá-lo e usá-lo gratuitamente online, e testa suas capacidades com prompts cuidadosamente elaborados para avaliar seu desempenho.

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

O DeepSeek-Prover-V2-671B é um modelo de linguagem Mixture-of-Experts (MoE) de 671 bilhões de parâmetros desenvolvido pela DeepSeek, otimizado para prova de teoremas matemáticos formais. De acordo com postagens no X, ele representa um salto significativo no raciocínio matemático impulsionado pela IA, construído sobre a arquitetura do DeepSeek V3, mas adaptado especificamente para tarefas com forte lógica.

O modelo é projetado para automatizar a geração de provas formais usando Lean 4, um assistente de prova amplamente utilizado em pesquisa matemática. Seu treinamento em enormes conjuntos de dados sintéticos permite que ele lide com problemas matemáticos complexos de forma eficiente, tornando-o uma ferramenta valiosa para pesquisadores e matemáticos.

Membros da comunidade de IA destacaram suas principais características:

• Uma escala de 671B parâmetros com 37B parâmetros ativos por passagem de inferência, utilizando 8 experts ativados dinamicamente de 256 por token, com suporte para precisão FP8 e BF16 para desempenho otimizado.
• Provavelmente suporta uma janela de contexto de até 163.840 tokens, conforme herdado do DeepSeek V3, permitindo processar extensos contextos matemáticos com modelagem estável de texto longo via codificação YaRN RoPE avançada.
• Lançado sob uma Licença MIT para seu código e uma Licença de Modelo permissiva para seus pesos, ambas permitindo uso comercial.

O modelo é descrito como uma "fera da prova matemática" no X, destacando-se na automação de teoremas formais e construindo sobre o sucesso de seus predecessores, que alcançaram 63,5% no benchmark miniF2F e 25,3% no ProofNet. O DeepSeek-Prover-V2-671B foca na lógica matemática em vez de raciocínio geral, posicionando-o como uma ferramenta especializada em vez de um modelo de linguagem de propósito geral.

Seu lançamento no Hugging Face gerou entusiasmo, com alguns membros da comunidade de IA no X chamando-o de "potência para provas matemáticas formais" e observando seu potencial para superar outros modelos de código aberto em aplicações matemáticas formais. Ele é distinto do DeepSeek R2, um modelo mais geral esperado em breve, ressaltando a estratégia da DeepSeek de desenvolver modelos específicos de domínio que ultrapassam os limites em áreas de nicho. O Prover-V2-671B estabelece um novo padrão para IA em matemática formal.

Link do Huggingface: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/tree/main

Como Usar o DeepSeek Prover V2 Gratuitamente Online

Acessar o DeepSeek Prover V2 é simples, graças a plataformas como OpenRouter, que fornecem um nível gratuito para testar o modelo via uma API compatível com OpenAI. Abaixo está um guia passo a passo para usar o DeepSeek Prover V2 gratuitamente em https://openrouter.ai/models/deepseek/deepseek-prover-v2:free, com base em recursos disponíveis e melhores práticas.

Passo 1: Cadastre-se no OpenRouter

1. Visite OpenRouter.ai e clique no botão "Sign Up" no canto superior direito.
2. Registre-se usando um e-mail, conta Google ou GitHub. Uma conta GitHub é recomendada para desenvolvedores devido à configuração mais rápida.
3. Uma vez logado, navegue até o painel.

Passo 2: Localize o DeepSeek Prover V2

1. Role até a seção "Trending Models" ou use a barra de pesquisa para digitar "DeepSeek".
2. Selecione "DeepSeek: DeepSeek Prover V2 (free)" na lista. Isso garante que você está acessando o modelo do nível gratuito.

Passo 3: Gere uma Chave de API

1. Na página do modelo, encontre o botão "Create API Key" (sob a descrição do modelo ou nas configurações da conta).
2. Nomeie sua chave (por exemplo, "ProverV2-Test") e confirme. Copie a chave e armazene-a de forma segura, pois ela é necessária para as requisições da API.
3. A API do OpenRouter é compatível com OpenAI, simplificando a integração com ferramentas existentes.

Passo 4: Configure Seu Ambiente

Para interagir com a API, você precisará de um ambiente de programação. Python é recomendado por sua simplicidade. Instale a biblioteca openai se ainda não o fez:

pip install openai

Passo 5: Faça Requisições da API

Use o seguinte script Python para testar o DeepSeek Prover V2. Substitua YOUR_API_KEY_HERE pela sua chave de API do OpenRouter:

import openai

client = openai.OpenAI(
    base_url="<https://openrouter.ai/api/v1>",
    api_key="YOUR_API_KEY_HERE"
)

response = client.chat.completions.create(
    model="deepseek/deepseek-prover-v2:free",
    messages=[
        {"role": "system", "content": "You are a mathematical proof assistant specializing in formal theorem proving with Lean 4."},
        {"role": "user", "content": "Prove that the sum of two even numbers is even."}
    ]
)

print(response.choices[0].message.content)

Este script envia um prompt para o Prover V2 e imprime a resposta. Você pode ajustar parâmetros como temperature (para criatividade da resposta) ou max_tokens (para comprimento da resposta) conforme necessário.

Passo 6: Monitore o Uso

O nível gratuito tem limites de uso, então monitore seu consumo de tokens. O OpenRouter garante confiabilidade roteando requisições para provedores como "Together" para baixa latência. Se precisar de mais capacidade, explore níveis pagos ou outros modelos DeepSeek no OpenRouter.

Dicas para Sucesso

• Prompts Detalhados: O Prover V2 é um modelo base otimizado para testes, exigindo prompts precisos e detalhados para resultados ótimos.
• Tratamento de Erros: Implemente mecanismos de repetição, pois o modelo pode ocasionalmente retornar respostas vazias.
• Segurança: Nunca compartilhe sua chave de API publicamente para evitar acesso não autorizado.

Testando o DeepSeek Prover V2 com Prompts

Para avaliar as capacidades do DeepSeek Prover V2, projetei três prompts de teste que visam seus pontos fortes em raciocínio matemático formal e prova de teoremas. Esses prompts variam de básico a avançado, refletindo casos de uso comuns em pesquisa matemática. Cada prompt é elaborado para avaliar a capacidade do modelo de gerar provas formais precisas, idealmente em um formato compatível com Lean 4, dada sua especialização.

Vamos Começar com um Prompt Fácil

Prompt: "prove that for any two sets A and B, their intersection is a subset of A; that is. A ∩ B ⊆ A.Provide the complete Lean 4 proof and a one-sentence explanation of the key step."

Respostas do Modelo Deepseek-Prover-V2:

### Lean 4 Proof

```lean
theorem intersection_subset_left (A B : Type) (a : A) : A ∩ B ⊆ A := by
  intro x hx
  cases hx with
  | intro hx₁ hx₂ =>
    exact hx₁
  <;> simp_all
```

### Explanation of the Key Step

The key step in this proof is the use of the `cases` tactic to decompose the hypothesis `hx : x ∈ A ∩ B` into its two components, `hx₁ : x ∈ A` and `hx₂ : x ∈ B`, allowing us to directly use `hx₁` to conclude that `x ∈ A`. 

### One-Sentence Explanation

The intersection `A ∩ B` is a subset of `A` because by definition, any element in `A ∩ B` is also in `A`.

Por curiosidade, pedi ao modelo OpenAI o3 para fazer um comentário sobre a resposta, e é muito interessante:

Your idea is right—​“from `x ∈ A ∩ B` extract the first conjunct”—but the statement and proof need a few fixes.

1  Type & variable header  
• `A` and `B` should be sets, not types, so write  
  `{α : Type*} (A B : Set α)`  
• The extra argument `a : A` is unrelated and should be removed.

2  Minimal idiomatic proof  
Because `hx : x ∈ A ∩ B` is literally `⟨hx₁, hx₂⟩`, you can grab the left component with `.1` (or `.left`) instead of destructuring with `cases`.  
```lean
open Set

theorem inter_subset_left {α} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1          -- or `exact hx.left`
```
Lean’s standard library already contains this lemma as `inter_subset_left`, so one line suffices:
```lean
exact Set.inter_subset_left
```

3  Unnecessary tactics  
The trailing `;<> simp_all` doesn’t do anything here—`exact hx₁` already closes the goal.

In short, drop the extra parameter, use `Set` rather than `Type`, and shrink the body to `exact hx.1` (or just reuse the builtin lemma) for a clean, conventional proof.

Enviei a resposta do OpenAI o3 para o Deepseek-Prover-V3, e ele disse:

### Revised Lean 4 Proof

```lean
theorem intersection_subset_left {α : Type*} (A B : Set α) : A ∩ B ⊆ A := by
  intro x hx
  exact hx.1
```

### One-Sentence Explanation

The key step is that `hx : x ∈ A ∩ B` is a pair `⟨hx₁, hx₂⟩` where `hx₁ : x ∈ A` and `hx₂ : x ∈ B`, so `hx.1` directly gives `x ∈ A`, proving `A ∩ B ⊆ A`.

### Additional Notes

1. The proof correctly uses `Set α` instead of `Type` to represent sets.
2. The `{α : Type*}` syntax allows the theorem to be generic over any type `α`.
3. The unnecessary parameter `a : A` and trailing tactics have been removed.
4. The `open Set` command is omitted because we use the full name `Set α`.
5. The proof leverages the fact that `hx.1` directly extracts the first component of `hx`, which is `x ∈ A`.

E a resposta do o3 a este prompt diz:

Your revision is spot-on.

• Correctness and conciseness `hx.1` (alias `hx.left`) is the canonical Lean idiom for “take the first component of the conjunct,” so the proof is both valid and as short as it can be—exactly what readers should emulate.

• Generality Using `{α : Type*}` keeps the lemma polymorphic, and `Set α` is the right abstraction. Good call on deleting the stray parameter and tactics.

• Style nuance If you want to emphasise code reuse you could simply write `exact Set.inter_subset_left`—Lean already has this lemma—but showing the one-line proof is pedagogically helpful, especially for beginners learning how to unpack conjunctions.

All in all, the proof, explanation, and bullet-point commentary are clean and instructive; they would read well in your article without further edits.

É realmente interessante observar o vai e vem dos 2 modelos e corrigindo um ao outro.

Conclusão

O DeepSeek Prover V2 é uma ferramenta inovadora para prova de teoremas matemáticos formais, utilizando uma arquitetura MoE de 671B parâmetros para automatizar provas complexas em Lean 4. Acessível gratuitamente via API do OpenRouter, ele oferece a pesquisadores e entusiastas uma plataforma poderosa para explorar a matemática impulsionada pela IA. Os prompts de teste fornecidos — cobrindo teoremas básicos, intermediários e avançados — demonstram seu potencial para lidar com diversos desafios matemáticos. À medida que a IA continua a remodelar a pesquisa acadêmica, o Prover V2 se destaca como uma solução especializada e de código aberto impulsionando a inovação em matemática formal.