DeepSeek-Prover-V2 es el último avance de la iniciativa open source DeepSeek-AI, enfocado en el razonamiento matemático formal. Este modelo de lenguaje de gran tamaño (LLM), entrenado con técnicas de refuerzo y descomposición de subobjetivos, promete transformar la resolución automatizada de teoremas mediante código en Lean 4, el lenguaje de pruebas formales que gana tracción en entornos académicos y matemáticos.
Una IA capaz de razonar en matemáticas formales
A diferencia de otros modelos generales de lenguaje, DeepSeek-Prover-V2 está especializado en construir demostraciones formales paso a paso. Su entrenamiento parte de una técnica de cold start que utiliza otro modelo (DeepSeek-V3) para descomponer problemas complejos en subproblemas más simples, sintetizando razonamientos y pasos formales en Lean 4. Posteriormente, un modelo de menor tamaño (7B) resuelve estos subobjetivos para generar un conjunto de datos inicial que alimenta el entrenamiento reforzado del modelo final.
Este proceso permite unir razonamiento informal (chain-of-thought) con formalización rigurosa en código de demostración, lo que marca una diferencia sustancial respecto a otras aproximaciones anteriores.
Comparativa frente a otros modelos de prueba de teoremas
| Modelo | Formalización en Lean 4 | Entrenamiento por refuerzo | Descomposición de subobjetivos | Precisión miniF2F | Capacidad de contexto |
|---|---|---|---|---|---|
| DeepSeek-Prover-V2-671B | Sí | Sí | Sí | 88,9 % | 8K tokens |
| Minerva (Google, 2022) | No | No | Parcial | ~50 % | 2K–4K tokens |
| GPT-4 (OpenAI) + Chain-of-Thought | Parcial | No | Sí | N/A | Hasta 128K (GPT-4o) |
| LeanCop, LeanDojo | Sí | No | No | N/A | Limitada (manual) |
Nota: miniF2F es un benchmark de problemas matemáticos formales.
DeepSeek-Prover-V2 supera en precisión a anteriores intentos de formalización automática, como LeanCop o métodos basados únicamente en modelos autoregresivos generalistas como GPT-3.
ProverBench: una nueva colección de problemas formales
Además del modelo, DeepSeek también ha lanzado ProverBench, un conjunto de 325 problemas formales divididos en:
- 15 problemas extraídos de AIME 24 y 25 (competencia matemática preuniversitaria en EE. UU.)
- 310 ejercicios extraídos de libros de texto en álgebra, análisis, cálculo y probabilidad.
Este banco permite evaluar el rendimiento del modelo en escenarios reales y educativos, ofreciendo una base más amplia que miniF2F y acercando su uso a entornos pedagógicos.
¿Cómo funciona?
La arquitectura de DeepSeek-Prover-V2 se basa en dos fases:
- Cold-start reasoning: Generación automática de demostraciones a partir de descomposición de teoremas usando DeepSeek-V3 y modelos de menor tamaño.
- Entrenamiento reforzado: Optimización mediante aprendizaje por refuerzo a partir del acierto/error en las demostraciones formales.
Se trata de una técnica que recuerda a AlphaZero, pero aplicada al lenguaje y a la lógica matemática formal.
Ejemplo práctico con Hugging Face Transformers
Puedes probar el modelo directamente desde Hugging Face:
from transformers import AutoModelForCausalLM, AutoTokenizer
import torch
model_id = "DeepSeek-Prover-V2-7B"
tokenizer = AutoTokenizer.from_pretrained(model_id)
model = AutoModelForCausalLM.from_pretrained(model_id, device_map="auto", torch_dtype=torch.bfloat16, trust_remote_code=True)
prompt = """...""" # Aquí va tu código Lean con el teorema a completar
inputs = tokenizer(prompt, return_tensors="pt").to(model.device)
outputs = model.generate(inputs["input_ids"], max_new_tokens=8192)
print(tokenizer.decode(outputs[0]))
Este enfoque es ideal para automatizar tareas en pipelines de verificación formal, integraciones educativas, o como copiloto para desarrolladores Lean.
Modelos y descarga
- DeepSeek-Prover-V2-671B: basado en DeepSeek-V3, modelo de última generación.
- DeepSeek-Prover-V2-7B: más ligero, adecuado para uso local y con soporte para contextos de hasta 32.000 tokens.
Ambos modelos pueden descargarse desde Hugging Face o consultar su repositorio en GitHub.
Conclusión: el futuro de las matemáticas formales es híbrido
DeepSeek-Prover-V2 es más que un modelo de lenguaje: representa un paso decisivo hacia el futuro del razonamiento formal asistido por inteligencia artificial. Su capacidad para combinar razonamiento informal y codificación formal puede cambiar no solo la educación matemática, sino también la verificación de software crítico, pruebas científicas reproducibles y automatización de pruebas en investigación académica.
