Un sistema de IA lograría una medalla en la Olimpiada Internacional de Matemáticas, según un estudio

El artículo presenta un sistema de IA (AlphaProof) que, a diferencia de otros sistemas, añade un método de verificación para comprobar la corrección de sus resultados. Según explican los autores, AlphaProof (como otros sistemas de IA) ‘aprende’ encontrando demostraciones de problemas matemáticos (y variantes de ellos) para adaptarlos y hallar la solución de cada cuestión planteada. Además (y esta es la principal mejora), es capaz de perfeccionar sus resultados mediante un sistema de ensayo y error que ayuda a optimizar las soluciones.  

Han probado la eficacia de este sistema en un concurso matemático de élite (Olimpiadas Internacionales de Matemáticas 2024). De los seis problemas planteados en esta competición, AlphaProof resolvió correctamente tres problemas de álgebra y teoría de números, pero no consiguió solucionar los dos de combinatoria. El sistema AlphaGeometry 2 resolvió el problema de geometría. Todo esto se realizó en un tiempo muy superior (dos o tres días) al de un participante humano.   

Es probable que en poco tiempo mejoren las capacidades (en términos de velocidad y tipo de problemas solucionados correctamente) de estos sistemas de IA. De todos modos, entiendo que existen problemas matemáticos complejos que requieren no solo de ‘entrenamiento’ (a base de estudio y ensayo) para llegar a solucionarlos, precisan de grandes dosis de creatividad. Y la creatividad es una capacidad humana.

La impresión general es que es un artículo con cierto rigor científico, lo que hará que muchas personas fuera de la Ingeniería Informática se queden en la capa más superficial, esto es, en las aplicaciones. Respecto a la calidad, me parece que es un trabajo digno dada la situación de la IA, en donde o tienes unos recursos de cómputo ‘infinitos’ o no serás capaz de desarrollar un prototipo de principio a fin. Y esto es lo que le pasa a este grupo de investigadores, que han usado modelos preentrenados y que posteriormente han desarrollado una capa de adaptación a su problema particular. Aunque pueda sonar a ‘fraudulento’, si se aclara —como honradamente hacen los autores— no hay problema ninguno. La bibliografía científica al respecto está plagada de este tipo de trabajos con este planteamiento. 

Respecto a las implicaciones, creo que esto nos obligará a los examinadores a ser más imaginativos a la hora de proponer problemas. Me explico: la ley del mínimo esfuerzo nos lleva a poner ejercicios basados en anteriores con ligerísimas variaciones. Y aquí es donde entra la IA, que se aprovecha de una vasta base de ejercicios y efectuando pequeñas modificaciones lleva a soluciones que pudieran ser aceptables, incluso a primera vista sorprendentes. Ahora bien, si la solución a un ejercicio propuesto no se parece en absoluto a lo que tiene en sus bases de datos, o si se da esa semejanza pero no tanto, la IA generativa es muy probable que falle.  

Huyendo del sensacionalismo relativo a la Olimpiada de Matemáticas, creo que esto es lo que realmente hay detrás de este trabajo, que podría resumir que es aceptable, al igual que mucha de la IA generativa que se está ofreciendo comercialmente en ámbitos muy específicos como derecho, seguros, informes médicos, etc.

Es muy raro que un artículo en Nature no cumpla con los más altos estándares de calidad. Si ha pasado el complicado sistema de revisión por pares (personas más especializadas en el tema que yo) es casi seguro que la calidad del trabajo está en el nivel más alto. 

