La IA alcanza la medalla de plata en la Olimpiada de Matemáticas de este año
Durante la Olimpiada Internacional de Matemáticas de 2024, Google DeepMind presentó un programa de IA que puede generar pruebas matemáticas complejas
Mientras París se preparaba para acoger los 33º Juegos Olímpicos, más de 600 estudiantes de casi 110 países se reunieron en la idílica ciudad inglesa de Bath en julio para la Olimpiada Internacional de Matemáticas (OIM). Tuvieron dos sesiones de cuatro horas y media cada una para resolver seis problemas de varias disciplinas matemáticas. La estudiante china Haojia Shi se llevó el primer puesto en la clasificación individual con una puntuación perfecta. Clasificación por países: el equipo de Estados Unidos quedó en primer lugarSin embargo, los resultados más destacados del evento fueron los obtenidos por dos máquinas de Google DeepMind que participaron en la competición. Los programas de inteligencia artificial de DeepMind fueron capaces de resolver un total de cuatro de seis problemas, lo que correspondería al nivel de un medallista de plata. Los dos programas obtuvieron 28 de los 42 puntos posibles. Sólo unos 60 estudiantes obtuvieron mejores resultadosescribió el matemático y medallista Fields Timothy Gowers, medallista de oro anterior en la competencia, en un hilo en X (anteriormente Twitter).
Para lograr este impresionante resultado, el equipo de DeepMind utilizó dos programas de IA diferentes: AlphaProof y AlphaGeometry 2. obras anteriores de manera similar Los algoritmos que dominan el ajedrez, el shogi y el Go utilizan el denominado aprendizaje por refuerzo para competir contra sí mismo una y otra vez y mejorar paso a paso. Este método se puede implementar con bastante facilidad en los juegos de mesa. La IA ejecuta varias jugadas; si no dan como resultado una victoria, es penalizada y aprende a aplicar otras estrategias.
Sin embargo, para hacer lo mismo con los problemas matemáticos, un programa debe ser capaz no solo de comprobar que ha resuelto el problema, sino también de verificar que los pasos de razonamiento que siguió para llegar a la solución fueron correctos. Para lograr esto, AlphaProof utiliza los llamados asistentes de prueba, algoritmos que repasan un argumento lógico paso a paso para comprobar si las respuestas a los problemas planteados son correctas. Aunque los asistentes de prueba existen desde hace varias décadas, su uso en el aprendizaje automático se ha visto limitado por la cantidad muy limitada de datos matemáticos disponibles en un lenguaje formal, como Lean, que la computadora puede entender.
Sobre el apoyo al periodismo científico
Si le gusta este artículo, considere apoyar nuestro periodismo galardonado suscribiéndoseAl comprar una suscripción, usted contribuye a garantizar el futuro de historias impactantes sobre los descubrimientos e ideas que dan forma a nuestro mundo actual.
Por otro lado, las soluciones a los problemas matemáticos escritos en lenguaje natural están disponibles en abundancia. Existen numerosos problemas en Internet que los humanos han resuelto paso a paso. Por ello, el equipo de DeepMind entrenó un gran modelo de lenguaje llamado Gemini para traducir un millón de problemas de este tipo al lenguaje de programación Lean, de modo que el asistente de pruebas pudiera usarlos para entrenar. “Cuando se le presenta un problema, AlphaProof genera candidatos a soluciones y luego los prueba o refuta buscando posibles pasos de prueba en Lean”, dice el autor. Los desarrolladores escribieron en el sitio web de DeepMindAl hacerlo, AlphaProof aprende gradualmente qué pasos de prueba son útiles y cuáles no, mejorando su capacidad para resolver problemas más complejos.
Los problemas de geometría, que también aparecen en la OMI, requieren normalmente un enfoque completamente diferente. En enero, DeepMind presentó una IA llamada AlphaGeometry que puede resolver con éxito este tipo de problemas. Para ello, los expertos generaron primero un gran conjunto de “premisas” geométricas, o puntos de partida: por ejemplo, un triángulo con las alturas dibujadas y los puntos marcados a lo largo de los lados. A continuación, los investigadores utilizaron lo que se llama un “motor de deducción” para inferir otras propiedades del triángulo, como qué ángulos coinciden y qué líneas son perpendiculares entre sí. Al combinar estos diagramas con las propiedades derivadas, los expertos crearon un conjunto de datos de entrenamiento compuesto por teoremas y sus correspondientes demostraciones. Este procedimiento se combinó con un gran modelo de lenguaje que a veces también utiliza lo que se conoce como construcciones auxiliares; el modelo puede agregar otro punto a un triángulo para convertirlo en cuadrilátero, lo que puede ayudar a resolver un problema. El equipo de DeepMind ahora ha presentado una versión mejorada, llamada AlphaGeometry 2, entrenando el modelo con aún más datos y acelerando el algoritmo.
Para probar sus programas, los investigadores de DeepMind hicieron que los dos sistemas de IA compitieran en la Olimpiada de Matemáticas de este año. El equipo primero tuvo que traducir manualmente los problemas a Lean. AlphaGeometry 2 logró Resuelve el problema de geometría correctamente en solo 19 segundosMientras tanto, AlphaProof fue capaz de resolver un problema de teoría de números y dos de álgebra, incluido uno que sólo cinco de los participantes humanos pudieron resolver. Sin embargo, la IA no logró resolver los problemas combinatorios, lo que podría deberse a que estos problemas son muy difíciles de traducir a lenguajes de programación como Lean.
El rendimiento de AlphaProof fue lentorequiriendo más de 60 horas para completar algunos de los problemas, significativamente más tiempo que las nueve horas totales que se les asignaron a los estudiantes. “Si a los competidores humanos se les hubiera permitido ese tipo de tiempo por problema, sin duda habrían obtenido una puntuación más alta”, escribió Gowers en X. “Sin embargo, (i) esto está muy por encima de lo que los demostradores automáticos de teoremas podían hacer antes, y (ii) es probable que estos tiempos disminuyan a medida que se obtengan ganancias de eficiencia”.
Gowers y el matemático Joseph K. Myers, otro ganador anterior de la medalla de oro, evaluaron las soluciones de los dos sistemas de IA utilizando los mismos criterios que se utilizaron para los participantes humanos. Según estos estándares, los programas obtuvieron una impresionante puntuación de 28 puntos, lo que corresponde a una medalla de plata. Esto significa que la IA se quedó a las puertas de alcanzar el nivel de rendimiento de la medalla de oro, que se otorga por una puntuación de 29 puntos o más.
En X, Gowers enfatizó que los programas de IA han sido entrenados con una gama bastante amplia de problemas y que estos métodos no se limitan a las Olimpíadas Matemáticas. “Podríamos estar cerca de tener un programa que permita a los matemáticos Obtenga respuestas a una amplia gama de preguntas“, explicó. “¿Estamos cerca del punto en que los matemáticos sean redundantes? Es difícil decirlo”.
Este artículo apareció originalmente en Espectro de la ciencia y fue reproducido con permiso.