Google DeepMind ha desarrollado AlphaProof, un sistema de IA que igualó el rendimiento de medalla de plata en la Olimpiada Internacional de Matemáticas de 2024, anotando 28 de 42 puntos. El sistema se quedó a solo un punto del oro en la competencia de matemáticas para universitarios más prestigiosa del mundo. Este avance demuestra progresos en la capacidad de la IA para manejar pruebas matemáticas complejas.
Los ordenadores han destacado durante mucho tiempo en cálculos, pero han tenido dificultades con el razonamiento lógico requerido para las matemáticas avanzadas. La nueva IA de Google DeepMind, AlphaProof, aborda esto al lograr un rendimiento de medallista de plata en la Olimpiada Internacional de Matemáticas de 2024 (IMO), la principal competición de matemáticas a nivel de secundaria. La IMO incluyó seis problemas valorados en siete puntos cada uno, sumando 42 puntos en total. Las medallas de oro requerían 29 puntos o más, logrados por 58 de 609 participantes, mientras que la plata se otorgó a quienes puntuaron entre 22 y 28 puntos, con 123 receptores. AlphaProof obtuvo 28 puntos, resolviendo cuatro problemas de forma independiente por 21 puntos y recurriendo a la especializada AlphaGeometry 2 para el problema de geometría para alcanzar el nivel de plata.
El desarrollo de AlphaProof comenzó superando la limitada disponibilidad de datos de entrenamiento para pruebas matemáticas formales. El equipo utilizó el software Lean, una herramienta para definiciones y verificaciones matemáticas precisas. Para ampliar el conjunto de datos, entrenaron un modelo de lenguaje grande Gemini para traducir enunciados matemáticos en lenguaje natural a Lean, generando alrededor de 80 millones de enunciados formalizados. Como explicó Thomas Hubert, investigador de DeepMind y autor principal, «La principal dificultad de trabajar con lenguajes formales es que hay muy pocos datos». A pesar de las imperfecciones, «Hay muchas formas de capitalizar las traducciones aproximadas», añadió.
La arquitectura del sistema se inspira en AlphaZero de DeepMind, combinando una red neuronal entrenada mediante ensayo y error con un algoritmo de búsqueda en árbol para explorar rutas de prueba. Recompensa las pruebas correctas y penaliza los pasos ineficientes, promoviendo soluciones elegantes. Una novedad, el Aprendizaje por Refuerzo en Tiempo de Prueba (TTRL), permite a AlphaProof generar variaciones de problemas difíciles para entrenamiento en el momento, imitando la resolución de problemas humanos. «Estábamos tratando de aprender este juego mediante ensayo y error», dijo Hubert.
Sin embargo, AlphaProof requirió asistencia humana para formalizar problemas en Lean y tardó varios días por problema desafiante, consumiendo cientos de días-TPU, mucho más allá de los límites de tiempo humanos de 4,5 horas por sesión. Solo seis humanos resolvieron el problema más difícil; AlphaProof fue el séptimo. DeepMind reconoce los altos costos computacionales, pero busca optimizar para un uso más amplio. «No queremos detenernos en competiciones de matemáticas. Queremos construir un sistema de IA que realmente contribuya a las matemáticas a nivel de investigación», afirmó Hubert. El equipo planea un programa de probadores de confianza para compartir una herramienta AlphaProof con matemáticos.
El trabajo se detalla en un artículo de Nature de 2025 (DOI: 10.1038/s41586-025-09833-y).