La IA va ocupando y sobrepasando cada vez más parcelas del conocimiento humano. Esto lo ilustra muy bien el investigador Hans Moravec, tal y como dice Max Tegmark en su libro Vida 3.0 sobre la IA: un panorama de competencias humanas se puede visualizar como un paisaje con sus llanuras y sus montañas, las llanuras o los valles serían las habilidades humanas que son más fáciles para un ordenador, “como «aritmética» y «memorización», laderas como «demostración de teoremas» y «ajedrez» y elevados picos montañosos con nombres como «locomoción», «coordinación entre ojo y mano» e «interacción social». El avance del rendimiento de los ordenadores es como la lenta crecida de las aguas. Hace medio siglo, empezó a inundar las tierras bajas, expulsando a las calculadoras humanas y a los funcionarios de registros, pero permitiendo que la mayoría aún permaneciésemos secos. Ahora las aguas han llegado a las laderas, y los puestos fronterizos que tenemos allí están barajando retirarse. Nos sentimos a salvo en nuestros picos, pero, a la velocidad actual, estos también acabarán sumergidos dentro de otro medio siglo” y en ese momento la IA habrá superado todas las capacidades cognitivas humanas. 

[En cuanto a posibles limitaciones] Casi todo lo contrario: en el caso del artículo que se menciona, lo cierto es que las Olimpiadas Matemáticas están enfocadas a un tipo de problemas muy especiales que requieren relativamente poco bagaje matemático, pero gran uso de dichos conocimientos y mucho ingenio. Supongo que adquirir mayor cantidad de conocimiento matemático debe de ser relativamente sencillo para una máquina y lo que siempre se ha considerado más humano, que es el ingenio, es lo que ha demostrado este trabajo: que una IA puede alcanzarlo.

Se trata de un resultado excelente. Demuestra que aquellos problemas matemáticos formalizables mediante aprendizaje por refuerzo (combinado con otras técnicas, como por ejemplo un demostrador interactivo de teoremas y un potente algoritmo de búsqueda para explorar el espacio de posibles demostraciones) empiezan a ser accesibles para la IA, aunque es importante tener en cuenta que requieren considerable pericia humana para su formalización y una enorme potencia computacional.  

Existen, además, otras importantes limitaciones. La fase de aprendizaje específica de AlphaProof requiere un nivel de entrenamiento especializado y costoso. Resolver los problemas más difíciles puede tomar varios días de inferencia, lo que evidencia la necesidad de estrategias más eficientes.  

Hasta ahora, los éxitos del sistema 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. 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 que ni siquiera a medio plazo. En otras palabras, estos logros 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 que AlphaProof demuestra es una notable ampliación de las herramientas automáticas que pueden asistir a los matemáticos humanos, pero nunca sustituirlos. A pesar de ello, cabe esperar que AlphaProof se convierta a largo plazo en una herramienta valiosa para los investigadores humanos, abriendo nuevas posibilidades para explorar los límites del conocimiento, pero siempre como herramienta que solamente será útil para aquellos con conocimientos profundos de matemáticas.  

Los elevados requerimientos computacionales también plantean dudas sobre la reproducibilidad y el acceso a este tipo de avances, lo cual es un serio hándicap en ciencia. Es por eso que los responsables de AlphaProof plantean desarrollar herramientas interactivas para el acceso a este sistema y también tienen como objetivo mejorar la eficiencia algorítmica, reduciendo las barreras de entrada y convirtiendo estas técnicas en recursos colaborativos para la comunidad matemática.

AlphaProof parece un sistema potente porque da garantías formales de las pruebas, no ‘alucina’ como los LLMs [Grandes Modelos de Lenguaje]. AlphaProof representa un avance conceptual fundamental: demuestra que los modelos de razonamiento pueden alcanzar la verificación formal, eliminando el riesgo de alucinaciones factuales que afecta a otros sistemas de IA.  

A diferencia de los modelos de lenguaje que pueden generar contenido plausible pero incorrecto, su arquitectura garantiza que cada inferencia sea lógicamente sólida y comprobable (esto es un aspecto fundamental del sistema). Pero hay que saber usarlo. Por ejemplo, si el sistema formal (Lean) tiene axiomas inconsistentes, producirá ‘verdades formales’ pero matemáticamente falsas. El artículo no describe con excesivo detalle el sistema, sino los resultados de la olimpiada. Yo destacaría el hecho de la verificación formal y que no ‘alucina’ como los LLMs.