Resolución de teoremas con IA, DeepSeek presenta Prover-V2
La empresa china de inteligencia artificial DeepSeek ha presentado una versión actualizada de su modelo DeepSeek-Prover-V2, diseñado específicamente para demostrar teoremas matemáticos de manera formal.
Este modelo de lenguaje avanzado (LLM) utiliza el lenguaje de programación Lean 4 para verificar la consistencia lógica de las pruebas matemáticas, analizando cada paso de forma independiente. Al igual que sus lanzamientos anteriores, DeepSeek-Prover-V2 es de código abierto y está disponible en plataformas como GitHub y Hugging Face.
¿Cómo funciona DeepSeek-Prover-V2?
El nuevo modelo está basado en DeepSeek-V3, lanzado en diciembre de 2024, y se especializa en razonamiento matemático con un enfoque de cadena de pensamiento (CoT). Entre sus capacidades destacan:
– Resolver problemas matemáticos de nivel bachillerato a universitario.
– Detectar y corregir errores en demostraciones de teoremas.
– Funcionar como herramienta educativa, generando explicaciones paso a paso.
– Asistir a investigadores en la exploración y validación de nuevos teoremas.
Especificaciones técnicas y entrenamiento
DeepSeek-Prover-V2 está disponible en dos versiones:
– Un modelo de 7 mil millones de parámetros, basado en DeepSeek-Prover-V1.5, con un contexto de hasta 32.000 tokens.
– Un modelo más grande de 671 mil millones de parámetros, entrenado sobre DeepSeek-V3-Base.
Para su desarrollo, los investigadores implementaron un sistema de entrenamiento “cold-start”, en el que el modelo base descompone problemas complejos en subobjetivos. Las demostraciones de estos subobjetivos se integran en la cadena de razonamiento (CoT) y se combinan con el modelo base para mejorar el aprendizaje por refuerzo.
Disponibilidad y futuro de los modelos de IA especializados
Además de GitHub, el modelo puede descargarse desde la página de DeepSeek en Hugging Face. Este lanzamiento demuestra cómo los ajustes iterativos en el entrenamiento pueden potenciar las capacidades de la IA en dominios especializados, como las matemáticas.
Aunque DeepSeek mantiene en reserva detalles sobre la arquitectura y el conjunto de datos utilizado, su enfoque en modelos abiertos y accesibles sigue impulsando la innovación en el campo de la inteligencia artificial.
Fuente: DeepSeek
