El razonamiento matemático es un aspecto vital de las capacidades cognitivas humanas, que impulsa el progreso de los descubrimientos científicos y los desarrollos tecnológicos. A medida que nos esforzamos por desarrollar una inteligencia artificial general que coincida con la cognición humana, es esencial equipar a la IA con capacidades avanzadas de razonamiento matemático. Si bien los sistemas de inteligencia artificial actuales pueden manejar problemas matemáticos básicos, tienen dificultades con el razonamiento complejo necesario para disciplinas matemáticas avanzadas como el álgebra y la geometría. Sin embargo, esto podría estar cambiando, ya que Google DeepMind ha logrado avances significativos en el avance de las capacidades de razonamiento matemático de un sistema de inteligencia artificial. Este avance se logra en la Olimpiada Internacional de Matemáticas (OMI) 2024. Establecida en 1959, la OMI 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 inteligencia artificial: 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 seis problemas, con un desempeño al nivel de un medallista de plata. En este artículo, exploraremos cómo funcionan estos sistemas para resolver problemas matemáticos.
AlphaProof: combinación de inteligencia artificial y lenguaje formal para la demostración de teoremas matemáticos
AlphaProof es un sistema de inteligencia artificial diseñado para probar afirmaciones matemáticas utilizando el lenguaje formal Lean. Integra Gemini, un modelo de lenguaje previamente entrenado, con AlphaZero, un algoritmo de aprendizaje por refuerzo reconocido por dominar el ajedrez, el shogi y el Go.
El modelo Gemini traduce enunciados de problemas en lenguaje natural a planteamientos formales, creando una biblioteca de problemas con distintos niveles de dificultad. Esto tiene dos propósitos: convertir el lenguaje natural impreciso en un lenguaje formal preciso para verificar pruebas matemáticas y utilizar las habilidades predictivas de Gemini para generar una lista de posibles soluciones con precisión del lenguaje formal.
Cuando AlphaProof encuentra un problema, genera posibles soluciones y busca pasos de prueba en Lean para verificarlas o refutarlas. Se trata esencialmente de un enfoque neurosimbólico, en el que la red neuronal Gemini traduce instrucciones del lenguaje natural al lenguaje formal simbólico Lean para probar o refutar la afirmación. De manera similar al mecanismo de autojuego de AlphaZero, donde el sistema aprende jugando contra sí mismo, AlphaProof se entrena intentando probar afirmaciones matemáticas. Cada intento de prueba refina el modelo de lenguaje de AlphaProof, y las pruebas exitosas refuerzan la capacidad del modelo para abordar problemas más desafiantes.
Para la Olimpiada Internacional de Matemáticas (OMI), AlphaProof se capacitó demostrando o refutando millones de problemas que cubrían diferentes niveles de dificultad y temas matemáticos. Esta formación continuó durante la competición, donde AlphaProof perfeccionó sus soluciones hasta encontrar respuestas completas a los problemas.
AlphaGeometry 2: integración de LLM e IA simbólica para resolver problemas de geometría
AlphaGeometry 2 es la última versión de la serie AlphaGeometry, diseñada para abordar problemas geométricos con mayor precisión y eficiencia. Partiendo de la base de su predecesor, AlphaGeometry 2 emplea un enfoque neurosimbólico que fusiona modelos neuronales de lenguaje grande (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 la resolución de problemas de geometría. El LLM en AlphaGeometry predice nuevas construcciones geométricas, mientras que la IA simbólica aplica la lógica formal para generar pruebas.
Cuando se enfrenta a un problema geométrico, el LLM de AlphaGeometry evalúa numerosas posibilidades y predice construcciones cruciales para la resolución de problemas. Estas predicciones sirven como pistas valiosas, guiando el motor simbólico hacia deducciones precisas y acercándose a una solución. Este enfoque innovador permite a AlphaGeometry abordar desafíos geométricos complejos que se extienden más allá de los escenarios convencionales.
Una mejora clave en AlphaGeometry 2 es la integración de Gemini LLM. Este modelo se entrena desde cero con muchos más datos sintéticos que su predecesor. Esta amplia formación lo prepara para manejar problemas de geometría más difíciles, incluidos aquellos que involucran movimientos de objetos y ecuaciones de ángulos, proporciones 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 a una velocidad sin precedentes. Estos avances hacen de AlphaGeometry 2 una poderosa herramienta para resolver problemas geométricos complejos, estableciendo un nuevo estándar en el campo.
AlphaProof y AlphaGeometry 2 en la OMI
Este año, en la Olimpiada Internacional de Matemáticas (OMI), los participantes fueron evaluados con seis problemas diferentes: 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 un problema 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 superó los dos desafíos combinatorios.
Cada problema en la IMO vale siete puntos, sumando un máximo de 42. 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 para la 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 mostrado avances impresionantes en las capacidades de resolución de problemas matemáticos de la IA. Sin embargo, estos sistemas todavía dependen de expertos humanos para traducir los problemas matemáticos a un lenguaje formal para su procesamiento. Además, no está claro cómo estas habilidades matemáticas especializadas podrían incorporarse a otros sistemas de IA, por ejemplo para explorar hipótesis, probar soluciones innovadoras a problemas de larga data y gestionar de manera eficiente aspectos de las pruebas que consumen mucho tiempo.
Para superar estas limitaciones, los investigadores de Google están desarrollando un sistema de razonamiento en lenguaje natural basado en Gemini y sus últimas investigaciones. Este nuevo sistema tiene como objetivo mejorar las capacidades de resolución de problemas sin requerir traducción formal de idiomas y está diseñado para integrarse sin problemas con otros sistemas de IA.
La conclusión
La actuación de AlphaProof y AlphaGeometry 2 en la Olimpiada Internacional de Matemáticas es un avance notable en la capacidad de la IA para abordar el razonamiento matemático complejo. Ambos sistemas demostraron un rendimiento de nivel de medalla de plata al resolver cuatro de seis problemas desafiantes, lo que demuestra avances significativos en la prueba formal y la resolución de problemas geométricos. A pesar de sus logros, estos sistemas de IA todavía dependen de la aportación humana para traducir los problemas al lenguaje formal y enfrentan desafíos de integración con otros sistemas de IA. Las investigaciones futuras tienen como objetivo mejorar aún más estos sistemas, integrando potencialmente el razonamiento del lenguaje natural para ampliar sus capacidades a una gama más amplia de desafíos matemáticos.