Tras un período de inactividad, DeepSeek ha retomado el protagonismo con el lanzamiento de Prover V2, una innovadora solución de inteligencia artificial de código abierto que se especializa en la demostración de teoremas matemáticos.
Curiosamente, DeepSeek no ha hecho anuncios oficiales sobre Prover V2. La compañía china ha subido el modelo y su descripción a la plataforma Hugging Face, pero aún no ha proporcionado detalles extensos sobre las funcionalidades de esta nueva herramienta.
El modelo DeepSeek Prover V2 se presenta en dos variantes: una con 7.000 millones de parámetros que sigue la línea de Prover V1.5-Base, y otra con 671.000 millones de parámetros, entrenada sobre la base de DeepSeek V3-Base.
Es crucial destacar que, al ser una IA diseñada para una función muy específica, DeepSeek Prover V2 no está destinada a operar como un chatbot estándar. Según sus desarrolladores, está configurada para llevar a cabo demostraciones formales de teoremas utilizando Lean 4, un lenguaje de programación y sistema interactivo de demostración de teoremas.
DeepSeek Prover V2: Innovación en IA de código abierto para las matemáticas
Desde DeepSeek explican que Prover V2 aprovecha un método de entrenamiento de aprendizaje por refuerzo denominado «arranque en frío». Este método implica que DeepSeek V3 desglose problemas complicados en subobjetivos menores, para después sintetizar las soluciones de estos subobjetivos en una secuencia lógica, utilizando también las capacidades de razonamiento secuencial de DeepSeek V3.
Gracias a este complejo método, Prover V2 es capaz de integrar el razonamiento matemático tanto informal como formal. DeepSeek afirma que el desempeño de su nueva IA es sobresaliente, destacándose en varios de los benchmarks más importantes de la industria.
En este contexto, la compañía china subraya que DeepSeek Prover V2 ha logrado resolver 49 de los más de 600 problemas planteados en los desafíos de PutnamBench. Además, ha alcanzado un 88.9 % de éxito en MiniF2F, un test diseñado para la demostración de teoremas mediante redes neuronales.
El debut de DeepSeek Prover V2 ocurre justo un día después del lanzamiento de Qwen3 por parte de Alibaba, y en un momento clave para la startup china y su estrategia a futuro. Recordemos que la empresa prometió que en mayo realizará el lanzamiento de DeepSeek R2, su próximo modelo de razonamiento.
La entrada de DeepSeek en el mercado de la inteligencia artificial generativa ha sido notable. La firma no solo ha revolucionado el sector con modelos que afirma haber entrenado a una fracción del costo de las propuestas occidentales predominantes, sino que también ha recibido el reconocimiento de grandes nombres de la industria, incluyendo al propio CEO de Microsoft, quien ha mencionado que DeepSeek establece un nuevo estándar en el ámbito de la IA.
Hola, soy Carlos, parte del equipo de MuyMac. Me apasiona compartir las últimas novedades en entretenimiento y conectarte con el mundo del cine, la música y la cultura pop.
