Un sistema de inteligencia artificial (IA) llamado AlphaProof y AlphaGeometry 2 han resuelto problemas avanzados en matemáticas, alcanzando el mismo nivel que un medallista de plata en la Olimpiada Matemática Internacional por primera vez. Esta IA con capacidad de razonamiento matemático avanzado tiene el potencial de abrir nuevas fronteras en ciencia y tecnología. El sistema se basa en aprendizaje de refuerzo y es capaz de resolver problemas formalmente en matemáticas. La IMO es la competición más antigua, grande y prestigiosa para jóvenes matemáticos, donde los participantes tienen que resolver seis problemas excepcionalmente difíciles en áreas como álgebra, combinatoria, geometría e integers.
Los organizadores de la competición proporcionaron los problemas para nuestro sistema de IA. Nuestras soluciones fueron calificadas por matemáticos destacados en acuerdo con las normas de la OMI. El Dr. Joseph Myers, un dos veces medallista de oro de la OMI y presidente del Comité de Selección de Problemas de la OMI 2024, dijo que el hecho de que el sistema pueda resolver un problema tan complejo es muy impresionante. AlphaGeometry 2 probó el problema de la geometría, sin embargo, los dos problemas combinatorios quedaron sin resolver. Cada uno de los seis problemas puede ganar siete puntos, con un máximo total de 42. Nuestro sistema logró una puntuación final de 28 puntos, lo que equivale al nivel de medalla de plata en la competencia. Esta temporada, el umbral para obtener una medalla de oro comienza a los 29 puntos, y fue alcanzado por 58 de los 609 competidores en la competición oficial. Gráfico que muestra el rendimiento de nuestro sistema de IA en comparación con los humanos en IMO 2024. Ganamos 28 de los 42 puntos totales, lo que es el mismo nivel que un medallista de plata en la competencia. AlphaProof: un enfoque formal para probar razonamientos matemáticos AlphaProof es un sistema que se entrena a sí mismo para probar declaraciones matemáticas usando un lenguaje formal inclinado, combinando un modelo de lenguaje pre-entrenado con un algoritmo de aprendizaje de refuerzo AlphaZero. Las lenguas formales ofrecen la ventaja crítica que las pruebas que implican razonamientos matemáticos pueden ser verificadas formalmente para su corrección. Sin embargo, en el aprendizaje automático, los enfoques basados en lenguaje natural pueden conducir a pasos y soluciones de razonamiento intermedio plausibles pero erróneas, a pesar de tener acceso a datos de mayor escala. Hemos establecido un puente entre estas dos esferas complementarias mediante el ajuste de un modelo de Géminis para traducir automáticamente las declaraciones de problemas de lenguaje natural en declaraciones formales, creando una gran biblioteca de problemas formales de dificultad variable. Cuando se presenta con un problema, AlphaProof genera candidatos a la solución y luego los prueba o refuta buscando sobre posibles pasos de prueba en Lean. Cada prueba que fue encontrada y verificada se utiliza para reforzar el modelo del lenguaje de AlphaProof, mejorando su capacidad para resolver problemas posteriores, más difíciles.
Hemos entrenado AlphaProof para la OMI mediante la prueba o refutación de millones de problemas que abarcan una amplia gama de dificultades y áreas temáticas matemáticas durante un período de entrenamiento, así como durante el concurso. La infografía del proceso del ciclo de aprendizaje de AlphaProof muestra que alrededor de un millón de problemas matemáticos informales son traducidos a un lenguaje matemático formal por una red formalizadora. Posteriormente, una red de resolución de problemas busca pruebas o despruebas de los problemas utilizando el algoritmo AlphaZero para abordar problemas más difíciles. Una versión mejorada significativamente de AlfaGeometría (AlphaGeometry 2) es un sistema neuro-simbólico híbrido que utiliza un motor simbólico dos órdenes de magnitud más rápido que su predecesor. Este sistema fue basado en Géminis y entrenado en datos sintéticos de magnitud superior a sus antecedentes, lo cual le permitió abordar problemas de geometría mucho más complicados, incluyendo movimientos de objetos, ecuaciones de ángulos, proporciones o distancias. En competición este año, AlfaGeometría 2 pudo resolver el 83% de todos los problemas históricos de geometría de la OMI de los últimos 25 años en comparación con una tasa del 53%. Para la OMI 2024, AlfaGeometry 2 resolvió el problema 4 en 19 segundos después de recibir su formalización. El problema 4 solicita demostrar que la suma de KIL y XPY es igual a 180°. AlfaGeometría 2 fue propuesto para construir un punto E en la línea BI de modo que AEB sea de 90°. El punto E ayuda a dar sentido al punto medio L de AB, creando muchos pares de similares triángulos como ABE ~ YBI y ALE ~ IPC para demostrar la conclusión. En nuestro trabajo de la OMI, también experimentamos con un sistema de razonamiento del lenguaje natural basado en Géminis y nuestra última investigación para permitir habilidades avanzadas de resolución de problemas que no requieren traducir los problemas a un lenguaje formal y pueden combinarse con otros sistemas de IA. También probamos este enfoque en problemas de la OMI y obtenimos resultados prometedores. Nuestros equipos continúan investigando múltiples enfoques de IA para avanzar y planifican lanzar más detalles técnicos en AlphaProof pronto.
