IA. El sistema AlphaProof formaliza millones de enunciados y verifica cada paso, lo que que permite comprobar y desmostrar por qué acierta.
Una inteligencia artificial ha logrado algo que hasta ahora pertenecía al terreno de los estudiantes más brillantes del mundo: competir, con resultados comparables a una medalla de plata, en la Olimpiada Internacional de Matemáticas (IMO). El trabajo, publicado en Nature y desarrollado por Google DeepMind, presenta AlphaProof, un sistema de IA que no solo resuelve problemas, sino que lo hace dentro de un entorno de matemáticas formales donde cada paso queda verificado automáticamente. Eso lo sitúa un peldaño por encima de los grandes modelos de lenguaje que «parecen» razonar, pero cuya corrección cuesta comprobar.
El punto de partida del estudio es una limitación conocida: las IAs generales pueden escribir demostraciones elegantes en lenguaje natural, casi humano, pero los matemáticos necesitan certezas. Lo que hace AlphaProof es entrenarse con una cantidad descomunal de material matemático formalizado —los autores hablan de autoformalizar unos 80 millones de enunciados— y, a partir de ahí, aprender por refuerzo qué secuencias de pasos llevan a una demostración válida y cuáles no. Como explican los investigadores, ese aprendizaje se parece más a AlphaGo que a ChatGPT: la máquina intenta, falla, corrige y vuelve a intentar hasta dar con una prueba que acepta. Así se salva el gran problema de la verificación. Vamos, el ensayo, error de toda la vida.
Probado en un terreno real, la IMO 2024, el sistema resolvió por sí mismo tres de los seis problemas (los de álgebra y teoría de números) y necesitó apoyarse en AlphaGeometry 2 para el ejercicio de geometría. El conjunto alcanzó una puntuación equivalente a la de un medallista de plata, pero con una diferencia importante: el sistema estuvo dos o tres días computando, mientras que los alumnos humanos disponen de cuatro horas. «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», recuerda Marta Macho-Stadler, matemática de la Universidad del País Vasco en declaraciones a SMC España, donde subraya el avance clave: «añade un método de verificación para comprobar la corrección de sus resultados».
Esa verificación automática es lo que entusiasma a parte de la comunidad: no es solo que la IA acierte, es que podemos comprobar por qué acierta. Pero el trabajo también muestra sus costuras. Primero, porque la demostración de fuerza se ha hecho en un tipo de problemas muy particulares —los de olimpiada—, que combinan ingenio y pequeños trucos, pero no requieren el bagaje de un curso completo de geometría algebraica. Y segundo, porque el rendimiento se apoya en una cantidad de cómputo reservada a muy pocos laboratorios. «En la situación actual de la IA, o tienes unos recursos de cómputo ‘infinitos’ o no desarrollas un prototipo de principio a fin», señala Teodoro Calonge, profesor de Informática en la Universidad de Valladolid, que valora el artículo como «digno» y bien explicado en cuanto al uso de modelos ya preentrenados.
Hay, además, una consecuencia colateral que afecta directamente a la enseñanza: si una IA es capaz de resolver variaciones de problemas vistos, los exámenes —y las olimpiadas— tendrán que volverse más creativos. Calonge lo dice sin rodeos: los docentes tienden a «poner ejercicios basados en anteriores con ligerísimas variaciones», y es justo ahí donde un sistema entrenado con millones de ejemplos brilla. Cuando el problema se aleja de lo conocido, la IA todavía patina. Ese es uno de los límites que los propios autores señalan en Nature: pasar de la competición estructurada a la matemática abierta, la que exige creatividad, sigue siendo un reto.
Esa distinción la marca también Clara Grima, profesora de Matemáticas en la Universidad de Sevilla, cuando recuerda a SMC España la metáfora de Hans Moravec —popularizada por Max Tegmark— sobre el «paisaje» de las capacidades humanas: primero cayeron las tareas de cálculo, luego las de demostración y ajedrez, y poco a poco el agua va cubriendo laderas más altas. Para esta profesora, el artículo muestra que incluso ese ingenio que atribuíamos a los adolescentes olímpicos empieza a estar al alcance de las máquinas, aunque todavía no estemos hablando de investigación matemática original ni de conjeturas abiertas.
Con todo, el trabajo de DeepMind marca una frontera clara: es posible hacer que una IA razone en matemáticas de forma controlable y verificable. A corto plazo, eso puede traducirse en asistentes que ayuden a docentes a generar ejercicios, a correctores automáticos más fiables, o a matemáticos que quieran comprobar pasos rutinarios de una prueba larga. A medio plazo, si se abarata el cómputo y se amplía el repertorio de problemas, puede convertirse en una herramienta que permita explorar ramas enteras del conocimiento formal sin depender solo de horas humanas.
Fuente: https://www.elmundo.es/
