DeepMind de Google ha dado un paso importante en la ingeniería de inteligencia artificial con el desarrollo de dos modelos avanzados capaces de resolver problemas matemáticos complejos. Los modelos AlphaProof y AlphaGeometry 2 fueron puestos a prueba durante la Olimpiada Matemática Internacional (IMO) de 2024, alcanzando un rendimiento notable.
El desempeño de estos sistemas se reflejó en la resolución de cuatro de seis problemas planteados en la competencia, cubriendo dos de álgebra, uno de teoría de números y uno de geometría. Gracias a su capacidad de resolver estos retos, AlphaProof y AlphaGeometry 2 obtuvieron una puntuación de 28 sobre 42 puntos posibles, suficiente para lograr una medalla de plata. Solo para poner en perspectiva, la calificación para recibir una medalla de oro inicia en los 29 puntos. Esta puntuación situó a los modelos en la posición 58 de un total de 609 participantes.
AlphaProof es un sistema basado en aprendizaje por refuerzo que traduce problemas matemáticos en lenguaje natural al lenguaje formal utilizando Lean, un programa matemático. Su funcionamiento se basa en una versión optimizada del modelo Gemini y el algoritmo AlphaZero de DeepMind, conocido por su éxito en juegos como ajedrez y Go.
Por su parte, AlphaGeometry 2, una versión mejorada del modelo original AlphaGeometry, está optimizado para problemas de geometría. Utiliza un modelo híbrido neurosimbólico y ha sido entrenado con gran cantidad de datos sintéticos, permitiéndole resolver problemas complejos de geometría rápidamente, como lo demuestra su capacidad de resolver un problema en solo 19 segundos tras su formalización.
Uno de los logros más destacados de AlphaProof fue la resolución del problema más difícil del concurso, que solo cinco humanos fueron capaces de resolver. Sin embargo, ambos sistemas mostraron dificultades con dos problemas de combinatoria que no pudieron resolver.
En cuanto a la investigación detrás de estos sistemas, fueron entrenados con aproximadamente un millón de ejemplos de problemas de la IMO antes de la competencia. El enfoque de razonamiento formal de AlphaProof le permite generar y verificar candidatos de solución de manera efectiva, mejorando su proceso de aprendizaje. Tim Gowers y Joseph Myers, destacados matemáticos, colaboraron en la validación de las pruebas, confirmando la precisión de los modelos y otorgándoles máxima puntuación.
Estos avances refuerzan la idea de que las aplicaciones de la IA en la investigación matemática y la resolución de problemas son no solo posibles, sino también prometedoras.
DeepMind tiene planes de incorporar los insights logrados con estos modelos en futuras versiones de sus herramientas de IA Gemini, aunque aún no se han especificado los plazos para estas mejoras. AlphaProof y AlphaGeometry 2 fueron capaces de resolver la mayoría de los problemas en la IMO, una competencia que tradicionalmente ha sido un desafío incluso para los matemáticos humanos más talentosos.