DeepSeek lanza DeepSeek-Prover-V2 con búsqueda recursiva de pruebas y el nuevo benchmark ProverBench

DeepSeek AI anunció DeepSeek-Prover-V2, un modelo de lenguaje grande de código abierto para la demostración formal de teoremas en Lean 4. El modelo emplea un pipeline recursivo de demostración de teoremas que utiliza DeepSeek-V3 para generar datos de inicialización de alta calidad descomponiendo teoremas complejos en subobjetivos y formalizándolos. Un modelo de 7 mil millones de parámetros demuestra entonces estos subobjetivos, y las demostraciones completas se emparejan con el razonamiento de cadena de pensamiento de DeepSeek-V3 para el entrenamiento. El aprendizaje por refuerzo con retroalimentación binaria refina aún más el modelo. La versión de 671 mil millones de parámetros alcanza un 88,9% en MiniF2F-test y resuelve 49 de los 658 problemas de PutnamBench. DeepSeek también introdujo ProverBench, un conjunto de datos de 325 problemas de competiciones AIME y libros de texto para evaluar el razonamiento matemático. El modelo está disponible en dos tamaños: 7 mil millones y 671 mil millones de parámetros.