Los modelos innovadores AlphaProof y AlphaGeometry 2 resuelven problemas de razonamiento avanzado en matemáticas
La inteligencia general artificial (AGI) con razonamiento matemático avanzado tiene el potencial de abrir nuevas fronteras en ciencia y tecnología.
Hemos logrado grandes avances en la creación de sistemas de IA que ayudan a los matemáticos a descubrir nuevos conocimientos , algoritmos novedosos y respuestas a problemas pendientes . Sin embargo, los sistemas de IA actuales aún tienen dificultades para resolver problemas matemáticos generales debido a limitaciones en las habilidades de razonamiento y los datos de entrenamiento.
Hoy presentamos AlphaProof, un nuevo sistema basado en aprendizaje por refuerzo para el razonamiento matemático formal, y AlphaGeometry 2, una versión mejorada de nuestro sistema de resolución de geometría . Juntos, estos sistemas resolvieron cuatro de los seis problemas de la Olimpiada Internacional de Matemáticas (OIM) de este año , logrando por primera vez el mismo nivel que un medallista de plata en la competencia.
Rendimiento revolucionario de la IA para resolver problemas matemáticos complejos
La IMO es la competición más antigua, grande y prestigiosa para jóvenes matemáticos, que se celebra anualmente desde 1959.
Cada año, matemáticos de élite de nivel preuniversitario se entrenan, a veces durante miles de horas, para resolver seis problemas excepcionalmente difíciles de álgebra, combinatoria, geometría y teoría de números.
Muchos de los ganadores de la Medalla Fields , uno de los máximos honores para los matemáticos, han representado a su país en la OMI.
Más recientemente, la competencia anual de la OMI también ha sido ampliamente reconocida como un gran desafío en el aprendizaje automático y un punto de referencia aspiracional para medir las capacidades avanzadas de razonamiento matemático de un sistema de IA.
Este año, aplicamos nuestro sistema de IA combinado a los problemas de la competencia, proporcionados por los organizadores de la OMI.
Nuestras soluciones fueron calificadas de acuerdo con las reglas de concesión de puntos de la OMI por los destacados matemáticos Prof. Sir Timothy Gowers , medallista de oro de la OMI y ganador de la medalla Fields, y Dr. Joseph Myers , dos veces medallista de oro de la OMI y presidente del Comité de selección de problemas de la OMI 2024.
En primer lugar, los problemas se tradujeron manualmente a un lenguaje matemático formal para que nuestros sistemas los comprendieran.
En la competencia oficial, los estudiantes presentaron las respuestas en dos sesiones de 4,5 horas cada una. Nuestros sistemas resolvieron un problema en cuestión de minutos y tardaron hasta tres días en resolver los demás.
AlphaProof resolvió dos problemas de álgebra y un problema de teoría de números determinando la respuesta y demostrando que era correcta.
Esto incluyó el problema más difícil de la competencia, resuelto por solo cinco concursantes en la IMO de este año. AlphaGeometry 2 demostró el problema de geometría, mientras que los dos problemas de combinatoria quedaron sin resolver.
Cada uno de los seis problemas puede sumar siete puntos, con un máximo total de 42. Nuestro sistema logró una puntuación final de 28 puntos, lo que le permitió obtener una puntuación perfecta en cada problema resuelto, lo que equivale al punto más alto de la categoría de medalla de plata.
Este año, el umbral de la medalla de oro comienza en 29 puntos, y lo lograron 58 de los 609 concursantes en la competencia oficial.
AlphaProof: un enfoque formal del razonamiento
AlphaProof es un sistema que se entrena a sí mismo para demostrar enunciados matemáticos en el lenguaje formal Lean .
Combina un modelo de lenguaje previamente entrenado 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 fundamental de que las pruebas que implican razonamiento matemático pueden verificarse formalmente para comprobar su exactitud.
Sin embargo, su uso en el aprendizaje automático se ha visto limitado hasta ahora por la cantidad muy limitada de datos escritos por humanos disponibles.
Por el contrario, los enfoques basados en el lenguaje natural pueden alucinar pasos y soluciones intermedias de razonamiento plausibles pero incorrectos, a pesar de tener acceso a órdenes de magnitud mayores de datos.
Establecimos un puente entre estas dos esferas complementarias mediante el ajuste fino de un modelo Gemini para traducir automáticamente enunciados de problemas en lenguaje natural en enunciados formales, creando una gran biblioteca de problemas formales de diversa dificultad.
Cuando se presenta un problema, AlphaProof genera soluciones candidatas y luego las prueba o refuta buscando posibles pasos de prueba en Lean.
Cada prueba que se encuentra y verifica se utiliza para reforzar el modelo de lenguaje de AlphaProof, mejorando su capacidad para resolver problemas posteriores más desafiantes.
Entrenamos a AlphaProof para la OMI demostrando o refutando millones de problemas, cubriendo una amplia gama de dificultades y áreas temáticas matemáticas durante un período de semanas previo a la competencia.
El ciclo de entrenamiento también se aplicó durante el concurso, reforzando las demostraciones de variaciones autogeneradas de los problemas del concurso hasta que se pudo encontrar una solución completa.
Luego, una red de solucionadores busca pruebas o refutaciones de los problemas y se entrena progresivamente a través del algoritmo AlphaZero para resolver problemas más desafiantes.
Una AlphaGeometry 2 más competitiva
AlphaGeometry 2 es una versión significativamente mejorada de AlphaGeometry . Es un sistema híbrido neurosimbólico en el que el modelo de lenguaje se basó en Gemini y se entrenó desde cero con un orden de magnitud de datos más sintéticos que su predecesor.
Esto ayudó al modelo a abordar problemas de geometría mucho más desafiantes, incluidos problemas sobre movimientos de objetos y ecuaciones de ángulos, proporciones o distancias.
AlphaGeometry 2 utiliza un motor simbólico que es dos órdenes de magnitud más rápido que su predecesor.
Cuando se presenta un nuevo problema, se utiliza un novedoso mecanismo de intercambio de conocimientos para permitir combinaciones avanzadas de diferentes árboles de búsqueda para abordar problemas más complejos.
Antes de la competición de este año, AlphaGeometry 2 podía resolver el 83% de todos los problemas de geometría históricos de la OMI de los últimos 25 años, en comparación con el 53% logrado por su predecesor. Para la OMI 2024, AlphaGeometry 2 resolvió el problema 4 en 19 segundos después de recibir su formalización.
Nuevas fronteras en el razonamiento matemático
Como parte de nuestro trabajo en la OMI, también experimentamos con un sistema de razonamiento en lenguaje natural, basado en Gemini y en nuestras últimas investigaciones, para permitir habilidades avanzadas de resolución de problemas.
Este sistema no requiere que los problemas se traduzcan a un lenguaje formal y se puede combinar con otros sistemas de IA. También probamos este enfoque en los problemas de la OMI de este año y los resultados fueron muy prometedores.
Nuestros 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.
Estamos entusiasmados por un futuro en el que los matemáticos trabajen con herramientas de IA para explorar hipótesis, probar nuevos enfoques audaces para resolver problemas de larga data y completar rápidamente elementos de pruebas que consumen mucho tiempo, y donde los sistemas de IA como Gemini se vuelvan más capaces en matemáticas y razonamiento más amplio.