La demostración de teoremas en matemáticas se enfrenta a desafíos cada vez mayores debido a la creciente complejidad de las pruebas. Los sistemas formalizados como Lean, Isabelle y Coq ofrecen pruebas verificables por computadora, pero su creación exige un esfuerzo humano sustancial. Los modelos de lenguaje grandes (LLM) son prometedores para resolver problemas matemáticos de nivel secundario utilizando asistentes de prueba, pero su desempeño aún debe mejorar debido a la escasez de datos. Los lenguajes formales requieren una gran experiencia, lo que da como resultado corpus limitados. A diferencia de los lenguajes de programación convencionales, los lenguajes de prueba formal contienen información intermedia oculta, lo que hace que los corpus de lenguaje sin formato no sean adecuados para el entrenamiento. Esta escasez persiste a pesar de la existencia de valiosos corpus escritos por humanos. Los esfuerzos de autoformalización, si bien son útiles, no pueden sustituir por completo a los datos elaborados por humanos en calidad y diversidad.
Los intentos existentes para abordar los desafíos de la demostración de teoremas han evolucionado significativamente con los asistentes de prueba modernos como Coq, Isabelle y Lean que han expandido los sistemas formales más allá de la lógica de primer orden, aumentando el interés en la demostración automatizada de teoremas (ATP). La reciente integración de grandes modelos de lenguaje ha avanzado aún más en este campo. Los primeros enfoques de ATP usaban métodos tradicionales como KNN o GNN, y algunos empleaban aprendizaje de refuerzo. Los esfuerzos recientes utilizan métodos profundos basados en transformadores, tratando los teoremas como texto simple. Muchos sistemas basados en aprendizaje (por ejemplo, GPT-f, PACT, Llemma) entrenan modelos de lenguaje en pares (estado de prueba, próxima táctica) y usan la búsqueda de árbol para la demostración de teoremas. Los enfoques alternativos implican que los LLM generen pruebas completas de forma independiente o en función de pruebas proporcionadas por humanos. Las herramientas de extracción de datos son cruciales para ATP, ya que capturan estados intermedios invisibles en el código pero visibles durante el tiempo de ejecución. Existen herramientas para varios asistentes de prueba, pero las herramientas Lean 4 enfrentan desafíos en la extracción masiva en múltiples proyectos debido a las limitaciones de diseño de un solo proyecto. Algunos métodos también exploran la incorporación de pruebas informales en pruebas formales, ampliando el alcance de la investigación de ATP.
Investigadores de la Universidad China de Hong Kong proponen LEAN-GitHubun conjunto de datos Lean a gran escala que complementa el conjunto de datos Mathlib, que se utiliza con éxito. Este enfoque innovador proporciona repositorios Lean de código abierto en GitHub, lo que amplía significativamente los datos disponibles para entrenar modelos de demostración de teoremas. Los investigadores desarrollaron una canalización escalable para mejorar la eficiencia de extracción y el paralelismo, lo que permite la explotación de datos valiosos de un corpus Lean no compilado ni extraído previamente. Además, proporcionan una solución al problema de duplicación de estados común en los métodos de búsqueda a prueba de árboles.
El proceso de construcción del conjunto de datos LEAN-GitHub implicó varios pasos e innovaciones clave:
- Selección de repositorios: Los investigadores identificaron 237 repositorios Lean 4 (GitHub no diferencia entre Lean 3 y Lean 4) en GitHub, y calcularon aproximadamente 48 091 teoremas. Después de descartar 90 repositorios con versiones Lean 4 obsoletas, quedaron 147. Solo 61 de ellos pudieron compilarse sin modificaciones.
- Desafíos de compilación: el equipo desarrolló scripts automatizados para encontrar las versiones oficiales más cercanas para proyectos que utilizan versiones no oficiales de Lean 4. También abordaron el problema de los archivos aislados dentro de proyectos Lean vacíos.
- Compilación del código fuente: en lugar de utilizar la herramienta Lake, llamaron directamente al compilador Leanc. Este enfoque permitió compilar proyectos Lean no compatibles y archivos aislados, que Lake no podía manejar. Extendieron el gráfico de importación de Lake y crearon un script de compilación personalizado con mayor paralelismo.
- Proceso de extracción: Basándose en LeanDojo, el equipo implementó la extracción de datos para archivos aislados y reestructuró la implementación para aumentar el paralelismo. Este enfoque superó los cuellos de botella en la conexión de red y las redundancias computacionales.
- Resultados: De 8639 archivos fuente Lean, se extrajeron con éxito 6352 y 42 000 teoremas. El conjunto de datos final incluye 2133 archivos y 28 000 teoremas con información táctica válida.
El conjunto de datos LEAN-GitHub resultante es diverso y abarca varios campos matemáticos, como la lógica, la lógica de primer orden, la teoría de matroides y la aritmética. Contiene temas matemáticos de vanguardia, estructuras de datos y problemas de nivel olímpico. En comparación con los conjuntos de datos existentes, LEAN-GitHub ofrece una combinación única de contenido escrito por humanos, estados intermedios y diversos niveles de complejidad, lo que lo convierte en un recurso valioso para avanzar en la demostración automatizada de teoremas y las matemáticas formales.
InternLM2-StepProver, capacitado en el diverso conjunto de datos LEAN-GitHub, demuestra habilidades excepcionales de razonamiento formal en varios puntos de referencia. Logra un rendimiento de vanguardia en miniF2F (63,9 % en Valid, 54,5 % en Test), superando a los modelos anteriores. En ProofNet, alcanza una tasa de Pass@1 del 18,1 %, superando al líder anterior. Banco Putnamresuelve 5 problemas en una sola pasada, incluido el que no estaba resuelto anteriormente. Putnam 1988 B2. Estos resultados abarcan desde matemáticas de nivel secundario hasta nivel avanzado de pregrado, y muestran la versatilidad de InternLM2-StepProver y la eficacia del conjunto de datos LEAN-GitHub en el entrenamiento de modelos avanzados de demostración de teoremas.
LEAN-GitHub, un conjunto de datos a gran escala extraído de repositorios abiertos de Lean 4, contiene 28.597 teoremas y 218.866 tácticas. Este conjunto de datos diverso se utilizó para entrenar a InternLM2-StepProver, logrando un rendimiento de vanguardia en razonamiento formal de Lean 4. Los modelos entrenados en LEAN-GitHub demuestran un rendimiento mejorado en varios campos matemáticos y niveles de dificultad, lo que destaca la eficacia del conjunto de datos para mejorar las capacidades de razonamiento. Al publicar LEAN-GitHub como código abierto, los investigadores pretenden ayudar a la comunidad a utilizar mejor la información subexplotada en corpus sin procesar y avanzar en el razonamiento matemático. Esta contribución podría acelerar significativamente el progreso en la demostración automatizada de teoremas y las matemáticas formales.
Revisar la Papel y Conjunto de datos. Todo el crédito por esta investigación corresponde a los investigadores de este proyecto. Además, no olvides seguirnos en Gorjeo y ú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 Más de 47 000 suscriptores de ML en Reddit
Encuentra lo próximo Seminarios web sobre IA aquí
Asjad es consultor en prácticas en Marktechpost. Está cursando la licenciatura en ingeniería mecánica en el Instituto Indio de Tecnología de Kharagpur. Asjad es un entusiasta del aprendizaje automático y del aprendizaje profundo que siempre está investigando las aplicaciones del aprendizaje automático en el ámbito de la atención médica.