DeepSeek, la prometedora startup china de inteligencia artificial, vuelve a llamar la atención del sector con el lanzamiento silencioso de Prover V2, una IA de código abierto enfocada en la demostración formal de teoremas matemáticos. A pesar de no haber realizado anuncios formales, la compañía publicó recientemente el modelo en Hugging Face, junto con una descripción técnica que revela su potencial.
La propuesta no es menor: Prover V2 no es un chatbot ni un modelo generalista, sino una herramienta especializada que busca transformar la manera en que los matemáticos interactúan con sistemas formales como Lean 4, un lenguaje de programación utilizado para escribir y verificar pruebas matemáticas de manera rigurosa.
¿Qué es Prover V2 y qué lo hace diferente?
DeepSeek ha lanzado dos versiones de Prover V2:
- Una versión reducida de 7.000 millones de parámetros, basada en Prover V1.5-Base.
- Otra de 671.000 millones de parámetros, entrenada sobre DeepSeek V3-Base, un modelo de arquitectura Mixture-of-Experts (MoE) que divide las tareas en subtareas manejadas por componentes expertos especializados.
Este enfoque, propio de los modelos más avanzados, permite un mayor rendimiento con menor consumo de recursos al activar solo los “expertos” necesarios para cada tarea.
También te puede interesar:Microsoft Prohíbe DeepSeek Por Motivos de Seguridad y Riesgo de Propaganda ChinaAdemás, Prover V2 utiliza un proceso de entrenamiento particular: un sistema de aprendizaje por refuerzo con “arranque en frío”. En este procedimiento, se le pide al modelo DeepSeek V3 que descomponga problemas matemáticos complejos en subtareas más simples.
Luego, Prover V2 sintetiza las soluciones obtenidas en una única línea de razonamiento coherente, lo que representa un avance clave en la integración del razonamiento informal y formal en IA.
Resultados que avalan su rendimiento
Aunque aún en fases iniciales, los resultados presentados por DeepSeek son prometedores:
- 49 problemas resueltos de más de 600 en el benchmark PutnamBench, una prueba diseñada para medir la capacidad de las IAs en resolver problemas de matemáticas avanzadas.
- 88,9 % de precisión en MiniF2F, otro test centrado en la resolución de teoremas formales con razonamiento profundo.
Estos números colocan a Prover V2 como una de las IA más efectivas en su campo, aunque todavía lejos de una solución universal para las matemáticas formales.
También te puede interesar:Microsoft Prohíbe DeepSeek Por Motivos de Seguridad y Riesgo de Propaganda China¿Qué busca DeepSeek con este movimiento?
El lanzamiento de Prover V2 llega apenas un día después de que Alibaba presentara su nuevo modelo Qwen3, lo que sugiere una estrategia de DeepSeek para mantenerse relevante en la carrera por la supremacía en inteligencia artificial generativa.
Además, este movimiento se enmarca en la antesala del próximo gran lanzamiento de la compañía: DeepSeek R2, un modelo que promete avances importantes en razonamiento general.
A pesar de su bajo perfil mediático, DeepSeek ha ganado notoriedad en la industria. El propio CEO de Microsoft destacó su capacidad de ofrecer modelos altamente competitivos a una fracción del costo que manejan empresas occidentales.
Esta eficiencia, unida a la apuesta por el código abierto y la especialización, ha posicionado a la startup como una referencia emergente en el ecosistema global de IA.
¿El futuro de las matemáticas asistidas por IA?
Prover V2 no solo representa un nuevo modelo, sino un paso más hacia la automatización formal del conocimiento matemático. Herramientas como esta podrían revolucionar el trabajo de investigadores, docentes y estudiantes, facilitando el desarrollo y verificación de pruebas complejas en menor tiempo y con menor margen de error.
Me dedico al SEO y la monetización con proyectos propios desde 2019. Un friki de las nuevas tecnologías desde que tengo uso de razón.
Estoy loco por la Inteligencia Artificial y la automatización.
