Probando DeepSeek-Prover-V2-671B: Análisis Rápido

El desarrollo de la IA ha traído una nueva ola de modelos especializados diseñados para abordar tareas complejas con una precisión sin precedentes. Entre ellos, DeepSeek Prover V2 ha surgido como un modelo destacado, particularmente en el ámbito de las matemáticas formales y la demostración de teoremas. Este artículo profundiza en qué es DeepSeek Prover V2, cómo acceder y usarlo de forma gratuita en línea, y prueba sus capacidades con indicaciones cuidadosamente elaboradas para evaluar su rendimiento.

¿Qué es DeepSeek-Prover-V2-671B?

DeepSeek-Prover-V2-671B es un modelo de lenguaje con 671 mil millones de parámetros, basado en la arquitectura Mixture-of-Experts (MoE), desarrollado por DeepSeek y optimizado para la demostración formal de teoremas matemáticos. Según publicaciones en X, representa un salto significativo en el razonamiento matemático impulsado por IA, construido sobre la arquitectura de DeepSeek V3 pero adaptado específicamente para tareas de lógica pesada.

El modelo está diseñado para automatizar la generación de pruebas formales utilizando Lean 4, un asistente de pruebas ampliamente utilizado en la investigación matemática. Su entrenamiento en conjuntos de datos sintéticos masivos le permite manejar problemas matemáticos complejos de manera eficiente, convirtiéndolo en una herramienta valiosa para investigadores y matemáticos.

Miembros de la comunidad de IA han destacado sus características clave:

• Una escala de 671 mil millones de parámetros con 37 mil millones de parámetros activos por pase de inferencia, aprovechando 8 expertos activados dinámicamente de 256 por token, con soporte para precisión FP8 y BF16 para un rendimiento optimizado.
• Probablemente soporta una ventana de contexto de hasta 163,840 tokens, heredada de DeepSeek V3, lo que le permite procesar extensos contextos matemáticos con modelado estable de texto largo a través de codificación YaRN RoPE avanzada.
• Lanzado bajo una Licencia MIT para su código y una Licencia de Modelo permisiva para sus pesos, ambas permitiendo el uso comercial.

El modelo es descrito como una "bestia de pruebas matemáticas" en X, sobresaliendo en la automatización de teoremas formales y basándose en el éxito de sus predecesores, que lograron un 63.5% en el benchmark miniF2F y un 25.3% en ProofNet. DeepSeek-Prover-V2-671B se enfoca en la lógica matemática en lugar del razonamiento general, posicionándolo como una herramienta especializada en lugar de un modelo de lenguaje de propósito general.

Su lanzamiento en Hugging Face ha generado entusiasmo, con algunos miembros de la comunidad de IA en X llamándolo una "potencia para pruebas matemáticas formales" y señalando su potencial para superar a otros modelos de código abierto en aplicaciones de matemáticas formales. Se distingue de DeepSeek R2, un modelo de propósito más general esperado pronto, lo que subraya la estrategia de DeepSeek de desarrollar modelos específicos de dominio que superen los límites en áreas nicho. Prover-V2-671B establece un nuevo estándar para la IA en matemáticas formales.

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

Cómo Usar DeepSeek Prover V2 Gratis en Línea

Acceder a DeepSeek Prover V2 es sencillo, gracias a plataformas como OpenRouter, que proporcionan un nivel gratuito para probar el modelo a través de una API compatible con OpenAI. A continuación, se presenta una guía paso a paso para usar DeepSeek Prover V2 de forma gratuita en https://openrouter.ai/models/deepseek/deepseek-prover-v2:free, basada en recursos disponibles y mejores prácticas.

Paso 1: Registrarse en OpenRouter

1. Visita OpenRouter.ai y haz clic en el botón "Sign Up" (Registrarse) en la esquina superior derecha.
2. Regístrate usando un correo electrónico, una cuenta de Google o de GitHub. Se recomienda una cuenta de GitHub para desarrolladores debido a una configuración más rápida.
3. Una vez iniciada la sesión, navega al panel de control.

Paso 2: Localizar DeepSeek Prover V2

