El jueves, Google DeepMind Anunciado que los sistemas de IA llamados AlphaProof y AlphaGeometry 2 habrían resuelto cuatro de los seis problemas de este año Olimpiada Internacional de Matemáticas (OMI), logrando una puntuación equivalente a una medalla de plata. El gigante tecnológico afirma que es la primera vez que una IA alcanza este nivel de rendimiento en la prestigiosa competencia de matemáticas, pero como es habitual en la IA, las afirmaciones no son tan claras como parecen.
Google dice que AlphaProof utiliza el aprendizaje de refuerzo para probar afirmaciones matemáticas en el lenguaje formal llamado InclinarseEl sistema se entrena a sí mismo generando y verificando millones de pruebas, y abordando progresivamente problemas más difíciles. Mientras tanto, AlphaGeometry 2 se describe como una versión mejorada del algoritmo de Google. Modo de IA de resolución de geometría anteriorahora impulsado por un modelo de lenguaje basado en Gemini y entrenado con muchos más datos.
Según Google, matemáticos destacados Señor Timothy Gowers y Dr. Joseph Myers La empresa calificó las soluciones del modelo de IA utilizando las reglas oficiales de la OMI. La empresa informa que su sistema combinado obtuvo 28 de los 42 puntos posibles, apenas por debajo del umbral de 29 puntos para la medalla de oro. Esto incluyó una puntuación perfecta en el problema más difícil de la competencia, que Google afirma que solo cinco concursantes humanos resolvieron este año.
Un concurso de matemáticas como ningún otro
La IMO, que se celebra anualmente desde 1959, enfrenta a matemáticos de élite de nivel preuniversitario a problemas excepcionalmente difíciles de álgebra, combinatoria, geometría y teoría de números. El desempeño en los problemas de la IMO se ha convertido en un punto de referencia reconocido para evaluar las capacidades de razonamiento matemático de un sistema de IA.
Google afirma que AlphaProof Resuelto Dos problemas de álgebra y un problema de teoría de números, mientras que AlphaGeometry 2 abordó la cuestión de geometría. El modelo de IA no logró resolver los dos problemas combinatorios. La empresa afirma que sus sistemas resolvieron un problema en cuestión de minutos, mientras que otros tardaron hasta tres días.
Google afirma que primero tradujo los problemas de la OMI a un lenguaje matemático formal para que su modelo de inteligencia artificial los procesara. Este paso difiere de la competencia oficial, donde los participantes humanos trabajan directamente con los enunciados de los problemas durante dos sesiones de 4,5 horas.
Google informa que antes de la competición de este año, AlphaGeometry 2 podía resolver el 83 por ciento de los problemas de geometría históricos de la OMI de los últimos 25 años, frente al 53 por ciento de éxito de su predecesor. La empresa afirma que el nuevo sistema resolvió el problema de geometría de este año en 19 segundos después de recibir la versión formalizada.
Limitaciones
A pesar de las afirmaciones de Google, Sir Timothy Gowers ofreció una perspectiva más matizada sobre los modelos de Google DeepMind en un hilo Publicado en X. Si bien reconoció el logro como “mucho más allá de lo que los demostradores automáticos de teoremas podían hacer antes”, Gowers señaló varias calificaciones clave.
“La principal limitación es que el programa necesitó mucho más tiempo que los competidores humanos (para algunos de los problemas, más de 60 horas) y, por supuesto, una velocidad de procesamiento mucho mayor que la del pobre cerebro humano”, escribió Gowers. “Si los competidores humanos hubieran tenido ese tiempo por problema, sin duda habrían obtenido mejores resultados”.
Gowers también señaló que los humanos tradujeron manualmente los problemas al lenguaje formal Lean antes de que el modelo de IA comenzara a funcionar. Hizo hincapié en que, si bien la IA realizó el razonamiento matemático central, este paso de “autoformalización” lo realizaron los humanos.
En cuanto a las implicaciones más amplias para la investigación matemática, Gowers expresó incertidumbre. “¿Estamos cerca del punto en que los matemáticos sean redundantes? Es difícil decirlo. Supongo que todavía nos faltan uno o dos avances para lograrlo”, escribió. Sugirió que los largos tiempos de procesamiento del sistema indican que no ha “resuelto las matemáticas”, pero reconoció que “claramente ocurre algo interesante cuando funciona”.
Incluso con estas limitaciones, Gowers especuló que estos sistemas de IA podrían convertirse en valiosas herramientas de investigación. “Así que podríamos estar cerca de tener un programa que permitiría a los matemáticos obtener respuestas a una amplia gama de preguntas, siempre que esas preguntas no fueran demasiado difíciles, el tipo de cosas que uno puede hacer en un par de horas. Eso sería enormemente útil como herramienta de investigación, incluso si no fuera capaz de resolver problemas abiertos”.
