IA y Pruebas Matemáticas: Un Nuevo Enfoque

Escribir pruebas matemáticas formales puede ser tan complicado como intentar doblar una sábana ajustada. Ya seas humano o computadora, puede parecer un rompecabezas interminable. Recientemente, algunas personas inteligentes pensaron: "Oye, ¿por qué no usamos IA para echarnos una mano?" Miraron un tipo especial de problemas matemáticos llamados problemas IMO de la Olimpiada Internacional de Matemáticas.

Ahora, estos problemas matemáticos van desde moderados hasta auténticos quebraderos de cabeza. Ya sabes, esos problemas que te hacen rascarte la cabeza y preguntarte si sabes sumar. El equipo quería escribir Pruebas Formales usando una herramienta llamada Lean, que es un lenguaje de programación para pruebas matemáticas. Su objetivo era abordar algunos de estos problemas complicados con IA, y lo que encontraron fue bastante fascinante.

#El desafío de las pruebas matemáticas

A los humanos les cuesta un montón escribir pruebas matemáticas formales, y las computadoras tampoco son unas genios en eso. Incluso algunos de los modelos de IA más avanzados tienen sus dificultades. El conjunto de datos miniF2F, que se usa a menudo como referencia para la demostración automatizada de teoremas, contiene 20 problemas IMO, pero más de la mitad no tiene pruebas formales. Entonces, ¿por qué es tan importante? Bueno, cuando una computadora dice que puede resolver un problema pero no tiene una prueba adecuada que lo respalde, es como afirmar que eres un cocinero increíble pero solo calientas pizzas congeladas.

Muchos modelos de IA, como GPT-4, tienen problemas para probar estos problemas matemáticos correctamente. A veces pueden tener suerte, pero cuando se trata de los problemas más difíciles, es como ver a un niño pequeño intentando atarse los zapatos: mucho esfuerzo, pero poco éxito.

#Ampliando el pool de pruebas

Para ayudar a generar más pruebas formales, el equipo se propuso escribir pruebas originales para 13 de los 20 problemas IMO del conjunto de datos miniF2F, además de algunos extras de años más recientes. ¡Eso es un total de 5,150 líneas de prueba, incluso más largo que algunas novelas! Este enorme esfuerzo facilita a los futuros investigadores aprender y experimentar con estos problemas.

No se detuvieron ahí. También desglosaron estas pruebas en piezas más pequeñas, llamadas lemmas. Piensa en estos lemmas como las piezas fundamentales de las pruebas matemáticas. El equipo creó alrededor de 900 lemmas con unas 25,500 líneas de código Lean. ¡Ahora eso son un montón de bloques de matemáticas! Estos lemmas son más fáciles de manejar y brindan un camino más claro para que los modelos de IA aprendan.

#Evaluando las habilidades de escritura de pruebas de la IA

Después de generar estos lemmas, el equipo decidió probar las habilidades de escritura de pruebas de GPT-4 con ellos. Spoiler: no salió tan bien como esperaban. La IA tuvo dificultades para escribir pruebas correctas, lo cual fue sorprendente dado todo el tecnología sofisticada detrás de ella. Usaron varias técnicas de prompts, incluyendo Zero-Shot prompting (pidiéndole que simplemente lo intentara) y Chain-of-Thought reasoning (guiándola paso a paso). Pero aun así, el robot no brilló.

Lo que fue aún más interesante fue que GPT-4 se desempeñó mejor en problemas IMO más antiguos en comparación con los más nuevos. Los problemas más antiguos parecían ser un poco más amigables, como un día de verano tranquilo, mientras que los más nuevos eran más como una noche tormentosa: desafiantes y difíciles de navegar.

#Por qué la IA necesita datos de alta calidad

