Un gran avance en el razonamiento matemático es el uso de lenguajes formales verificables por computadora, como Lean, para demostrar teoremas matemáticos. Estos lenguajes formales permiten verificar rigurosamente las pruebas, garantizando la precisión y la consistencia de los resultados matemáticos. El uso de modelos de lenguaje grande (LLM) entrenados en pruebas de lenguaje natural (NL) para producir pruebas formales integrales es un método prometedor para la demostración formal de teoremas.
Sin embargo, la falta de datos alineados de demostración de teoremas en lenguaje formal (FL) y NL frecuentemente dificulta que los LLM contemporáneos operen con máxima eficiencia. La falta de recursos disponibles impide el avance de enfoques y estrategias de capacitación eficientes para aprovechar al máximo el potencial de los LLM en la creación de pruebas matemáticas formales. Para superar estas limitaciones, un equipo de investigadores de la Universidad de Ciencia y Tecnología de Hong Kong y la Universidad de Illinois Urban-Champagin ha presentado TheoremLlama, un marco de trabajo de extremo a extremo creado para especializar un LLM de propósito general en la demostración de teoremas Lean4.
El teorema de Llama se compone de varias partes importantes, que son las siguientes.
- Generación de conjuntos de datos alineados con NL-FL: TheoremLlama presenta técnicas para crear un conjunto de datos alineado con NL-FL para superar la escasez de datos. Este conjunto de datos, llamado Open Bootstrapped Theorems (OBT), utiliza una técnica de bootstrapping para incluir pruebas de NL en el código Lean4. Al integrar el razonamiento de NL en los escenarios de Lean4, el marco mejora la comprensión y la ejecución del razonamiento formal por parte de los LLM.
- Capacitación formal para los probadores de teoremas de LLM: el sistema aplica nuevas estrategias de capacitación para ayudar a los LLM a convertirse en probadores de teoremas Lean4 exitosos. Se han utilizado métodos como la capacitación en bloques y la clasificación de datos del plan de estudios para mejorar el aprendizaje en contexto de los LLM y garantizar una capacitación confiable en el conjunto de datos OBT.
- Escritura de pruebas Lean4 para LLM: esta parte trata de mejorar la capacidad del LLM para escribir pruebas formales en Lean4 por sí solo. El LLM perfecciona sus habilidades de razonamiento formal de manera iterativa mediante el uso de pruebas generadas correctamente como ejemplos.
El enfoque de arranque NL-FL de TheoremLlama es una invención importante que permite un entrenamiento eficiente al coordinar el razonamiento en lenguaje natural con las restricciones del lenguaje matemático formal. La eficiencia del marco ha sido demostrada por hallazgos experimentales, que en los conjuntos de datos MiniF2F-Valid y Test, respectivamente, arrojaron precisiones acumuladas de 36,48% y 33,61%. Estos resultados superaron los hallazgos de referencia de GPT-4, que en los mismos conjuntos de datos arrojaron precisiones de 22,95% y 25,41%.
En conclusión, TheoremLlama es un paso importante hacia el uso de las capacidades de lenguaje natural de los LLM para formalizar la demostración de teoremas en Lean4, mejorar el razonamiento matemático y abordar problemas importantes con la alineación de datos y los enfoques de entrenamiento.
Revisar la Papel. Todo el crédito por esta investigación corresponde a los investigadores de este proyecto. Además, no olvides seguirnos en Gorjeo.
Únete a nuestro Canal de Telegram y LinkedIn Gr¡Arriba!.
Si te gusta nuestro trabajo, te encantará nuestro Boletin informativo..
No olvides unirte a nuestro Subreddit de más de 46 000 millones de usuarios
Tanya Malhotra es una estudiante de último año de la Universidad de Estudios de Petróleo y Energía, Dehradun, que cursa BTech en Ingeniería Informática con una especialización en Inteligencia Artificial y Aprendizaje Automático.
Es una entusiasta de la ciencia de datos con un buen pensamiento analítico y crítico, junto con un gran interés en adquirir nuevas habilidades, liderar grupos y gestionar el trabajo de manera organizada.