DeepSeek ha lanzado un modelo especializado en el ámbito de la demostración de teoremas matemáticos llamado Prover-V2, cuyo objetivo es utilizar IA para demostrar automáticamente teoremas matemáticos en el sistema de verificación formal Lean 4.
¿Por qué es importante esta dirección?
La demostración de teoremas matemáticos es un campo de prueba extremo para las capacidades de la IA. Esto se debe a que las matemáticas no aceptan "más o menos correcto": una demostración o es completamente correcta o es incorrecta. No existe algo como una "demostración 95% correcta".
Los sistemas de verificación formal (como Lean 4) verifican cada paso del razonamiento lógico de la misma manera que un compilador verifica la sintaxis. Si un paso es incorrecto, toda la demostración arroja un error. Esta es la prueba más rigurosa para la capacidad de razonamiento lógico de la IA.
Rendimiento de Prover-V2
En el benchmark miniF2F, Prover-V2 obtuvo resultados cercanos o iguales a los mejores resultados actuales. El método que utiliza es la descomposición de subobjetivos: dividir una demostración compleja en una serie de subobjetivos más pequeños y resolverlos uno por uno.
Esto es muy similar a la forma de pensar de los matemáticos humanos: ante un problema difícil, primero piensan "para demostrar A, necesito demostrar primero B y C, y para demostrar B, primero necesito confirmar D…"
Diferencia con los modelos de razonamiento de uso general
Los modelos de uso general (GPT, Claude, Gemini) realizan razonamiento matemático basándose en Chain-of-Thought – esencialmente "razonar paso a paso en lenguaje natural". Este enfoque funciona bien para problemas simples, pero en demostraciones complejas es fácil que surja una falla lógica en algún paso.
Prover-V2 sigue la ruta formal, donde cada paso es verificado por Lean 4. La ventaja es que no existen "alucinaciones"; la desventaja es que el ámbito de aplicación es muy limitado: solo funciona dentro de sistemas formales.
Significado
La demostración de teoremas matemáticos es una dirección que parece muy de nicho, pero tiene un impacto profundo. Si la IA realmente puede demostrar de manera confiable teoremas complejos en sistemas formales, podría aplicarse en áreas como verificación de software, verificación de hardware, demostraciones criptográficas y una serie de otros campos críticos.
La inversión de DeepSeek en esta dirección demuestra que no solo están compitiendo en benchmarks de modelos grandes de uso general, sino que también están construyendo seriamente herramientas científicas fundamentales.
Fuente de referencia: CocoLoop, artículo de DeepSeek Prover-V2