Alphaproof, la IA de Google, ha conseguido la medalla de plata en la Olimpiada internacional de matemáticas

Madrid

El primer problema de este año de la IMO, la Olimpiada Internacional de Matemáticas, era este: "Determina todos los números reales α tales que, para cada entero positivo n, el número ⌊α⌋+⌊2α⌋+⋯+⌊nα⌋ es múltiplo de n". Si, tras leer el titular, ha pensado que conseguir la medalla de plata en una prueba así era una cosa menor, por favor, reevalúe su posición.

La IMO es, desde 1959, el mayor desafío intelectual para estudiantes de secundaria de todo el mundo. Cada año, los mejores jóvenes matemáticos del mundo se enfrentan a seis problemas que exigen creatividad, razonamiento y una comprensión profunda de lo que tienen entre manos. Resolver uno de los problemas es un logro gigante. Conseguir una medalla está al alcance de muy pocos.

Lo que ha logrado AlphaProof —uno de los sistemas de inteligencia artificial desarrollados por Google DeepMind— es resolver tres de los cinco problemas no geométricos del IMO 2024, "incluido el más difícil del concurso”. A la vez, otra IA complementaria, llamada AlphaGeometry 2, ha resuelto el de geometría.

Google ya lo había anunciado a través de su blog sobre Inteligencia artificial pero ahora lo hace a través de una publicación en Nature. Dice que "juntando los esfuerzos de computación de las dos IAs", "ambos sistemas han conseguido una puntuación equivalente a la de un medallista de plata". Es la primera vez que una IA logra un rendimiento de nivel "olímpico". Es la primera vez que vemos a un agente de IA con "estrategias de razonamiento matemático complejas".

La clave es el "razonamiento formal"

El estudio explica que AlphaProof hace lo que se llama un "aprendizaje por refuerzo" que garantiza que va haciendo una "corrección lógica de cada paso". Su motor de razonamiento está inspirado en otro sistema llamado AlphaZero, que fue noticia porque aprendió a jugar al ajedrez desde cero. En este caso, en lugar de aprender a mover piezas, esta IA aplica “tácticas matemáticas” verificadas automáticamente, lo que elimina el riesgo de errores o “alucinaciones” que sí están presentes en los modelos de lenguaje.

Para entrenarlo, los investigadores generaron 80 millones de problemas matemáticos a partir de textos matemáticos en lenguaje natural, y dedicaron miles de unidades de procesamiento durante semanas de aprendizaje. El resultado es un agente capaz de “descubrir demostraciones formales complejas y estrategias de razonamiento generalizadas”, algo que antes se consideraba fuera del alcance de las IAs

Siguen las mejoras

El propio artículo de Nature reconoce que AlphaProof todavía tiene limitaciones. Por ejemplo, el tiempo que tardó en responder: dos o tres días por problema en una prueba que los participantes tienen que terminar, completa, en cuatro horas y media. Otra limitación es el gigantesco entrenamiento que requiere: “decenas de miles de TPU al día”

En todo caso, los autores confían en que su trabajo “pavimente el camino hacia una herramienta de IA fiable en la resolución de problemas matemáticos complejos” y anuncian planes para “desarrollar herramientas interactivas” que hagan accesible el sistema a la comunidad científica.

Lo que opinan los matemáticos

En declaraciones a Science Media Center, Carles Sierra, profesor de investigación del CSIC, destaca que “AlphaProof parece un sistema potente porque da garantías formales de las pruebas, no ‘alucina’ como los LLMs”. Para Sierra, este trabajo “representa un avance conceptual fundamental: demuestra que los modelos de razonamiento pueden alcanzar la verificación formal, eliminando el riesgo de alucinaciones que afecta a otros sistemas de IA”. No obstante, advierte que “hay que saber usarlo: si el sistema formal (Lean) tiene axiomas inconsistentes, producirá ‘verdades formales’ pero matemáticamente falsas”.

Ramón López de Mántaras, pionero de la IA en España, lo califica como “un resultado excelente”, pero subraya que “requiere considerable pericia humana para su formalización y una enorme potencia computacional”. Aunque reconoce que AlphaProof “demuestra que los problemas formalizables mediante aprendizaje por refuerzo empiezan a ser accesibles para la IA”, recuerda que “estos logros no significan que la IA sea comparable a un matemático, ya que no ‘entiende’ los conceptos ni puede crear soluciones completamente nuevas”. En su opinión, el sistema será “una herramienta valiosa para los investigadores humanos”, pero no un sustituto.

Marta Macho-Stadler, matemática de la Universidad del País Vasco, resalta que AlphaProof resolvió correctamente “tres problemas de álgebra y teoría de números, pero no consiguió solucionar los de combinatoria”, y que el proceso “requirió dos o tres días” por problema. “Existen problemas matemáticos complejos que precisan de grandes dosis de creatividad —añade—, y la creatividad es una capacidad humana”.

Por su parte, Teodoro Calonge, profesor de Informática en la Universidad de Valladolid, destaca que “esta situación obligará a los examinadores a ser más imaginativos a la hora de proponer problemas”, ya que la IA puede aprovechar bases de datos de ejercicios previos para encontrar soluciones plausibles.