[공지사항]을 빙자한 안부와 근황 
Show more

Daily Arxiv

Esta página recopila y organiza artículos sobre inteligencia artificial publicados en todo el mundo.
La información aquí presentada se resume utilizando Google Gemini y el sitio se gestiona sin fines de lucro.
Los derechos de autor de los artículos pertenecen a sus autores y a las instituciones correspondientes; al compartir el contenido, basta con citar la fuente.

DeepSeek-Prover-V2: Avanzando en el razonamiento matemático formal mediante el aprendizaje por refuerzo para la descomposición de subobjetivos

Created by
  • Haebom

Autor

ZZ Ren, Zhihong Shao, Junxiao Song, Huajian

Describir

DeepSeek-Prover-V2 es un modelo de lenguaje de código abierto a gran escala diseñado para la demostración formal de teoremas en Lean 4. Se inicializa con datos recopilados mediante un flujo de trabajo recursivo de demostración de teoremas basado en DeepSeek-V3. Realiza un entrenamiento de arranque en frío aprovechando la capacidad de DeepSeek-V3 para descomponer problemas complejos en múltiples subobjetivos. Las demostraciones de los subobjetivos resueltos se combinan con inferencias paso a paso de DeepSeek-V3 para generar datos iniciales para el aprendizaje por refuerzo. Esto integra razonamiento matemático formal e informal. El modelo resultante, DeepSeek-Prover-V2-671B, alcanza un rendimiento de vanguardia en la demostración de teoremas de redes neuronales, con una tasa de aprobación del 88,9 % en el test MiniF2F y resolviendo 49 de 658 problemas de PutnamBench. Presentamos una nueva métrica, ProverBench (325 problemas formalizados), que incluye 15 problemas de la reciente competencia AIME (24-25). Los resultados de la evaluación muestran que resuelve 6 de los 15 problemas AIME, lo que demuestra que la brecha entre el razonamiento matemático formal e informal se reduce significativamente en comparación con el método de votación mayoritaria de DeepSeek-V3 (que resuelve 8 problemas).

Takeaways, Limitations

Takeaways:
DeepSeek-Prover-V2 logra un rendimiento de última generación en la demostración de teoremas de redes neuronales.
Presentamos un enfoque novedoso que integra el razonamiento formal e informal.
Un nuevo punto de referencia, ProverBench, permite una evaluación más amplia.
Demostramos que la brecha entre el razonamiento formal e informal se está reduciendo en los modelos de lenguaje a gran escala.
Limitations:
Las tasas de solución para los problemas de PutnamBench y AIME aún no son perfectas (49/658 para PutnamBench y 6/15 para AIME).
El modelo puede carecer de poder explicativo sobre su proceso de inferencia.
Es necesario ampliar aún más la escala de ProverBench.
👍