La IA en la Olimpiada Matemática Internacional: Cómo AlphaProof y AlphaGeometry 2 alcanzaron el nivel de medalla de plata

La razón matemática es un aspecto vital de las capacidades cognitivas humanas, impulsando el progreso en los descubrimientos científicos y los desarrollos tecnológicos. A medida que nos esforzamos por desarrollar una inteligencia artificial general que iguale la cognición humana, es esencial equipar a la IA con capacidades de razonamiento matemático avanzadas. Si bien los sistemas de IA actuales pueden manejar problemas matemáticos básicos, luchan con el razonamiento complejo necesario para las disciplinas matemáticas avanzadas como el álgebra y la geometría. Sin embargo, esto podría estar cambiando, ya que Google DeepMind ha hecho avances significativos en el desarrollo de un sistema de IA con capacidades de razonamiento matemático. Este avance se logró en la Olimpiada Matemática Internacional (IMO) 2024. Establecida en 1959, la IMO es la competencia de matemáticas más antigua y prestigiosa, que desafía a estudiantes de secundaria de todo el mundo con problemas de álgebra, combinatoria, geometría y teoría de números. Cada año, equipos de jóvenes matemáticos compiten para resolver seis problemas muy desafiantes. Este año, Google DeepMind presentó dos sistemas de IA: AlphaProof, que se centra en el razonamiento matemático formal, y AlphaGeometry 2, que se especializa en la resolución de problemas geométricos. Estos sistemas de IA lograron resolver cuatro de los seis problemas, lo que les valió un desempeño al nivel de medalla de plata. En este artículo, exploraremos cómo funcionan estos sistemas para resolver problemas matemáticos.

AlphaProof: Combinando IA y lenguaje formal para la demostración de teoremas matemáticos

AlphaProof es un sistema de IA diseñado para demostrar afirmaciones matemáticas utilizando el lenguaje formal Lean. Integra Gemini, un modelo de lenguaje preentrenado, con AlphaZero, un algoritmo de aprendizaje por refuerzo renombrado por dominar el ajedrez, el shogi y el Go.

El modelo Gemini traduce las declaraciones de problemas de lenguaje natural a declaraciones formales, creando una biblioteca de problemas con diferentes niveles de dificultad. Esto sirve para dos propósitos: convertir el lenguaje natural impreciso en lenguaje formal preciso para verificar las demostraciones matemáticas y utilizar las capacidades predictivas de Gemini para generar una lista de posibles soluciones con precisión de lenguaje formal.

Cuando AlphaProof se enfrenta a un problema, genera posibles soluciones y busca pasos de demostración en Lean para verificar o refutarlos. Esto es esencialmente un enfoque neuro-simbólico, donde la red neuronal, Gemini, traduce las instrucciones de lenguaje natural en el lenguaje formal simbólico Lean para demostrar o refutar la afirmación. Similar al mecanismo de autojuego de AlphaZero, donde el sistema aprende jugando partidas contra sí mismo, AlphaProof se entrena intentando demostrar afirmaciones matemáticas. Cada intento de demostración refina el modelo de lenguaje de AlphaProof, con demostraciones exitosas que refuerzan la capacidad del modelo para abordar problemas más desafiantes.

Para la Olimpiada Matemática Internacional (IMO), AlphaProof se entrenó demostrando o refutando millones de problemas que cubrían diferentes niveles de dificultad y temas matemáticos. Este entrenamiento continuó durante la competencia, donde AlphaProof refinó sus soluciones hasta que encontró respuestas completas a los problemas.

AlphaGeometry 2: Integrando LLM y IA simbólica para resolver problemas geométricos

AlphaGeometry 2 es la última iteración de la serie AlphaGeometry, diseñada para abordar problemas geométricos con mayor precisión y eficiencia. Basándose en la base de su predecesor, AlphaGeometry 2 emplea un enfoque neuro-simbólico que combina modelos de lenguaje grandes (LLM) con IA simbólica. Esta integración combina la lógica basada en reglas con la capacidad predictiva de las redes neuronales para identificar puntos auxiliares, esenciales para resolver problemas geométricos. El LLM en AlphaGeometry predice nuevas construcciones geométricas, mientras que la IA simbólica aplica la lógica formal para generar demostraciones.

