Lo curioso del caso es que DeepSeek no ha realizado anuncios formales sobre el lanzamiento de Prover V2. La startup china ha publicado el modelo, junto con su correspondiente descripción, a Hugging Face, pero todavía no se ha expresado con mayor detalle sobre las capacidades de esta nueva tecnología.

DeepSeek Prover V2 se ha lanzado en dos versiones. Una de ellas es de 7.000 millones de parámetros y se basa en Prover V1.5-Base, mientras que la otra es de 671.000 millones de parámetros y su entrenamiento se ha concretado sobre DeepSeek V3-Base.

Es importante mencionar que, como se trata de una IA especializada para una labor bastante específica, DeepSeek Prover V2 no se ha desarrollado para impulsar un chatbot convencional. Según revelan sus creadores, se ha diseñado para demostrar formalmente teoremas en Lean 4, un lenguaje de programación y demostrador de teoremas interactivo.

DeepSeek Prover V2, una nueva IA de código abierto enfocada en las matemáticas

Desde DeepSeek indican que Prover V2 utiliza un procedimiento de entrenamiento de aprendizaje por refuerzo con "arranque en frío". Este consiste en pedirle a DeepSeek V3 que descomponga problemas complejos en una serie de subobjetivos, para luego sintetizar las demostraciones de los subobjetivos resueltos en una cadena de pensamiento. Esto se combina con las capacidades de razonamiento paso a paso de DeepSeek V3.

De la mano de ese complejo procedimiento, Prover V2 logra unificar los razonamientos matemáticos informales y formales. DeepSeek sostiene que el funcionamiento de su nueva IA es lo suficientemente bueno como para destacarse en algunos de los benchmarks más destacados del segmento.

En tal sentido, la firma china remarca que DeepSeek Prover V2 ha resuelto 49 de los más de 600 problemas estipulados en las pruebas de PutnamBench. Asimismo, ha logrado una aprobación del 88,9 % en MiniF2F, una prueba destinada a la demostración de teoremas neuronales.

El lanzamiento de DeepSeek Prover V2 se produce un día después de que Alibaba lanzara Qwen3. Además, llega en un momento crucial para la startup china y sus planes a futuro. Recordemos que la compañía ha prometido que durante mayo se va a concretar el lanzamiento de DeepSeek R2, su próximo modelo de razonamiento.

La irrupción de DeepSeek en el mercado de la inteligencia artificial generativa no ha pasado desapercibida. La firma asiática no solo puso al mundo patas arriba con sus modelos supuestamente entrenados a una fracción del coste de las principales propuestas occidentales, sino que también se ganó el visto bueno de los grandes jugadores del sector. El propio CEO de Microsoft reconoció que DeepSeek representaba un nuevo estándar para la industria de la IA.

Fuentes:
https://hipertextual.com/2025/04/deepseek-prover-v2-una-ia-especializada-en-teoremas-matematicos