DeepSeekMath-V2: Hacia un Razonamiento Matemático Autoverificable
DeepSeekMath-V2: Towards Self-Verifiable Mathematical Reasoning
November 27, 2025
Autores: Zhihong Shao, Yuxiang Luo, Chengda Lu, Z. Z. Ren, Jiewen Hu, Tian Ye, Zhibin Gou, Shirong Ma, Xiaokang Zhang
cs.AI
Resumen
Los grandes modelos de lenguaje han logrado avances significativos en el razonamiento matemático, que sirve como un importante banco de pruebas para la IA y podría impactar la investigación científica si continúa avanzando. Mediante la escalabilidad del razonamiento con aprendizaje por refuerzo que premia respuestas finales correctas, los LLM han evolucionado de un rendimiento deficiente a saturar competencias de razonamiento cuantitativo como AIME y HMMT en un año. Sin embargo, este enfoque enfrenta limitaciones fundamentales. Buscar una mayor precisión en las respuestas finales no aborda un problema clave: las respuestas correctas no garantizan un razonamiento correcto. Además, muchas tareas matemáticas como la demostración de teoremas requieren una derivación rigurosa paso a paso en lugar de respuestas numéricas, haciendo inaplicables las recompensas por respuestas finales. Para superar los límites del razonamiento profundo, creemos necesario verificar la exhaustividad y el rigor del razonamiento matemático. La autoverificación es particularmente importante para escalar el cómputo en tiempo de prueba, especialmente para problemas abiertos sin soluciones conocidas. Hacia un razonamiento matemático autoverificable, investigamos cómo entrenar un verificador preciso y fiel basado en LLM para demostración de teoremas. Luego entrenamos un generador de demostraciones utilizando el verificador como modelo de recompensa, incentivando al generador a identificar y resolver tantos problemas como sea posible en sus propias demostraciones antes de finalizarlas. Para mantener la brecha generación-verificación a medida que el generador se fortalece, proponemos escalar el cómputo de verificación para etiquetar automáticamente nuevas demostraciones difíciles de verificar, creando datos de entrenamiento para mejorar aún más el verificador. Nuestro modelo resultante, DeepSeekMath-V2, demuestra sólidas capacidades para demostrar teoremas, alcanzando puntuaciones de nivel oro en la IMO 2025 y CMO 2024 y un casi perfecto 118/120 en el Putnam 2024 con cómputo escalado en tiempo de prueba.
English
Large language models have made significant progress in mathematical reasoning, which serves as an important testbed for AI and could impact scientific research if further advanced. By scaling reasoning with reinforcement learning that rewards correct final answers, LLMs have improved from poor performance to saturating quantitative reasoning competitions like AIME and HMMT in one year. However, this approach faces fundamental limitations. Pursuing higher final answer accuracy doesn't address a key issue: correct answers don't guarantee correct reasoning. Moreover, many mathematical tasks like theorem proving require rigorous step-by-step derivation rather than numerical answers, making final answer rewards inapplicable. To push the limits of deep reasoning, we believe it is necessary to verify the comprehensiveness and rigor of mathematical reasoning. Self-verification is particularly important for scaling test-time compute, especially for open problems without known solutions. Towards self-verifiable mathematical reasoning, we investigate how to train an accurate and faithful LLM-based verifier for theorem proving. We then train a proof generator using the verifier as the reward model, and incentivize the generator to identify and resolve as many issues as possible in their own proofs before finalizing them. To maintain the generation-verification gap as the generator becomes stronger, we propose to scale verification compute to automatically label new hard-to-verify proofs, creating training data to further improve the verifier. Our resulting model, DeepSeekMath-V2, demonstrates strong theorem-proving capabilities, achieving gold-level scores on IMO 2025 and CMO 2024 and a near-perfect 118/120 on Putnam 2024 with scaled test-time compute.