DeepSeek ha presentado DeepSeek-Prover-V2, un innovador modelo de lenguaje grande (LLM) de código abierto meticulosamente diseñado para el intrincado dominio de la demostración formal de teoremas dentro del marco de Lean 4. Este novedoso modelo aprovecha un canal de demostración de teoremas recursivo, aprovechando el poder del modelo base DeepSeek-V3 de vanguardia de DeepSeek. Lean 4, la última iteración del demostrador de teoremas Lean, se erige como un asistente de prueba interactivo desarrollado por Microsoft Research. Este sofisticado lenguaje de programación funcional y sistema interactivo de demostración de teoremas permite a los matemáticos e informáticos construir pruebas formales con una verificación automatizada sin precedentes.
El proyecto significa un paso monumental hacia la superación de la brecha entre el razonamiento matemático formal e informal. Al capitalizar las capacidades inherentes de los LLM de propósito general, busca abordar eficazmente el dominio altamente estructurado de la demostración formal de teoremas. El equipo de investigación de DeepSeek postula que su enfoque innovador refleja los procesos cognitivos empleados por los matemáticos humanos al construir pruebas, diseccionando meticulosamente teoremas complejos en componentes más manejables y comprensibles.
Ampliando el marco de evaluación: Presentación de ProverBench
En un movimiento significativo para mejorar el rigor de su investigación, el equipo de DeepSeek ha ampliado significativamente su marco de evaluación con la introducción de ProverBench, una colección de referencia completamente nueva meticulosamente diseñada específicamente para la evaluación integral de las capacidades de demostración formal de teoremas. Esta colección integral sirve como un recurso valioso para evaluar el rendimiento de los LLM en el contexto de las matemáticas formales.
"Más allá de los puntos de referencia convencionales, presentamos con orgullo ProverBench, una colección meticulosamente seleccionada de 325 problemas formalizados, para enriquecer nuestro proceso de evaluación. Esta colección incluye 15 problemas cuidadosamente seleccionados procedentes directamente de las recientes competiciones del American Invitational Mathematics Examination (AIME), específicamente de los años 24-25", explicaron los investigadores.
La inclusión de problemas AIME en el conjunto de datos de ProverBench es particularmente notable, ya que introduce un conjunto de problemas matemáticos desafiantes y bien establecidos que son ampliamente reconocidos dentro de la comunidad matemática. Esto proporciona una base estandarizada y rigurosa para evaluar el rendimiento de DeepSeek-Prover-V2 y compararlo con otros enfoques.
Resultados iniciales prometedores: Abordando los problemas de AIME
Los resultados iniciales derivados de las pruebas rigurosas de estos desafiantes problemas de AIME han revelado un rendimiento excepcionalmente prometedor de su modelo especializado de demostración de teoremas meticulosamente diseñado. El equipo de DeepSeek informa con orgullo que DeepSeek-Prover-V2 demostró su destreza al resolver con éxito 6 de los 15 problemas AIME presentados. En comparación, el modelo DeepSeek-V3 de propósito general, cuando utiliza técnicas de votación mayoritaria, logró resolver con éxito 8 problemas.
Estos hallazgos resaltan el potencial tanto de los LLM especializados como de propósito general para abordar problemas matemáticos complejos. Si bien el modelo de propósito general exhibió una tasa de éxito ligeramente mayor en este punto de referencia en particular, el modelo especializado de demostración de teoremas demostró su competencia en el razonamiento matemático formal.
Imitando la construcción de pruebas humanas: Un enfoque de cadena de pensamiento
"Dadas las dificultades bien documentadas que los modelos de propósito general a menudo encuentran al intentar producir pruebas Lean completas, instruimos estratégicamente a DeepSeek-V3 para que genere solo un esquema de prueba de alto nivel, omitiendo deliberadamente los detalles intrincados. La cadena de pensamiento resultante culmina en un teorema Lean compuesto por una secuencia de declaraciones have, cada una meticulosamente concluida con un marcador de posición sorry, que indica efectivamente un subobjetivo que debe resolverse. Este enfoque innovador refleja elegantemente el estilo humano de construcción de pruebas, en el que un teorema complejo se reduce incrementalmente a una secuencia de lemas más manejables", explicó el equipo de DeepSeek.
Este enfoque innovador de generar esquemas de prueba de alto nivel se alinea con la forma en que los matemáticos a menudo abordan pruebas complejas. Al centrarse en la estructura general y los pasos clave, el modelo puede guiar eficazmente el posterior refinamiento y finalización de la prueba.
Una estrategia metódica: Abordando cada componente de la prueba individualmente
El sistema luego emplea meticulosamente una estrategia metódica y estructurada para abordar cada componente individual de la prueba. Este enfoque sistemático asegura que cada aspecto de la prueba sea cuidadosamente considerado y abordado de una manera lógica y coherente. El sistema crea un enfoque altamente estructurado para la demostración de teoremas, basándose en resultados previamente establecidos para asegurar una base sólida para cada paso subsiguiente.
"Aprovechando los subobjetivos generados por DeepSeek-V3, adoptamos una estrategia de resolución recursiva para resolver sistemáticamente cada paso de prueba intermedio. Extraemos expresiones de subobjetivo de las declaraciones have para sustituirlas por los objetivos originales en los problemas dados y luego incorporamos los subobjetivos precedentes como premisas. Esta construcción permite que los subobjetivos subsiguientes se resuelvan utilizando los resultados intermedios de los pasos anteriores, promoviendo así una estructura de dependencia más localizada y facilitando el desarrollo de lemas más simples", detallaron los investigadores.
La estrategia de resolución recursiva es un aspecto clave de la capacidad del sistema para manejar pruebas complejas. Al dividir el problema en subobjetivos más pequeños y manejables, el sistema puede aplicar eficazmente sus capacidades de razonamiento a cada componente individual.
Optimizando los recursos computacionales: Un modelo especializado de 7B parámetros
Para optimizar eficazmente los recursos computacionales y asegurar un procesamiento eficiente, el sistema emplea estratégicamente un modelo más pequeño y altamente especializado de 7B parámetros para procesar los lemas descompuestos. Este enfoque es crucial para gestionar eficazmente las demandas computacionales asociadas con las extensas búsquedas de pruebas, asegurando que el sistema pueda operar eficientemente sin ser abrumado por la complejidad del espacio de búsqueda. El enfoque finalmente culmina en una prueba completa derivada automáticamente cuando todos los pasos descompuestos se resuelven con éxito.
"El marco algorítmico opera en dos etapas distintas, aprovechando dos modelos complementarios: DeepSeek-V3 para la descomposición de lemas y un modelo de demostrador de 7B para completar los detalles formales de la prueba correspondientes", describieron los investigadores.
Este enfoque de dos etapas permite al sistema aprovechar las fortalezas tanto de un modelo grande de propósito general como de un modelo especializado más pequeño. El modelo grande se utiliza para generar esquemas de prueba de alto nivel, mientras que el modelo más pequeño se utiliza para completar los detalles y completar la prueba formal.
Sintetizando datos de razonamiento formal: Un camino natural
Esta arquitectura meticulosamente diseñada establece eficazmente un camino natural e intuitivo para sintetizar datos de razonamiento formal, fusionando a la perfección el razonamiento matemático de alto nivel con los requisitos estrictos y rigurosos de la verificación formal. Esta integración es esencial para asegurar la fiabilidad y la confiabilidad de los resultados del sistema.
"Curamos un subconjunto de problemas desafiantes que permanecen sin resolver por el modelo de demostrador de 7B de manera integral, pero para los cuales todos los subobjetivos descompuestos se han resuelto con éxito. Al componer las pruebas de todos los subobjetivos, construimos una prueba completa y formal para el problema original", explicaron los investigadores.
Este enfoque permite al sistema aprender de sus errores y mejorar su capacidad para resolver problemas complejos. Al identificar los subobjetivos específicos que están causando dificultades, el sistema puede enfocar sus esfuerzos en mejorar su rendimiento en esas áreas.
Preocupaciones y desafíos: Detalles de implementación bajo escrutinio
A pesar de los innegables logros técnicos demostrados por DeepSeek-Prover-V2, algunos expertos en el campo han planteado preocupaciones pertinentes con respecto a ciertos detalles de implementación. Elliot Glazer, un respetado matemático principal de Epoch AI, ha señalado posibles problemas que ameritan una mayor investigación.
Some concerns about the DeepSeek-Prover-V2 paper. Potentially misformalized examples, and discussion on the Lean zulip suggests the PutnamBench proofs are nonsense and use an implicit sorry (possibly hidden in the apply? tactic) not reported in their read-eval-print-loop.
Estas preocupaciones resaltan vívidamente los desafíos continuos inherentes al espacio de verificación formal, donde incluso los detalles de implementación más minuciosos y aparentemente insignificantes pueden ejercer un impacto desproporcionadamente grande en la validez y confiabilidad general de los resultados. El proceso de verificación formal exige una atención inquebrantable al detalle y una adhesión meticulosa a los estándares establecidos.
El potencial de ejemplos mal formalizados y la posibilidad de tácticas “sorry” ocultas en las pruebas de PutnamBench plantean preguntas importantes sobre el rigor y la integridad del proceso de verificación. Estas preocupaciones subrayan la necesidad de un escrutinio continuo y una verificación independiente de los resultados.
Disponibilidad y recursos: Democratización del acceso a la demostración formal de teoremas
DeepSeek ha puesto a disposición su Prover-V2 en dos tamaños de modelo distintos, que se adaptan a una diversa gama de recursos computacionales y objetivos de investigación. La primera versión es un modelo de 7B parámetros construido sobre su anterior Prover-V1.5-Base, que presenta una longitud de contexto extendida de hasta 32K tokens. La segunda versión es un modelo significativamente más grande de 671B parámetros entrenado en DeepSeek-V3-Base. Ambos modelos ahora son fácilmente accesibles en HuggingFace, una plataforma líder para compartir y colaborar en modelos de aprendizaje automático.
Además de los modelos en sí, DeepSeek también ha puesto a disposición en HuggingFace el conjunto de datos completo de ProverBench, que contiene 325 problemas formalizados meticulosamente con fines de evaluación. Este conjunto de datos integral proporciona a los investigadores y desarrolladores un recurso valioso para evaluar el rendimiento de sus modelos y compararlos con DeepSeek-Prover-V2.
Al poner estos recursos a disposición de forma gratuita, DeepSeek está democratizando el acceso a la tecnología de demostración formal de teoremas y fomentando la colaboración dentro de la comunidad investigadora. Es probable que este enfoque de código abierto acelere el progreso en el campo y conduzca a nuevos avances en el razonamiento y la verificación automatizados.
Este lanzamiento empodera a los investigadores y desarrolladores con los recursos necesarios para profundizar en las capacidades y limitaciones de esta tecnología. Al proporcionar acceso abierto a los modelos y al conjunto de datos de ProverBench, DeepSeek fomenta una mayor exploración y esfuerzos colaborativos para abordar las preocupaciones planteadas por los expertos en el campo. Este enfoque colaborativo tiene la clave para desentrañar las complejidades de la demostración formal de teoremas y solidificar la confiabilidad de estos avances innovadores.