Cuando se enfrenta a un problema geométrico, el LLM de AlphaGeometry evalúa numerosas posibilidades, prediciendo constructos cruciales para la resolución del problema. Estas predicciones sirven como pistas valiosas, guiando el motor simbólico hacia deducciones precisas y avanzando hacia una solución. Este enfoque innovador permite a AlphaGeometry abordar desafíos geométricos complejos que van más allá de los escenarios convencionales.

Una de las mejoras clave en AlphaGeometry 2 es la integración del LLM Gemini. Este modelo se entrena desde cero con una cantidad significativamente mayor de datos sintéticos que su predecesor. Este entrenamiento extensivo lo equipa para manejar problemas geométricos más difíciles, incluidos aquellos que involucran movimientos de objetos y ecuaciones de ángulos, razones o distancias. Además, AlphaGeometry 2 cuenta con un motor simbólico que opera dos órdenes de magnitud más rápido, lo que le permite explorar soluciones alternativas con una velocidad sin precedentes. Estos avances convierten a AlphaGeometry 2 en una herramienta poderosa para resolver problemas geométricos intrincados, estableciendo un nuevo estándar en el campo.

AlphaProof y AlphaGeometry 2 en la IMO

Este año en la Olimpiada Matemática Internacional (IMO), los participantes se enfrentaron a seis problemas diversos: dos de álgebra, uno de teoría de números, uno de geometría y dos de combinatoria. Los investigadores de Google tradujeron estos problemas al lenguaje matemático formal para AlphaProof y AlphaGeometry 2. AlphaProof abordó dos problemas de álgebra y uno de teoría de números, incluido el problema más difícil de la competencia, resuelto por solo cinco concursantes humanos este año. Mientras tanto, AlphaGeometry 2 resolvió con éxito el problema de geometría, aunque no logró resolver los dos desafíos de combinatoria.

Cada problema en la IMO vale siete puntos, lo que suma un máximo de 42 puntos. AlphaProof y AlphaGeometry 2 obtuvieron 28 puntos, logrando puntuaciones perfectas en los problemas que resolvieron. Esto los colocó en el extremo superior de la categoría de medalla de plata. El umbral de medalla de oro este año fue de 29 puntos, alcanzado por 58 de los 609 concursantes.

Próximo salto: Lenguaje natural para desafíos matemáticos

AlphaProof y AlphaGeometry 2 han demostrado avances impresionantes en las capacidades de resolución de problemas matemáticos de la IA. Sin embargo, estos sistemas aún dependen de expertos humanos para traducir problemas matemáticos al lenguaje formal para su procesamiento. Además, no está claro cómo estas habilidades matemáticas especializadas podrían incorporarse en otros sistemas de IA, como para explorar hipótesis, probar soluciones innovadoras a problemas de larga data y gestionar eficientemente aspectos tediosos de las demostraciones.

Para superar estas limitaciones, los investigadores de Google están desarrollando un sistema de razonamiento de lenguaje natural basado en Gemini y su investigación más reciente. Este nuevo sistema tiene como objetivo avanzar en las capacidades de resolución de problemas sin requerir la traducción al lenguaje formal y está diseñado para integrarse suavemente con otros sistemas de IA.

En resumen

El desempeño de AlphaProof y AlphaGeometry 2 en la Olimpiada Matemática Internacional es un salto notable hacia adelante en la capacidad de la IA para abordar el razonamiento matemático complejo. Ambos sistemas demostraron un desempeño al nivel de medalla de plata al resolver cuatro de los seis problemas desafiantes, demostrando avances significativos en la demostración formal y la resolución de problemas geométricos. A pesar de sus logros, estos sistemas de IA aún dependen de la entrada humana para traducir problemas al lenguaje formal y enfrentan desafíos de integración con otros sistemas de IA. La investigación futura apunta a mejorar aún más estos sistemas, potencialmente integrando el razonamiento de lenguaje natural para extender sus capacidades a través de una gama más amplia de desafíos matemáticos.