¿Pueden los LLMs generar pruebas matemáticas que puedan ser rigurosamente verificadas? Conoce LeanDojo un espacio de juego de inteligencia artificial de código abierto con herramientas, puntos de referencia y modelos para que los modelos de lenguaje grandes demuestren teoremas formales en el asistente de pruebas Lean.

Sí, los LLMs pueden generar pruebas matemáticas rigurosamente verificables a través de LeanDojo, un espacio de juego de inteligencia artificial de código abierto que proporciona herramientas, puntos de referencia y modelos para que los grandes modelos de lenguaje demuestren teoremas formales en el asistente de pruebas Lean.

La Inteligencia Artificial y el Aprendizaje Automático son los campos más populares en la actualidad. Con los enormes avances que se están realizando en IA, nuevas innovaciones están transformando la forma en que los seres humanos interactúan con las máquinas. El razonamiento en la inteligencia humana es una parte importante de la Inteligencia Artificial. Se han investigado diferentes enfoques para demostrar teoremas, como la demostración automática de teoremas (ATP), que es el proceso de producir automáticamente pruebas para teoremas formulados en lógica formal. Debido al enorme espacio de búsqueda, la demostración interactiva de teoremas (ITP) ha surgido como un paradigma alternativo en el que los expertos humanos interactúan con herramientas de software llamadas asistentes de prueba para construir pruebas.

Los modelos de lenguaje grandes (LLMs), que han demostrado notables capacidades de generación de código, también enfrentan dificultades en la demostración de teoremas debido a defectos en la factualidad y la alucinación. Para superar estas limitaciones, un equipo de investigadores de Caltech, NVIDIA, MIT, UC Santa Barbara y UT Austin ha presentado LeanDojo, que es un conjunto de herramientas de código abierto para la demostración de teoremas basada en LLM. LeanDojo se ha construido alrededor del asistente de prueba Lean, que es popular entre los matemáticos. Ofrece recursos para trabajar con Lean y extraer datos.

En la extracción de datos, se recopilan datos de entrenamiento a partir de árboles de prueba y estados de prueba intermedios que no son inmediatamente evidentes en el código Lean original. LeanDojo ha sido capaz de permitir que los modelos se comuniquen con Lean de forma programática. Esto les permite ver los estados de prueba, llevar a cabo acciones o tácticas de prueba y obtener retroalimentación de Lean. El entorno de prueba de Lean de código abierto se compone de numerosos elementos, incluidos conjuntos de herramientas, datos, modelos y puntos de referencia, para permitir la interacción programada con el entorno de prueba y extraer datos de Lean.

• Contextual AI presenta LENS un marco de inteligencia artificial para modelos de lenguaje con visión aumentada que supera a Flamingo en un 9% (56->65%) en VQAv2.
• Unity anuncia el lanzamiento de Muse una plataforma de juegos de texto a video que te permite crear texturas, sprites y animaciones con lenguaje natural.
• Conoce a FastSAM La solución revolucionaria en tiempo real que logra una segmentación de alto rendimiento con una carga computacional mínima.

LeanDojo proporciona anotaciones detalladas de premisas en las pruebas, lo cual es valioso para la selección de premisas, un cuello de botella crítico en la demostración de teoremas. Mediante el uso de las capacidades de extracción de datos de LeanDojo, los investigadores también han desarrollado ReProver, el primer demostrador basado en LLM mejorado con recuperación para seleccionar premisas de una gran biblioteca matemática. A diferencia de los métodos anteriores que dependían de conjuntos de datos privados que requerían recursos computacionales sustanciales, ReProver se ha diseñado para ser más accesible y rentable. Requiere menos potencia informática y puede ser entrenado con solo una GPU por semana.

La capacidad de análisis de programas de LeanDojo ha sido utilizada por el mecanismo de recuperación de ReProver para encontrar premisas accesibles y producir ejemplos concretos de posibles errores. Como resultado, el demostrador tiene un mejor rendimiento y el procedimiento de recuperación es más efectivo. Para la evaluación e investigación adicional, el equipo ha desarrollado un nuevo conjunto de datos de referencia que consta de 96,962 teoremas y pruebas extraídos de la biblioteca matemática de Lean. Este conjunto de datos de referencia presenta una división desafiante que requiere que el demostrador generalice a teoremas que dependen de premisas novedosas que no se utilizaron durante el entrenamiento. Los resultados experimentales han demostrado que ReProver tiene un buen rendimiento en comparación con las líneas de base sin recuperación y GPT-4 cuando se utiliza este conjunto de datos de referencia para el entrenamiento y la evaluación.

En conclusión, esta solución de código abierto para la demostración de teoremas basada en LLM parece prometedora para el futuro. Supera las barreras del código privado, los datos y los grandes requisitos informáticos al proporcionar conjuntos de herramientas, datos, modelos y puntos de referencia accesibles.

We will continue to update Zepes; if you have any questions or suggestions, please contact us!