DeepSeek lanza DeepSeek-Prover-V2-671B: modelo de próxima generación para demostración automática de teoremas con arquitectura MoE de 671B parámetros 65

小编 · 2025-04-30

DeepSeek AI lanzó el 30 de abril de 2025 DeepSeek-Prover-V2-671B, un modelo de próxima generación para demostración automática de teoremas con una arquitectura MoE de 671B parámetros que genera y verifica demostraciones dentro del marco Lean 4. Entre sus ventajas se encuentran llevar las matemáticas formales a escala GPT-4, mejoras de eficiencia gracias a MoE, y un modelo open-source con uso comercial permitido. Respecto a V1.5 mejora significativamente el

DeepSeek lanza DeepSeek-Prover-V2-671B: modelo de próxima generación para demostración automática de teoremas con arquitectura MoE de 671B parámetros

DeepSeek ai lanzó el 30 de abril de 2025 DeepSeek-Prover-V2-671B, un modelo de demostración automática de teoremas de próxima generación basado en una arquitectura MoE de 671.000 millones de parámetros, que genera y verifica demostraciones dentro del marco Lean 4. Sus ventajas incluyen elevar las matemáticas formales a una escala de "nivel GPT-4", mejoras de eficiencia gracias a MoE, y es de código abierto con uso comercial permitido. En comparación con la versión V1.5, presenta mejoras significativas en número de parámetros, longitud de contexto, tasa de aprobación, entre otros. Se espera un rendimiento excelente en pruebas de referencia como miniF2F, y puede usarse en verificación formal, aceleración de la investigación matemática, entre otros campos. Para usarlo, es necesario descargar los pesos desde Hugging Face y completar la configuración correspondiente.

DeepSeek lanza DeepSeek-Prover-V2-671B: modelo de demostración automática de teoremas de próxima generación basado en arquitectura MoE de 671.000 millones de parámetros.webp

Características técnicas

Cantidad de parámetros y arquitectura: el modelo tiene un total de 671.000 millones de parámetros, adopta una arquitectura MoE, activando aproximadamente 37.000 millones de parámetros por token. Esta arquitectura reduce significativamente los requisitos de memoria mientras mantiene una capacidad de razonamiento potente.
Longitud de contexto: admite un contexto ultra largo, con una incrustación posicional máxima de 163840, capaz de manejar demostraciones matemáticas complejas.
Precisión de cálculo: admite múltiples precisiones de cálculo como BF16, FP8, F32, lo que facilita un entrenamiento e implementación del modelo más rápidos y con menos recursos.
Formato de archivo: utiliza el formato de archivo safetensors más eficiente.
Técnica de cuantización: emplea cuantización FP8, reduciendo el tamaño del modelo mediante técnicas de cuantización y mejorando la eficiencia de inferencia.

Características técnicas.webp

Ventajas clave

Escala y complejidad: el enorme número de parámetros y la ventana de contexto larga (aproximadamente 128k tokens) permiten manejar cadenas lógicas de demostraciones matemáticas más largas y complejas.
Optimización de eficiencia: con la arquitectura MoE, en comparación con un modelo completamente conectado de 671.000 millones de parámetros, reduce significativamente los requisitos de memoria y mejora la velocidad de inferencia.
Código abierto y licencia: el modelo es de código abierto, los pesos están disponibles en Hugging Face y se espera que permita el uso comercial.

Escenarios de aplicación

Verificación formal: realizar comprobaciones rigurosas en demostraciones de seguridad criptográfica o en demostraciones de corrección del diseño de chips.
Aceleración de la investigación matemática: ayudar a los matemáticos a formalizar teoremas existentes, explorar nuevas conjeturas y resolver problemas matemáticos de nivel olímpico.
Herramienta educativa avanzada: crear sistemas de tutoría interactiva que guíen a los estudiantes en la realización de demostraciones formales.
Sistemas críticos de seguridad: verificar propiedades críticas del software e invariantes mediante la integración con Lean antes del despliegue del código.

Pasos de inicio rápido

Obtener el modelo: descargue los pesos desde Hugging Face: deepseek-ai/DeepSeek-Prover-V2-671B.
Configurar Lean: instale Lean 4 (se recomienda versión ≥4.5) y la biblioteca mathlib4.
Verificar el hardware: asegúrese de que la configuración del hardware cumpla los requisitos mínimos (se recomienda una configuración de alto rendimiento).
Instalar el motor de inferencia: configure, por ejemplo, vLLM u otro marco compatible con MoE.
Explorar ejemplos: revise los scripts de evaluación o cuadernos de ejemplo en el repositorio del modelo.

Preguntas frecuentes

¿Es de código abierto? ¿Se puede usar con fines comerciales?

Sí, DeepSeek-Prover-V2-671B es de código abierto (los pesos están disponibles en Hugging Face) y se espera que su licencia permita el uso tanto académico como comercial.

¿Se puede ejecutar en una NVIDIA 4090?

Informes preliminares indican que, gracias a optimizaciones como MoE, MLA y cuantización, el modelo puede ejecutarse en una sola GPU NVIDIA 4090, especialmente cuando se combina con suficiente RAM y un NVMe SSD rápido para la carga dinámica. El rendimiento variará según la configuración específica.