AlphaProof: la IA de DeepMind que domina las matemáticas como un medallista olímpico
Cuando hablamos de IA aplicada a las matemáticas, normalmente pensamos en ordenadores realizando cálculos a velocidades imposibles para humanos. Pero hacer matemáticas de alto nivel va mucho más allá de calcular: requiere razonamiento lógico, comprensión profunda y una pizca de creatividad. Y ahí es donde las máquinas siempre habían tropezado… hasta ahora.
DeepMind acaba de presentar AlphaProof, una IA que ha conseguido igualar el rendimiento de los medallistas de plata en la Olimpiada Internacional de Matemáticas de 2024. A solo un punto de la medalla de oro. Y esto, créeme, no es poca cosa.
De calculadoras a razonadores: el salto evolutivo de la IA
Los ordenadores siempre han sido excelentes con los números, pero eso no ha provocado despidos masivos entre matemáticos. ¿Por qué? Porque calcular rápido y entender matemáticas son habilidades completamente diferentes.
Un ordenador tradicional puede multiplicar millones de cifras en microsegundos, pero le cuesta entender por qué lo está haciendo. Es como tener un Ferrari pero no saber conducir: tienes potencia, pero te falta comprensión.
El reto de la comprensión matemática real
Cuando los matemáticos construyen demostraciones, no solo aplican fórmulas mecánicamente. Entienden la estructura profunda de las matemáticas, eligen caminos elegantes y diseñan pasos inteligentes para llegar a una conclusión. Como comenta Thomas Hubert, investigador principal del estudio AlphaProof: «Bertrand Russell publicó un libro de 500 páginas solo para demostrar que uno más uno son dos».
El equipo de DeepMind no quería una IA que simplemente pareciera entender matemáticas, sino una que realmente las comprendiera al nivel de los mejores cerebros humanos.
Lean: el traductor matemático que cambió las reglas del juego
El primer obstáculo era el mismo que enfrenta cualquier proyecto de IA: la falta de datos de entrenamiento. Los modelos de lenguaje como ChatGPT aprenden de miles de millones de páginas de texto, pero aunque incluyan material matemático, su razonamiento sigue siendo estadístico. Predicen secuencias que «suenan bien», pero eso no basta en matemáticas avanzadas.
DeepMind necesitaba certeza absoluta, no aproximaciones bonitas. Para conseguirlo, recurrieron a Lean, un software que permite a los matemáticos escribir definiciones y demostraciones precisas mediante un lenguaje de programación formal.
El problema era que la mayoría de enunciados matemáticos están escritos en lenguaje natural, no en Lean. La solución: entrenar un modelo Gemini para traducir automáticamente enunciados matemáticos al lenguaje formal de Lean, generando unos 80 millones de enunciados formalizados.
Lo curioso es que las imperfecciones en estas traducciones resultaron ser una ventaja: «Hay muchas maneras de aprovechar las traducciones aproximadas», explica Hubert. Detectar errores se convirtió en un ejercicio valioso para el sistema.
Aprendiendo a pensar como un matemático
Para AlphaProof, DeepMind adaptó la arquitectura de su famoso AlphaZero, el sistema que dominó el ajedrez, Go y shogi. La idea era tratar las demostraciones matemáticas como otro juego por dominar.
«Intentábamos aprender este juego mediante prueba y error», comenta Hubert. El sistema utilizó dos componentes principales:
-
Una enorme red neuronal con miles de millones de parámetros, que aprendía a trabajar en el entorno Lean. Se le premiaba por cada enunciado demostrado y se le penalizaba por cada paso de razonamiento, incentivando así demostraciones cortas y elegantes.
-
Un algoritmo de búsqueda en árbol que exploraba todas las posibles acciones en cada paso. Como en matemáticas las posibilidades son prácticamente infinitas, la red neuronal dirigía los recursos computacionales solo hacia las ramas más prometedoras.
Después de semanas de entrenamiento, el sistema rendía bien en la mayoría de problemas de competiciones matemáticas de nivel de secundaria, pero aún le costaban los más difíciles. Para superar esta barrera, añadieron un tercer componente totalmente nuevo.
La chispa de humanidad: aprendizaje sobre la marcha
Este tercer componente, llamado Test-Time Reinforcement Learning (TTRL), imita cómo los matemáticos humanos abordan problemas especialmente difíciles.
En lugar de basarse únicamente en su base de datos de problemas, AlphaProof en modo TTRL generaba un conjunto de entrenamiento completamente nuevo basado en el problema específico que enfrentaba. Creaba infinitas variaciones del enunciado original: algunas simplificadas, otras más generales, y algunas apenas relacionadas.
Es exactamente lo que hacemos los humanos ante un problema complejo: «No lo entiendo, así que voy a probar con una versión más sencilla primero para practicar». Esto permitía a AlphaProof aprender sobre la marcha, y funcionó de maravilla.
En la Olimpiada Internacional de Matemáticas de 2024, con 42 puntos posibles distribuidos en seis problemas, AlphaProof consiguió 28 puntos, igualando a los medallistas de plata. Y lo más impresionante: resolvió el problema más difícil de todos, algo que solo consiguieron seis participantes humanos.
El precio del éxito: recursos y limitaciones
Pero no todo es perfecto. AlphaProof no funcionó completamente solo. Los humanos tuvieron que hacer compatibles los problemas con Lean antes de que el software pudiera trabajar. Además, para el cuarto problema, sobre geometría, tuvo que recurrir a AlphaGeometry 2, otra IA especializada. Por sí solo, AlphaProof habría conseguido 21 puntos, medalla de bronce.
Y luego está la cuestión del tiempo y los recursos. Mientras los participantes humanos tenían dos sesiones de cuatro horas y media, AlphaProof trabajó durante varios días utilizando múltiples unidades de procesamiento tensorial a pleno rendimiento. El componente TTRL necesitó tres días para cada uno de los tres problemas que consiguió resolver.
El equipo admite que los requisitos computacionales de AlphaProof son prohibitivos para la mayoría de grupos de investigación y matemáticos aspirantes. Hablamos de cientos de «TPU-días» por problema, un nivel de recursos que solo una empresa como Google puede permitirse.
¿Estamos ante un investigador matemático o solo un buen estudiante?
Otra limitación importante: la Olimpiada es una competición de nivel de secundaria. Por muy difíciles que sean los problemas, se basan en conceptos matemáticos conocidos. Las matemáticas de investigación requieren inventar conceptos completamente nuevos, no solo trabajar con los existentes.
Sin embargo, el equipo de DeepMind cree poder superar estos obstáculos y optimizar AlphaProof para que consuma menos recursos. «No queremos quedarnos en las competiciones matemáticas. Queremos construir un sistema de IA que pueda contribuir realmente a las matemáticas de nivel de investigación», afirma Hubert, que planea hacer AlphaProof disponible para la comunidad investigadora mediante un programa inicial de probadores de confianza.
¿Qué significa esto para el futuro de la IA y las matemáticas?
Lo que hace especial a AlphaProof no es solo su capacidad de resolver problemas matemáticos complejos, sino cómo lo hace. A diferencia de un detector de IA tradicional, que busca patrones estadísticos, AlphaProof int
