En un avance sin precedentes, los modelos de inteligencia artificial AlphaProof y AlphaGeometry 2 han logrado resolver problemas avanzados de razonamiento matemático, alcanzando un nivel equivalente al de una medalla de plata en la Olimpiada Matemática Internacional (IMO). Este logro destaca el potencial de la inteligencia artificial general (AGI) en la exploración de nuevas fronteras en la ciencia y la tecnología.
Avances en el Razonamiento Matemático con IA
La IMO, establecida en 1959, es la competencia más prestigiosa para jóvenes matemáticos preuniversitarios. Cada año, estos competidores resuelven seis problemas extremadamente difíciles en áreas como álgebra, combinatoria, geometría y teoría de números, invirtiendo a menudo miles de horas de entrenamiento.
En este contexto, la competencia anual de la IMO también se ha convertido en un gran desafío para el aprendizaje automático y un referente aspiracional para medir las capacidades de razonamiento matemático avanzado de un sistema de IA. Este año, los modelos de IA AlphaProof y AlphaGeometry 2 se aplicaron a los problemas de la competencia proporcionados por los organizadores de la IMO. Las soluciones fueron evaluadas según las reglas de puntuación de la IMO por destacados matemáticos, incluyendo al profesor Sir Timothy Gowers, medallista Fields, y el Dr. Joseph Myers, presidente del Comité de Selección de Problemas de la IMO 2024.
Logros de AlphaProof y AlphaGeometry 2
AlphaProof resolvió dos problemas de álgebra y uno de teoría de números, incluyendo el problema más difícil de la competencia, que solo fue resuelto por cinco concursantes en la IMO de este año. AlphaGeometry 2 resolvió un problema de geometría, mientras que los dos problemas de combinatoria quedaron sin resolver.
Cada problema en la IMO puede otorgar hasta siete puntos, con un total máximo de 42. El sistema logró una puntuación final de 28 puntos, obteniendo una puntuación perfecta en cada problema resuelto, lo que equivale al nivel más alto de la categoría de medalla de plata. Este año, el umbral para la medalla de oro comienza en 29 puntos, alcanzado por 58 de los 609 concursantes en la competencia oficial.
AlphaProof: Un Enfoque Formal para el Razonamiento
AlphaProof es un sistema que se entrena para demostrar enunciados matemáticos en el lenguaje formal Lean. Combina un modelo de lenguaje preentrenado con el algoritmo de aprendizaje por refuerzo AlphaZero, que previamente se enseñó a sí mismo a dominar los juegos de ajedrez, shogi y Go.
Los lenguajes formales ofrecen la ventaja crítica de que las pruebas que involucran razonamiento matemático pueden verificarse formalmente para asegurar su corrección. Sin embargo, su uso en el aprendizaje automático ha sido limitado debido a la cantidad muy reducida de datos escritos por humanos disponibles.
Para superar esta limitación, se estableció un puente entre los enfoques basados en lenguaje natural y los formales mediante el ajuste fino de un modelo Gemini para traducir automáticamente enunciados de problemas en lenguaje natural a enunciados formales, creando una vasta biblioteca de problemas formales de diversa dificultad.
AlphaProof genera candidatos de solución y luego los prueba o refuta buscando posibles pasos de prueba en Lean. Cada prueba encontrada y verificada refuerza el modelo de lenguaje de AlphaProof, mejorando su capacidad para resolver problemas más desafiantes en el futuro.
Un AlphaGeometry 2 Más Competitivo
AlphaGeometry 2 es una versión significativamente mejorada de AlphaGeometry. Es un sistema híbrido neuro-simbólico basado en el modelo Gemini y entrenado desde cero con una cantidad de datos sintéticos mucho mayor que su predecesor. Esto permitió al modelo abordar problemas de geometría mucho más desafiantes, incluyendo movimientos de objetos y ecuaciones de ángulos, razones o distancias.
AlphaGeometry 2 emplea un motor simbólico que es dos órdenes de magnitud más rápido que su predecesor. 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 IMO de los últimos 25 años, en comparación con el 53% logrado por su predecesor.
Nuevas Fronteras en el Razonamiento Matemático
Como parte de su trabajo en la IMO, los desarrolladores de AlphaProof también experimentaron con un sistema de razonamiento en lenguaje natural, basado en Gemini y la última investigación para habilitar habilidades avanzadas de resolución de problemas. Este sistema no requiere que los problemas se traduzcan a un lenguaje formal y podría combinarse con otros sistemas de IA. Los resultados mostraron gran promesa.
Los equipos continúan explorando múltiples enfoques de IA para avanzar en el razonamiento matemático y planean publicar más detalles técnicos sobre AlphaProof pronto.
Agradecimientos
El desarrollo de AlphaProof fue liderado por Thomas Hubert, Rishi Mehta y Laurent Sartran; AlphaGeometry 2 y los esfuerzos de razonamiento en lenguaje natural fueron liderados por Thang Luong. Este trabajo fue asesorado por David Silver y Pushmeet Kohli. Agradecimientos especiales a la organización de la Olimpiada Matemática Internacional por su apoyo y a los numerosos contribuyentes de los proyectos Lean y Mathlib, sin los cuales AlphaProof no hubiera sido posible.
fuente: Deepmind.google
