DeepMind alcanza hito en la solución de problemas matemáticos: el próximo gran desafío para la IA

Después de que Google Deepmind derrotó a las personas en todo, desde Juego Vaya a los juegos de mesa de estrategia ,
Ahora afirma estar a punto de vencer a los mejores estudiantes del mundo al resolver tareas de matemáticas.

El La compañía de aprendizaje automático anunció el 25 de julio que sus sistemas de inteligencia artificial (KI) han resuelto cuatro de las seis tareas que se les dieron a los estudiantes de las Olímpicas Internacionales de Matemáticas (IMO) 2024 en Bath, Gran Bretaña. La IA proporcionó evidencia rigurosa y gradual, que fueron evaluadas por dos matemáticas superiores y lograron una puntuación de 28/42 solo un punto del área de medallas de oro.

"Obviamente es un progreso muy importante", dice Joseph Myers, un matemático de Cambridge, Gran Bretaña, quien, junto con el medallista de los campos Tim Gowers, verificó las soluciones y ayudó a seleccionar los problemas originales para este año.

DeepMind y otras compañías están en la carrera para proporcionar evidencia de máquinas, el esencial Resolver preguntas de investigación en matemáticas . Los problemas con la OMI, la competencia líder mundial por los jóvenes matemáticos, se han convertido en un criterio para el progreso en la dirección de este objetivo y son vistos como un "gran desafío" para el aprendizaje automático, según la compañía.

"Esta es la primera vez que un sistema de IA pudo lograr servicios a nivel de medalla", dijo Pushmeet Kohli, vicepresidente de IA en ciencias de Deepmind, en una consulta de prensa. "Este es un hito importante en el camino para desarrollar evidencia progresiva", dijo Kohli.

extensión

Hace solo unos meses, en enero, el sistema DeepMind Servicios de alfageometría a nivel de medallas Al resolver un tipo de problemas de IMO, a saber, aquellos en la geometría euclideana. La primera IA que funciona a un nivel de medalla de oro para las preguntas generales que incluyen en la prueba en álgebra, combinatoria y teoría de números, que generalmente se consideran más exigentes que la geometría, tiene derecho a obtener un precio de $ 5 millones, el Premio Olimpiado de Matemáticas de IA (Auto). (El precio tiene criterios estrictos, como la divulgación del código fuente y el trabajo con potencia informática limitada, lo que significa que los esfuerzos actuales de DeepMind no calificarían.)

En su último intento, los investigadores usaron 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 discos, dice el especialista en computación de DeepMind Thang Luong.

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 en la teoría de números, para los cuales tomó tres días. (Los participantes de la OMI real tienen dos sesiones de 4.5 horas cada una). No pudo resolver los dos problemas en la combinación, otra área de matemáticas.

Los investigadores han logrado resultados mixtos cuando responden preguntas matemáticas con modelos de voz, el tipo de sistema que impulsa chatbots como Chatt. A veces los modelos dan la respuesta correcta, pero no pueden explicar su razonamiento racionalmente, y a veces

Solo la semana pasada, un equipo de compañías de software Numina y Huggingface utilizaron un modelo de voz para ganar un "precio de progreso" de AMIO intermedio basado en versiones simplificadas de problemas de OMI. Las compañías pusieron todo su código abierto de sistemas y lo pusieron a disposición para descargar otros investigadores. Pero los ganadores dijeron que Naturaleza que los modelos de idiomas por sí solos probablemente no serían suficientes para resolver problemas difíciles.

solo clase

Alphaproof combina un modelo de voz con la tecnología de refuerzo del aprendizaje, que el motor "Alphazero" para juegos de ataque como GO y algunos Problemas matemáticos específicos . Con el aumento del aprendizaje, una red neuronal aprende a través de experimentos y errores. Esto funciona bien si sus respuestas se pueden evaluar utilizando una escala objetiva. Para este propósito, Alphaproof fue capacitado para leer y escribir evidencia en un lenguaje formal llamado Lean, que se utiliza en el paquete de software 'Proof Assistant' del mismo nombre que es popular entre los matemáticos. Para esto, Alphaproof probó si sus gastos fueron correctos al hacerlo en el paquete Lean, lo que ayudó a completar algunos de los pasos del código.

El entrenamiento de un modelo de voz requiere cantidades masivas de datos, pero solo unas pocas pruebas matemáticas estaban disponibles en Lean. Para superar este problema, el equipo desarrolló una red adicional que intentó traducir una grabación existente de un millón de problemas que se escribieron en lenguaje natural, pero sin traducir soluciones escritas en Lean, dice Thomas Hubert, un investigador de alumno de máquina de profundidad que realizó el desarrollo de Alphaproof. "¿Podemos aprender a probar nuestro enfoque, incluso si no hemos entrenado originalmente en evidencia escrita por humanos?" (La compañía era similar a la marcha, donde su IA aprendió a jugar el juego jugando contra sí misma, en lugar de la forma en que la gente lo hace).

clave mágica

Muchas de las traducciones Lean no tenían sentido, pero lo suficiente eran lo suficientemente buenos como para llevar el Alphaproof al punto en que podría comenzar sus ciclos de aprendizaje crecientes. Los resultados fueron mucho mejores de lo esperado, dijo Gowers en la consulta de prensa. "Muchos problemas con la OMI tienen esta propiedad de la clave mágica. El problema primero parece difícil hasta que encuentre una clave mágica que la abre", dijo Gowers, que trabaja en el Collège de France en París.

En algunos casos, Alphaproof parecía poder dar este paso adicional de creatividad dándole un paso correcto de una solución infinitamente grande posible. Pero se requiere un análisis adicional para determinar si las respuestas fueron menos sorprendentes de lo que parecían, agregó Gowers. Un discurso similar surgió después del sorprendente 'Zug 37' , Deepminds Alphago-Bot at His Victoria famosa en 2016 sobre el mejor jugador humano del mundo -Un punto de inflexión para el KI.

Queda por ver si las técnicas pueden perfeccionarse para trabajar a un nivel de investigación en matemáticas, dijo Myers en la revisión de la prensa. "¿Puede expandirse a otros tipos de matemáticas donde no se pueden capacitar millones de problemas?"

"Hemos llegado al punto en el que no solo se puede probar problemas de investigación abiertos, sino también problemas que son muy desafiantes para los mejores jóvenes matemáticos del mundo", dijo el especialista en informática de Deepmind, David Silver, quien fue el investigador líder en el desarrollo de Alphago a mediados de 2010.