¿Puede la IA razonar como un matemático?
DeepSeek-Prover-V2 desafía los límites de la inteligencia artificial: del cálculo a la lógica formal.
Hoy vengo con otra novedad procedente de DeepSeek: la cosa ya no va de responder a preguntas “tipo ChatGPT”, sino de resolver teoremas formales. Puede parecer una excentricidad académica, pero representa uno de los avances más significativos en la historia reciente del razonamiento automatizado.
Qué es DeepSeek-Prover-V2
El modelo se ha entrenado con Lean 4, una herramienta para demostraciones matemáticas formales que cada vez gana más adeptos en la comunidad científica. Pero no estamos ante una simple mejora incremental: DeepSeek-Prover-V2 se basa en una arquitectura MoE (Mixture of Experts) de 671 billones (americanos) de parámetros, lo que le permite seleccionar dinámicamente expertos distintos para distintas fases del razonamiento.
(para contextualizar cuán grande son 671 billones de parámetros: el modelo GPT-4 de OpenAI se estima que tiene entre 1.000 y 1.760 billones de parámetros.Gemini 1.5 de Google opera con arquitecturas de unos 1.600 billones. Modelos como GPT-3 (175 billones) o LLaMA 2 (70 billones) quedan muy por debajo en tamaño total)
El resultado es un sistema que descompone teoremas complejos en subobjetivos, como haría un humano, y construye demostraciones paso a paso.
Impacto y resultados
DeepSeek-Prover-V2 ha conseguido resultados espectaculares, como un 88,9% de éxito en el benchmark MiniF2F, o resolver correctamente 49 de los 658 problemas del exigente conjunto PutnamBench. Aunque este último número parezca poca cosa, estos resultados superan ampliamente los logrados por modelos anteriores y consolidan a DeepSeek como uno de los actores más innovadores en IA aplicada a la matemática formal.
Lo más relevante, sin embargo, no es solo el rendimiento, sino la forma en que el modelo razona: combina lenguaje natural, conocimiento matemático abstracto y formalismo técnico en una secuencia lógica comprensible y verificable.
Un cambio de paradigma?
Hasta ahora, la IA ha sido imbatible en todo lo que tiene que ver con el cálculo: extracción de patrones a partir de datos, optimización de funciones, búsqueda de soluciones por fuerza bruta o aprendizaje estadístico. Sin embargo, no había conseguido razonar de forma estructurada sobre conceptos abstractos o deducir teoremas a partir de axiomas.
DeepSeek-Prover-V2 no solo razona: demuestra. Y lo hace en un lenguaje formal que puede ser auditado, corregido y reutilizado. Esto abre la puerta a una nueva era en la que la IA no solo procesa información, sino que construye conocimiento estructurado.
La pregunta que queda en el aire es si estamos ante un caso aislado de especialización algorítmica o si, en cambio, estamos asistiendo a un cambio de paradigma: una transición desde la IA como herramienta de procesamiento hacia la IA como agente capaz de argumentar y construir.
El tiempo y los siguientes papers lo dirán. Pero la frontera del pensamiento ya se ha movido. Y eso, sin duda, es noticia.
PS: el artículo donde se explica todo esto ha sido publicado “solamente” en GitHub, y lo puedes leer aquí. DeepSeek sigue sin publicar en revistas científicas internacionales con revisión por pares…