DeepSeek-Prover-V2: Avanzando el razonamiento matemático formal mediante aprendizaje por refuerzo
DeepSeek-Prover-V2 es un modelo de lenguaje grande de código abierto diseñado para la demostración de teoremas formales en Lean 4. Utiliza un pipeline de demostración de teoremas recursivo impulsado por DeepSeek-V3 y aprendizaje por refuerzo para integrar el razonamiento matemático informal y formal. El modelo comienza descomponiendo problemas complejos en subobjetivos usando DeepSeek-V3, sintetizando las demostraciones de estos subobjetivos para crear datos iniciales para el aprendizaje por refuerzo. DeepSeek-Prover-V2-671B logra un rendimiento de vanguardia, alcanzando una tasa de aprobación del 88,9% en MiniF2F-test y resolviendo 49 problemas de PutnamBench. También se presenta un nuevo conjunto de datos de referencia, ProverBench, que contiene 325 problemas formalizados de competiciones de secundaria y libros de texto.