1. Desplázate a la sección "Trending Models" (Modelos Populares) o usa la barra de búsqueda para escribir "DeepSeek".
2. Selecciona "DeepSeek: DeepSeek Prover V2 (free)" de la lista. Esto asegura que estás accediendo al modelo del nivel gratuito.

Paso 3: Generar una Clave API

1. En la página del modelo, encuentra el botón "Create API Key" (Crear Clave API) (bajo la descripción del modelo o en la configuración de la cuenta).
2. Nombra tu clave (por ejemplo, "ProverV2-Test") y confirma. Copia la clave y guárdala de forma segura, ya que es necesaria para las solicitudes API.
3. La API de OpenRouter es compatible con OpenAI, lo que simplifica la integración con herramientas existentes.

Paso 4: Configurar tu Entorno

Para interactuar con la API, necesitarás un entorno de programación. Se recomienda Python por su simplicidad. Instala la librería openai si aún no lo has hecho:

pip install openai

Paso 5: Realizar Solicitudes API

Usa el siguiente script de Python para probar DeepSeek Prover V2. Reemplaza YOUR_API_KEY_HERE con tu clave API de 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 envía una indicación a Prover V2 e imprime la respuesta. Puedes ajustar parámetros como temperature (para la creatividad de la respuesta) o max_tokens (para la longitud de la respuesta) según sea necesario.

Paso 6: Monitorear el Uso

El nivel gratuito tiene límites de uso, así que monitorea tu consumo de tokens. OpenRouter garantiza la fiabilidad enrutando las solicitudes a proveedores como "Together" para baja latencia. Si necesitas más capacidad, explora los niveles de pago u otros modelos de DeepSeek en OpenRouter.

Consejos para el Éxito

• Indicaciones Detalladas: Prover V2 es un modelo base optimizado para pruebas, que requiere indicaciones precisas y detalladas para resultados óptimos.
• Manejo de Errores: Implementa mecanismos de reintento, ya que el modelo puede ocasionalmente devolver respuestas vacías.
• Seguridad: Nunca compartas tu clave API públicamente para evitar accesos no autorizados.

Probando DeepSeek Prover V2 con Indicaciones

Para evaluar las capacidades de DeepSeek Prover V2, he diseñado tres indicaciones de prueba que apuntan a sus fortalezas en el razonamiento matemático formal y la demostración de teoremas. Estas indicaciones varían de básicas a avanzadas, reflejando casos de uso comunes en la investigación matemática. Cada indicación está elaborada para evaluar la capacidad del modelo para generar pruebas precisas y formales, idealmente en un formato compatible con Lean 4, dada su especialización.

Comencemos con una Indicación Fácil

Indicación: "prueba que para cualquier par de conjuntos A y B, su intersección es un subconjunto de A; es decir, A ∩ B ⊆ A. Proporciona la prueba completa en Lean 4 y una explicación de un solo enunciado del paso clave."

Respuestas del 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 curiosidad, le pedí al modelo OpenAI o3 que hiciera un comentario sobre la respuesta, y es muy interesante:

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.

Le pasé la respuesta de OpenAI o3 a Deepseek-Prover-V3, y dice:

### 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`.

Y la respuesta de o3 a esta indicación dice:

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.

Es realmente interesante observar el intercambio entre los 2 modelos y cómo se corrigen mutuamente.

Conclusión

DeepSeek Prover V2 es una herramienta innovadora para la demostración formal de teoremas matemáticos, que aprovecha una arquitectura MoE de 671 mil millones de parámetros para automatizar pruebas complejas en Lean 4. Accesible de forma gratuita a través de la API de OpenRouter, ofrece a investigadores y entusiastas una potente plataforma para explorar las matemáticas impulsadas por IA. Las indicaciones de prueba proporcionadas, que cubren teoremas básicos, intermedios y avanzados, demuestran su potencial para manejar diversos desafíos matemáticos. A medida que la IA continúa reconfigurando la investigación académica, Prover V2 destaca como una solución especializada de código abierto que impulsa la innovación en matemáticas formales.