Los modelos de aprendizaje automático, como una persona hambrienta, necesitan datos de alta calidad para prosperar. Cuantos más buenos datos les des, mejor rinden. El éxito de muchos sistemas de aprendizaje automático a menudo se puede rastrear hasta una abundancia de datos de entrenamiento de calidad. Por ejemplo, ImageNet ha jugado un papel clave en la visión por computadora. Pero cuando se trata de matemáticas, los recursos disponibles son bastante escasos.

El conjunto de datos miniF2F no tiene suficientes pruebas de calidad para muchos de sus problemas. La mayoría de los modelos de IA fallan porque carecen de ejemplos sólidos de los cuales aprender. Es como intentar aprender a andar en bicicleta sin haber visto nunca a nadie hacerlo primero. Cuando un modelo intenta resolver un problema matemático y falla, es difícil saber dónde salió mal ya que no hay un buen punto de referencia.

#La Olimpiada Matemática: un duro desafío

La Olimpiada Internacional de Matemáticas presenta un desafío único. Los problemas se revelan solo el día del examen, y cada año se vuelven más difíciles. Así que si un modelo de IA quiere hacerse notar, tiene que ser ágil y capaz de manejar lo desconocido. Usar problemas pasados como práctica no es suficiente porque cada año, los estudiantes enfrentan nuevos desafíos que son intencionalmente complicados.

Para preparar a una IA para la Olimpiada Matemática, los investigadores tienen que usar métodos de evaluación rigurosos. Necesitan verificar si la IA puede generalizar su aprendizaje cuando se enfrenta a un nuevo conjunto de problemas más difíciles. Si estás tratando de ganar una medalla de oro y solo has practicado con cosas fáciles, podrías irte con las manos vacías.

#Estado actual de los conjuntos de datos matemáticos

El conjunto de datos miniF2F consiste en varios teoremas matemáticos que se utilizan para evaluar a los estudiantes. Entre los 244 teoremas, 20 son de la IMO, y su dificultad varía significativamente. Algunos requieren prueba en una sola línea, mientras que otros necesitan cientos de líneas. Tener éxito en los problemas más fáciles no garantiza el éxito en los más difíciles. Así que, si un modelo dice ser bueno, es esencial mirar más allá de los simples porcentajes.

El actual campeón de este conjunto de datos, LEGO-Prover, solo logró demostrar uno de los problemas IMO. Mientras tanto, métodos como HTPS pueden manejar más problemas, pero a menudo enfrentan problemas con declaraciones que están simplificadas o mal redactadas. Es como decir que puedes ganar una carrera solo porque lograste terminar un trote corto.

#Un nuevo enfoque para descomponer pruebas

El equipo se dio cuenta de que para muchos problemas, no había pruebas formales disponibles al público. Así que abordaron estos problemas complicados y compartieron sus pruebas formales en Lean. Desglosaron cada prueba en lemmas más pequeños. Este proceso hizo que los desafíos complejos fueran más manejables, permitiendo que otros los estudiaran y aprendieran de ellos.

Los lemmas varían en dificultad y cubren una variedad de temas. Mientras algunos son simples y directos, otros requieren un pensamiento más profundo. Incluso evitaron problemas fáciles que Lean podría probar automáticamente. En lugar de eso, se enfocaron en desafíos reales donde las mentes-humanas o de IA-tendrían que estar comprometidas.

#Probando GPT-4: esperando mejoras

Para ver si GPT-4 podría mejorar, el equipo le pidió que escribiera pruebas formales para sus lemmas. Proporcionaron instrucciones detalladas y revisaron las pruebas informales de GPT-4 junto con las formales. Sorprendentemente, incluso después de extensos prompts y retroalimentación, GPT-4 tuvo problemas con la precisión. Fue como decirle a alguien repetidamente cómo hacer un sándwich, y aún así terminan sirviéndote una ensalada.

