La startup china DeepSeek vuelve a la carga con el lanzamiento de Prover V2, una inteligencia artificial pensada exclusivamente para resolver teoremas matemáticos. Sin grandes anuncios ni eventos, la compañía ha publicado este innovador modelo en Hugging Face, despertando el interés de expertos en matemáticas y programación formal.
Prover V2 se especializa en pruebas formales con IA
A diferencia de otros modelos de lenguaje, Prover V2 no es un chatbot ni un asistente generalista. Según lo compartido por la empresa, se trata de una IA diseñada para interactuar con entornos formales como Lean 4, un sistema que permite escribir y verificar demostraciones matemáticas de forma rigurosa.
El objetivo de esta herramienta, según DeepSeek, es acelerar y facilitar la verificación de teoremas complejos, ayudando tanto a investigadores como a estudiantes en sus procesos de razonamiento lógico y matemático.
Esta nueva propuesta se suma a una creciente tendencia en la que la IA deja de imitar el lenguaje humano para adentrarse en tareas altamente especializadas y técnicas.
Dos versiones de Prover V2 con distintos niveles de potencia
De acuerdo con la información publicada, DeepSeek ha lanzado dos versiones de su nuevo modelo: una versión reducida con 7.000 millones de parámetros y otra más potente con 671.000 millones de parámetros, esta última basada en su arquitectura Mixture-of-Experts (MoE).
Este tipo de arquitectura permite que la IA divida el problema en partes y asigne cada una a un “experto” especializado, lo que se traduce en mayor eficiencia y menor consumo de recursos, ya que solo se activan los módulos necesarios en cada caso.
Ambas versiones están disponibles en código abierto, lo que significa que cualquier persona puede descargarlas, analizarlas o adaptarlas a sus necesidades específicas.
Entrenamiento con refuerzo y razonamiento formal
Prover V2 no solo destaca por su tamaño y arquitectura, sino también por su proceso de entrenamiento. La IA fue entrenada con un sistema de aprendizaje por refuerzo y arranque en frío, que consiste en plantear problemas matemáticos al modelo DeepSeek V3 y hacer que este los divida en subtareas más simples.
A partir de esas soluciones parciales, Prover V2 construye un razonamiento coherente que, según la compañía, representa un avance en la integración entre razonamiento informal y formal.
Este enfoque podría abrir nuevas posibilidades en la colaboración entre humanos e IAs, especialmente en el ámbito académico y científico.
Resultados prometedores en benchmarks especializados
Aunque el modelo aún se encuentra en fases tempranas, los resultados iniciales son alentadores. Según datos compartidos por DeepSeek, Prover V2 resolvió 49 de más de 600 problemas del benchmark PutnamBench, uno de los más exigentes en matemáticas avanzadas.
Además, alcanzó un 88,9 % de precisión en el test MiniF2F, centrado en teoremas formales con alto grado de complejidad lógica. Estas cifras lo sitúan entre los modelos más avanzados en su categoría.
No obstante, desde la propia empresa aclaran que Prover V2 no es una solución universal y que aún queda mucho por recorrer en la automatización total de las matemáticas formales.
DeepSeek busca marcar territorio frente a gigantes como Alibaba
El lanzamiento de Prover V2 ha sido interpretado por muchos analistas como una respuesta directa a Qwen3 de Alibaba, otro modelo presentado recientemente. Según algunas fuentes del sector, este movimiento busca reforzar la posición de DeepSeek como uno de los competidores más serios dentro del ecosistema IA.
La compañía ya había llamado la atención con modelos anteriores como DeepSeek R1, que generaron buenos comentarios por su calidad y eficiencia. Además, el próximo lanzamiento de DeepSeek R2 podría marcar un nuevo hito en modelos de razonamiento general.
Incluso Satya Nadella, CEO de Microsoft, destacó en su momento la capacidad de DeepSeek para ofrecer modelos de alto rendimiento a un coste mucho menor que sus homólogos occidentales.
El potencial impacto de Prover V2 en la educación y la ciencia
Más allá de los laboratorios y benchmarks, Prover V2 podría cambiar la forma en que docentes, investigadores y estudiantes abordan las matemáticas. Gracias a su capacidad para generar razonamientos precisos, sería posible automatizar parte del trabajo más tedioso en la verificación de pruebas.
Esto se traduce en más tiempo para pensar, investigar o crear, sin preocuparse tanto por los detalles formales. Además, la publicación en código abierto invita a desarrolladores de todo el mundo a experimentar con el modelo y adaptarlo a nuevos contextos.
En definitiva, Prover V2 es un paso firme hacia un futuro en el que la inteligencia artificial no solo interpreta, sino que también razona. ¿Estamos cerca de ver a las IAs resolviendo problemas matemáticos tan bien como un ser humano? Tal vez no todavía, pero cada vez están más cerca.
Fuente: https://hipertextual.com/2025/04/deepseek-prover-v2-una-ia-especializada-en-teoremas-matematicos