noticias

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Informe del corazón de la máquina

Departamento editorial de Machine Heart

Con el modelo grande de Gemini y el algoritmo de aprendizaje por refuerzo AlphaZero, puede dominar la geometría, el álgebra y la teoría de números.

Para la IA, la Olimpíada de Matemáticas ya no es un problema.

El jueves, la inteligencia artificial de Google DeepMind completó una hazaña: usar IA para resolver la verdadera pregunta de la Olimpiada Internacional de Matemáticas de la OMI de este año, y estuvo a solo un paso de ganar la medalla de oro.

La competencia de la OMI que acaba de finalizar la semana pasada tenía seis preguntas relacionadas con álgebra, combinatoria, geometría y teoría de números. El sistema híbrido de IA propuesto por Google acertó cuatro preguntas y obtuvo 28 puntos, alcanzando el nivel de medalla de plata.

A principios de este mes, el profesor titular de UCLA, Terence Tao, acababa de promover la Olimpiada de Matemáticas de IA (Premio al Progreso AIMO) con un premio de un millón de dólares. Inesperadamente, el nivel de resolución de problemas de IA había mejorado a este nivel antes de julio.

En mi opinión, haga las preguntas simultáneamente y responda correctamente las preguntas más difíciles.

La OMI es la competición más antigua, grande y prestigiosa para jóvenes matemáticos y se celebra anualmente desde 1959. Recientemente, la competencia de la OMI también ha sido ampliamente reconocida como un gran desafío en el campo del aprendizaje automático, convirtiéndose en un punto de referencia ideal para medir las capacidades avanzadas de razonamiento matemático de los sistemas de inteligencia artificial.

En la competencia IMO de este año, AlphaProof y AlphaGeometry 2 desarrollados por el equipo de DeepMind lograron conjuntamente un avance histórico.

Entre ellos, AlphaProof es un sistema de aprendizaje por refuerzo para el razonamiento matemático formal, y AlphaGeometry 2 es una versión mejorada del sistema de resolución de geometría AlphaGeometry de DeepMind.

Este avance demuestra el potencial de la inteligencia artificial general (AGI) con capacidades avanzadas de razonamiento matemático para abrir nuevas áreas de ciencia y tecnología.

Entonces, ¿cómo participó el sistema de inteligencia artificial de DeepMind en la competencia de la OMI?

En pocas palabras, estos problemas matemáticos primero se traducen manualmente a un lenguaje matemático formal para que el sistema de inteligencia artificial pueda comprenderlos. En la competición oficial, los concursantes humanos envían sus respuestas en dos sesiones (dos días), con un tiempo límite de 4,5 horas para cada sesión. El sistema de inteligencia artificial compuesto por AlphaProof+AlphaGeometry 2 resolvió un problema en unos minutos, pero tardó tres días en resolver otros problemas. Aunque si sigues estrictamente las reglas, el sistema de DeepMind habrá agotado su tiempo de espera. Algunas personas especulan que esto puede implicar una gran cantidad de craqueo por fuerza bruta.

AlphaProof resolvió dos problemas de álgebra y un problema de teoría de números determinando las respuestas y demostrando su exactitud, dijo Google. Entre ellos se encuentra el problema más difícil de la competición, que sólo cinco concursantes resolvieron en la IMO de este año. Y AlphaGeometry 2 demuestra un problema de geometría.

Solución proporcionada por IA: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

Timothy Gowers, medallista de oro y medallista Fields de la OMI, y el Dr. Joseph Myers, dos veces medallista de oro de la OMI, presidente del Comité de Selección de Problemas 2024 de la OMI, calificaron las soluciones proporcionadas por el sistema combinado de acuerdo con las reglas de puntuación de la OMI.

Cada una de las seis preguntas vale 7 puntos, para una puntuación total máxima de 42 puntos. El sistema de DeepMind recibió una puntuación final de 28, lo que significa que los cuatro problemas que resolvió recibieron puntuaciones perfectas, equivalente a la puntuación más alta en la categoría de medalla de plata. El umbral para la medalla de oro de este año fue de 29 puntos, y 58 de los 609 jugadores en la competición oficial ganaron medallas de oro.

Este gráfico muestra el rendimiento del sistema de inteligencia artificial de Google DeepMind en relación con los competidores humanos en IMO 2024. El sistema obtuvo 28 puntos de un total de 42 puntos, alcanzando el mismo nivel que el medallista de plata de la competencia. Además, este año, con 29 puntos se puede ganar la medalla de oro.

AlphaProof: un método de razonamiento formal

Entre los sistemas híbridos de IA utilizados por Google, AlphaProof es un sistema autodidacta que utiliza el lenguaje formal Lean para probar afirmaciones matemáticas. Combina un modelo de lenguaje previamente entrenado con el algoritmo de aprendizaje por refuerzo AlphaZero.

Entre ellos, los lenguajes formales brindan importantes ventajas para verificar formalmente la exactitud de las pruebas de razonamiento matemático. Hasta ahora, esto ha tenido un uso limitado en el aprendizaje automático porque la cantidad de datos escritos por humanos era muy limitada.

Por el contrario, los métodos basados ​​en lenguaje natural, a pesar de tener acceso a mayores cantidades de datos, producen pasos de razonamiento intermedios y soluciones que parecen razonables pero son incorrectas.

Google DeepMind tiende un puente entre estos dos campos complementarios al ajustar el modelo Gemini para traducir automáticamente enunciados de problemas en lenguaje natural en enunciados formales, creando así una gran biblioteca de problemas formales de diversa dificultad.

