Después de que Google DeepMind derrotara a los humanos en todo, desde Jugar Ir a juegos de mesa de estrategia,
ahora afirma estar a punto de vencer a los mejores estudiantes del mundo en la resolución de problemas matemáticos.
El con sede en Londres Aprendizaje automático La compañía anunció el 25 de julio que sus sistemas de inteligencia artificial (IA) resolvieron cuatro de los seis problemas planteados a los estudiantes en la Olimpiada Internacional de Matemáticas (OMI) de 2024 en Bath, Reino Unido. La IA proporcionó pruebas rigurosas paso a paso evaluadas por dos destacados matemáticos y obtuvo una puntuación de 28/42, a sólo un punto del territorio de la medalla de oro.
"Obviamente es un avance muy significativo", dice Joseph Myers, un matemático de Cambridge, Reino Unido, quien, junto con el medallista Fields Tim Gowers, revisó las soluciones y ayudó a seleccionar los problemas originales para la OMI de este año.
DeepMind y otras empresas están en la carrera para, en última instancia, proporcionar a las máquinas pruebas importantes. Resolver preguntas de investigación en matemáticas.. Los problemas presentados en la OMI, la principal competencia mundial para jóvenes matemáticos, se han convertido en un punto de referencia para el progreso hacia ese objetivo y se consideran un "gran desafío" para el aprendizaje automático, dijo la compañía.
"Esta es la primera vez que un sistema de IA logra un rendimiento de nivel de medalla", dijo Pushmeet Kohli, vicepresidente de IA en ciencia de DeepMind, en una rueda de prensa. "Este es un hito importante en la creación de investigadores de pruebas avanzadas", dijo Kohli.
Extensión
Hace apenas unos meses, en enero, el sistema DeepMind Logros de nivel de medalla AlphaGeometry logrado al resolver un tipo de problemas de la OMI, a saber, los de geometría euclidiana. La primera IA que alcance el nivel de medalla de oro en la prueba general, incluidas preguntas de álgebra, combinatoria y teoría de números, generalmente consideradas más desafiantes que la geometría, será elegible para recibir un premio de 5 millones de dólares, el Premio Olimpiada de Matemáticas de IA (AIMO). (El premio tiene criterios estrictos, como revelar el código fuente y trabajar con potencia informática limitada, lo que significa que los esfuerzos actuales de DeepMind no calificarían).
En su último intento, los investigadores utilizaron AlphaGeometry2 para resolver el problema de geometría en menos de 20 segundos; La IA es una versión mejorada y más rápida de su sistema de registro, afirma Thang Luong, especialista en informática de DeepMind.
Para los otros tipos de preguntas, el equipo desarrolló un sistema completamente nuevo llamado AlphaProof. AlphaProof resolvió dos problemas de álgebra en la competencia y uno de teoría de números, lo que llevó tres días. (Los participantes en el IMO real tienen dos sesiones de 4,5 horas cada una). No pudo resolver los dos problemas de combinatoria, otra área de las matemáticas.

Los investigadores han obtenido resultados mixtos al responder preguntas matemáticas utilizando modelos de lenguaje, el tipo de sistemas que impulsan los chatbots como ChatGPT. A veces los modelos dan la respuesta correcta pero no pueden explicar su razonamiento racionalmente y, a veces, dicen tonterías.
La semana pasada, un equipo de investigadores de las empresas de software Numina y HuggingFace utilizaron un modelo de lenguaje para ganar un 'premio al progreso' intermedio de AMIO basado en versiones simplificadas de problemas de IMO. Las empresas han hecho que todos sus sistemas sean de código abierto y los hayan puesto a disposición de otros investigadores para que los descarguen. Pero los ganadores dijeronNaturaleza, que los modelos de lenguaje por sí solos probablemente no serían suficientes para resolver problemas más difíciles.
solo clase
AlphaProof combina un modelo de lenguaje con tecnología de aprendizaje por refuerzo que utiliza el motor “AlphaZero” que la empresa ha utilizado con éxito para juegos de ataque como Go y algunos problemas matemáticos específicos usado. En el aprendizaje por refuerzo, una red neuronal aprende mediante prueba y error. Esto funciona bien cuando sus respuestas pueden evaluarse utilizando un estándar objetivo. Con este fin, AlphaProof recibió capacitación para leer y escribir pruebas en un lenguaje formal llamado Lean, que se utiliza en el paquete de software 'Proof Assistant' del mismo nombre, popular entre los matemáticos. Para hacer esto, AlphaProof probó si sus resultados eran correctos ejecutándolos en el paquete Lean, lo que ayudó a completar algunos de los pasos del código.
Entrenar un modelo de lenguaje requiere cantidades masivas de datos, pero había pocas pruebas matemáticas disponibles en Lean. Para superar este problema, el equipo desarrolló una red adicional que intentó traducir un registro existente de un millón de problemas escritos en lenguaje natural pero sin soluciones escritas por humanos a Lean, dice Thomas Hubert, un investigador de aprendizaje automático de DeepMind que codirigió el desarrollo de AlphaProof. "Nuestro enfoque fue: ¿podemos aprender a demostrar incluso si originalmente no nos entrenamos con pruebas escritas por humanos?" (La compañía adoptó un enfoque similar con Go, donde su IA aprendió a jugar jugando contra sí misma en lugar de hacerlo de la forma en que lo hacen los humanos).
llaves magicas
Muchas de las traducciones Lean no tenían sentido, pero suficientes fueron lo suficientemente buenas como para que AlphaProof llegara al punto en el que pudiera comenzar sus ciclos de aprendizaje por refuerzo. Los resultados fueron mucho mejores de lo esperado, dijo Gowers en la rueda de prensa. "Muchos problemas en la OMI tienen esta propiedad de llave mágica. El problema parece difícil al principio hasta que encuentras una llave mágica que lo abre", dijo Gowers, que trabaja en el Collège de France en París.
En algunos casos, AlphaProof parecía poder brindar ese paso adicional de creatividad al brindar un paso correcto a partir de una solución posible infinitamente grande. Pero se necesitan más análisis para determinar si las respuestas fueron menos sorprendentes de lo que parecían, añadió Gowers. Un discurso similar surgió tras el sorprendente 'Tren 37', el robot DeepMinds AlphaGo en su famosa victoria de 2016 sobre el mejor jugador humano de Go del mundo hecho: un punto de inflexión para la IA.
Queda por ver si las técnicas pueden perfeccionarse para funcionar a nivel de investigación en matemáticas, dijo Myers en la rueda de prensa. "¿Puede expandirse a otros tipos de matemáticas que tal vez no tengan millones de problemas entrenados?"
"Estamos en el punto en el que pueden demostrar no sólo problemas de investigación abiertos, sino también problemas que son muy desafiantes para los mejores matemáticos jóvenes del mundo", dijo el especialista en informática de DeepMind, David Silver, quien fue el investigador principal que desarrolló AlphaGo a mediados de la década de 2010.