Google presenta AlphaProof, la primera IA capaz de ganar una medalla en la Olimpiada Internacional de Matemáticas

Pero esa 'fortaleza' acaba de caer, y la 'frontera' entre hombres y máquinas se ha movido de forma dramática. Lo ha conseguido, de nuevo, Google DeepMind, la división de investigación de IA de Google, la misma que ya nos deslumbró con hitos como AlphaGo, que en 2016 derrotó al campeón del célebre juego milenario, y AlphaFold, un sistema capaz de predecir, en segundos en vez de en años, la compleja estructura de las proteínas.

Ahora, los investigadores de DeepMind acaban de presentar en 'Nature' su nueva creación, AlphaProof, un revolucionario motor de razonamiento que no solo es capaz de probar teorías matemáticas complejas, sino que ha alcanzado un rendimiento que habría sido digno de una medalla de plata en la Olimpiada Internacional de Matemáticas (IMO) de 2024. Una hazaña sin precedentes.

La IMO, en efecto, es la competición de matemáticas de nivel preuniversitario más importante y exigente del mundo, donde solo los jóvenes genios más brillantes consiguen destacar. Lograr una medalla en este certamen es toda una proeza, y que una IA lo consiga, no ya simulando un razonamiento, sino produciendo pruebas verificables y correctas, es, como afirma uno de los autores del estudio, un verdadero 'alunizaje' en el campo de la IA.

El nuevo sistema, de hecho, logró resolver correctamente tres de los cinco problemas no geométricos que se plantearon en la IMO de 2024, entre ellos el que fue catalogado como el más difícil de toda la competición. Si Alpha Proof hubiera competido realmente, habría ganado una medalla de plata. Nunca hasta ahora una IA había llegado a un nivel parecido.

No obstante, tal y como señala Marta Macho-Stadler, del departamento de Matemáticas de la Universidad del País Vasco, que no ha participado en el estudio, es necesario poner este logro en perspectiva. Y es que la IA necesitó hacer un esfuerzo computacional inmenso durante varios días para lograr este resultado, algo que un participante humano debe hacer en un tiempo muchísimo más corto. Además, señala la investigadora, aunque AlphaProof brilló en el álgebra y la teoría de números, tuvo dificultades con los dos problemas de combinatoria: «entiendo que existen problemas matemáticos complejos que requieren no solo de 'entrenamiento' (a base de estudio y ensayo) para llegar a solucionarlos, sino que precisan de grandes dosis de creatividad. Y la creatividad es una capacidad humana».

¿Pero cómo ha logrado DeepMind este avance? Según el estudio, la clave de AlphaProof reside en su arquitectura y, sobre todo, en su adhesión al 'rigor formal', algo que lo distingue radicalmente de los Grandes Modelos de Lenguaje (LLM) más conocidos. Y si bien es cierto que los LLM ya han mostrado capacidades prometedoras para generar textos que parecen pruebas matemáticas, no hay que olvidar que operan sobre lenguaje natural (informal). Es decir, que el gran riesgo de los LLM es la tristemente célebre 'alucinación'. O dicho de otra manera, pueden generar contenido plausible pero lógicamente incorrecto, lo cual en matemáticas es un fallo garrafal.

En este sentido, tal y como explica Carles Sierra, del Consejo Superior de Investigaciones Científicas (CSIC), AlphaProof representa un avance fundamental porque «da garantías formales de las pruebas, no 'alucina' como los LLMs». En otras palabras, su arquitectura garantiza que cada resultado sea lógicamente sólido y, sobre todo, comprobable. La solidez del nuevo sistema, en efecto, es que no trabaja en el resbaladizo terreno del lenguaje natural, sino que opera dentro de un entorno formal de software conocido como 'Lean', un asistente interactivo de pruebas donde una demostración se expresa en un formato que el ordenador puede verificar automáticamente. El sistema, de hecho, transforma las matemáticas en un dominio interactivo y verificable, permitiendo que el razonamiento subyacente se simule y se aprenda.

Según el estudio, AlphaProof trata la prueba matemática como si se tratara de una especie de juego de toma de decisiones. Es un agente que aprende a encontrar pruebas formales mediante Aprendizaje por Refuerzo (RL) y cuyo entrenamiento fue masivo. Para los problemas más difíciles, el sistema aplica la llamada 'Test-Time RL', una técnica muy costosa en términos de computación pero que le permite generar y aprender millones de variantes de un mismo problema y lograr así adaptarse para hallar la solución final.

El físico e informático Ramón López de Mántaras, del CSIC y uno de los mayores expertos españoles en Inteligencia Artificial, reconoce que se trata de «un resultado excelente y demuestra que problemas matemáticos formalizables mediante aprendizaje por refuerzo (...) empiezan a ser accesibles para la IA». Sin embargo, aterriza la euforia tecnológica con una serie de puntos que definen la frontera actual de estos sistemas.

En primer lugar, subraya López de Mántaras, los éxitos de AlphaProof se han dado principalmente en «matemáticas de nivel avanzado de secundaria y pregrado, que operan dentro de un conjunto conocido y relativamente fijo de conceptos». Motivo por el cual el verdadero salto cualitativo, la investigación matemática avanzada, sigue siendo una quimera: «Extender estas capacidades a la investigación matemática avanzada, que implica la creación de teoría y la incorporación de nuevos conceptos, sigue siendo un desafío monumental y no hay indicios de que pueda lograrse no ya a corto plazo, sino ni siquiera a medio plazo.»

Lo cual es, según el científico, el punto central de la cuestión. La capacidad de AlphaProof, en efecto, es de demostración y exploración dentro de un espacio de soluciones predefinido, no de invención. «Estos logros - afirma- no significan que la IA sea comparable a un matemático, ya que no 'entiende' en absoluto los conceptos matemáticos ni puede crear soluciones para problemas completamente nuevos.» Lo cual convierte a AlphaProof en un buen asistente para los matemáticos, pero no en un sustituto.

A ello se añade el ya mencionado hecho de que se necesita una gran infraestructura para alcanzar este nivel de rendimiento, y eso plantea serias preguntas sobre la democratización de la ciencia. «La fase de aprendizaje específica de AlphaProof -dice López de Mántaras- requiere un nivel de entrenamiento muy especializado y costoso. Resolver los problemas más difíciles puede tomar varios días de inferencia.» Algo que por ahora está fuera del alcance de la mayoría de los investigadores.

En definitiva, parece que sistemas como AlphaProof, a pesar de su novedad y capacidades, no vienen a sustituir a los matemáticos de carne y hueso, sino más bien a ser una valiosa herramienta para ellos, como lo es un telescopio para los astrónomos, algo que les permitirá ir más deprisa y hacer nuevos hallazgos. Y si bien es cierto que el nuevo sistema de Google DeepMind acaba de lograr un hito comparable al de llegar a la Luna en cuanto a la IA se refiere, sigue siendo solo el principio de una colaboración en la que, por lo menos por ahora, la creatividad humana seguirá dirigiendo la potencia lógica de las máquinas en busca de objetivos cada vez más ambiciosos.