Dado un problema matemático, AlphaProof genera soluciones candidatas y luego las prueba buscando posibles pasos de prueba en Lean. Cada solución de prueba encontrada y verificada se utiliza para fortalecer el modelo de lenguaje de AlphaProof y mejorar su capacidad para resolver problemas posteriores más desafiantes.

Para entrenar a AlphaProof, Google DeepMind demostró o refutó millones de problemas matemáticos que cubrían una amplia gama de dificultades y temas en las semanas previas a la competencia IMO. También se aplica un ciclo de entrenamiento durante la competencia para fortalecer la prueba de variantes de problemas de competencia autogenerados hasta que se encuentre una solución completa.

Infografía del proceso de bucle de entrenamiento de aprendizaje por refuerzo de AlphaProof: la red formal traduce alrededor de un millón de problemas matemáticos informales al lenguaje matemático formal. Luego, el solucionador busca en la red pruebas o refutación del problema, entrenándose gradualmente para resolver problemas más desafiantes utilizando el algoritmo AlphaZero.

AlphaGeometry 2 más competitivo

AlphaGeometry 2 es una versión significativamente mejorada de la IA matemática AlphaGeometry que apareció en la revista Nature este año. Es un sistema híbrido neurosimbólico en el que el modelo de lenguaje se basa en Gemini y se entrena desde cero con un orden de magnitud más de datos sintéticos que su predecesor. Esto ayuda al modelo a resolver problemas geométricos más desafiantes, incluidos aquellos relacionados con el movimiento de objetos y ecuaciones de ángulos, proporciones o distancias.

AlphaGeometry 2 presenta un motor simbólico que es dos órdenes de magnitud más rápido que su predecesor. Cuando se encuentran nuevos problemas, los novedosos mecanismos de intercambio de conocimientos permiten combinaciones avanzadas de diferentes árboles de búsqueda para resolver problemas más complejos.

Antes de la competencia de este año, AlphaGeometry 2 podía resolver el 83% de todos los problemas históricos de geometría de la OMI en los últimos 25 años, en comparación con solo el 53% de su predecesor. En IMO 2024, AlphaGeometry 2 resolvió el problema 4 dentro de los 19 segundos de recibir su formalización.

Un ejemplo de la pregunta 4 requiere demostrar que la suma de ∠KIL y ∠XPY es igual a 180°. AlphaGeometry 2 propone construir el punto E en la recta BI tal que ∠AEB = 90°. El punto E ayuda a dar significado al punto medio L del segmento de línea AB, creando así muchos pares de triángulos similares, como ABE ~ YBI y ALE ~ IPC, para probar la conclusión.

Google DeepMind también informa que, como parte del trabajo de la OMI, los investigadores también están experimentando con un nuevo sistema de razonamiento en lenguaje natural basado en Gemini y un sistema de razonamiento en lenguaje natural de última generación, con la esperanza de lograr capacidades avanzadas de resolución de problemas. El sistema no requiere traducción de preguntas a un lenguaje formal y puede combinarse con otros sistemas de inteligencia artificial. En la prueba de preguntas del concurso de la OMI de este año, "mostró un gran potencial".

Google continúa explorando métodos de inteligencia artificial para avanzar en el razonamiento matemático y planea publicar pronto más detalles técnicos sobre AlphaProof.

Estamos entusiasmados con un futuro en el que los matemáticos utilizarán herramientas de inteligencia artificial para explorar hipótesis, probar nuevos enfoques audaces para resolver problemas de larga data y completar rápidamente elementos de demostración que consumen mucho tiempo, y los sistemas de inteligencia artificial como Gemini marcarán una gran diferencia en matemáticas y más. El aspecto de razonamiento amplio se vuelve aún más poderoso.

equipo de investigación

Google dijo que la nueva investigación fue apoyada por la Olimpiada Internacional de Matemáticas y además:

El desarrollo de AlphaProof estuvo dirigido por Thomas Hubert, Rishi Mehta y Laurent Sartran; los contribuyentes clave incluyen a Hussain Masoom, Aja Huang, Miklós Z. Horváth, Tom Zahavy, Vivek Veeriah, Eric Wieser, Jessica Yung, Lei Yu, Yannick Schroecker, Julian Schrittwieser, Ottavia Bertolli, Borja Ibarz, Edward Lockhart, Edward Hughes, Mark Rowland y Grace Margand.

Entre ellos, Aja Huang, Julian Schrittwieser, Yannick Schroecker y otros miembros también fueron miembros principales del artículo AlphaGo hace 8 años (2016). Hace ocho años, AlphaGo, que construyeron basándose en el aprendizaje por refuerzo, se hizo famoso. Ocho años después, el aprendizaje por refuerzo vuelve a brillar en AlphaProof. Alguien se lamentó en el círculo de amigos: ¡RL ha vuelto!

Thang Luong dirige el trabajo de AlphaGeometry 2 y de inferencia del lenguaje natural. El desarrollo de AlphaGeometry 2 estuvo dirigido por Trieu Trinh y Yuri Chervonyi, con importantes contribuciones de Mirek Olšák, Xiaomeng Yang, Hoang Nguyen, Junehyuk Jung, Dawsen Hwang y Marcelo Menegali.

Además, David Silver, Quoc Le, Hassabis y Pushmeet Kohli son los responsables de coordinar y gestionar todo el proyecto.

Contenido de referencia:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/