En la mayoría de los casos, GPT-4 simplemente no pudo proporcionar las respuestas correctas. El equipo le dio retroalimentación y le pidió que corrigiera errores, pero se sintió como intentar enseñarle a un gato a traer cosas. Interactuaron con GPT-4 varias veces, pero después de diez rondas, decidieron cortar por lo sano.

#Un vistazo más cercano a los lemmas

Cada uno de los lemmas en el nuevo conjunto de datos tiene una prueba formal en Lean, lo que es crucial para cualquiera que quiera aprender sobre estos problemas. El equipo construyó 907 lemmas con niveles de dificultad que van desde fácil hasta complejo. Estos bloques de construcción son esenciales para cualquiera que busque entender mejor la escritura de pruebas, ya que proporcionan un camino para abordar problemas matemáticos más intrincados.

Por ejemplo, algunos lemmas son relativamente sencillos, implicando probar propiedades básicas de los números. Otros retan al solucionador a pensar críticamente sobre funciones y relaciones entre números. Muchos siguen siendo difíciles, incluso cuando están desglosados, pero esa es la belleza de las matemáticas: siempre hay algo nuevo que aprender.

#Haciendo las pruebas accesibles

Las pruebas formales creadas por el equipo fueron compartidas con la comunidad para ayudar a todos a entender el trabajo que se requiere para escribir una prueba formal. También pueden ayudar a identificar errores en pruebas informales que circulan en línea. El objetivo del equipo es mostrar cuán beneficiosas y detalladas pueden ser las pruebas formales, especialmente cuando se trata de temas más complicados.

Al hacer estas pruebas disponibles, están contribuyendo a una comprensión más amplia de las matemáticas. Los no matemáticos pueden ver el esfuerzo involucrado en las pruebas formales, y los matemáticos pueden utilizarlas para refinar sus enfoques informales.

#Puntos clave

El proyecto ayuda a arrojar luz sobre las dificultades de formalizar pruebas y enfatiza la importancia de contar con datos de alta calidad en el entrenamiento de modelos de IA. A pesar de que GPT-4 tuvo un rendimiento significativamente pobre, este trabajo ha sentado las bases para futuros avances.

El equipo espera que, al proporcionar una gran cantidad de pruebas formales y trabajar a través de los lemmas, puedan fomentar más éxitos en el área de la demostración automatizada de teoremas. Ven esto como un paso adelante en el largo camino hacia la construcción de IA capaz de abordar problemas matemáticos de alto nivel como los que se encuentran en la Olimpiada Matemática.

#Explorando direcciones futuras

Aunque el equipo enfrentó desafíos con GPT-4, se mantienen optimistas. Su objetivo de desarrollar un modelo que pueda probar eficazmente los lemmas en su conjunto de datos sigue vivo. Cada intento, incluso si no es perfecto, sirve para informar el futuro de la IA en matemáticas.

El proyecto también abre vías para modelos de IA más robustos que puedan entender pruebas complejas y conectar ideas de maneras nuevas. No hay escasez de desafíos en el mundo de las matemáticas, y la IA puede desempeñar un papel crítico en llevar esos límites aún más lejos.

#Conclusión

En resumen, el esfuerzo por escribir pruebas formales para problemas IMO usando Lean ofrece un gran potencial para futuros trabajos en la demostración automatizada de teoremas. Aunque el camino es complicado y está lleno de obstáculos inesperados, cada paso que se da nos acerca a una comprensión más profunda de cómo la IA puede ayudar en el mundo de las matemáticas.

A medida que los investigadores continúan refinando sus métodos y mejorando las capacidades de los modelos, pronto podríamos ver sistemas de IA que puedan abordar de manera efectiva los desafiantes problemas planteados en las competencias matemáticas, o al menos acercarse lo suficiente para no avergonzarse frente a la comunidad matemática. ¿Quién sabe? Un día, podríamos tener una IA que pueda sobresalir en la Olimpiada Matemática, pero hasta entonces, solo tendremos que seguir practicando esas pruebas, un Lema a la vez.