DeepMind alcanza nivel de plata en la Olimpiada Matemática con IA
AlphaProof y AlphaGeometry 2 resolvieron cuatro de los seis problemas de la Olimpiada Internacional de Matemáticas de 2024. Sus 28 puntos equivalen a una medalla de plata y quedaron a uno del corte de oro.
Google DeepMind ha llevado sus sistemas de razonamiento matemático a un resultado inédito en la Olimpiada Internacional de Matemáticas (IMO), la competición más exigente del mundo para estudiantes de secundaria. AlphaProof y AlphaGeometry 2 resolvieron cuatro de los seis problemas de la edición de 2024 y sumaron 28 puntos sobre 42: una puntuación equivalente a medalla de plata.
El umbral de oro en la competición celebrada este año era de 29 puntos. La distancia numérica parece mínima, pero conviene mantener la escala: no se trata de que una sola IA haya competido como un alumno bajo las condiciones habituales, sino de dos sistemas especializados que abordaron problemas distintos y cuyos resultados fueron evaluados con el estándar de la IMO.
Cuatro problemas de seis, con demostraciones verificables
Cada problema de la Olimpiada vale siete puntos y exige una demostración, no solo el resultado correcto. DeepMind afirma que AlphaProof resolvió dos ejercicios de álgebra y uno de teoría de números, mientras que AlphaGeometry 2 resolvió el problema de geometría. Las soluciones fueron calificadas por coordinadores de la Olimpiada, siguiendo el sistema de puntuación de la prueba.
Ese detalle diferencia este avance de muchos resultados llamativos de los modelos de lenguaje. Un chatbot puede producir una explicación matemática convincente y, aun así, contener un salto lógico o una operación falsa. AlphaProof trabaja de otra manera: busca demostraciones expresadas en Lean, un lenguaje formal que permite verificar cada paso con un programa.
Una demostración formal es, en la práctica, una prueba escrita en una notación que el ordenador puede comprobar sin ambigüedades. Si falta una condición o un paso no se deduce de los anteriores, el verificador la rechaza. El precio es que el problema debe estar traducido previamente a ese lenguaje formal, una tarea que sigue requiriendo conocimiento matemático y técnico.
De AlphaGo a la demostración de teoremas
AlphaProof parte de una idea conocida en DeepMind desde AlphaGo: aprender mediante refuerzo. En lugar de elegir jugadas en un tablero, el sistema explora pasos de razonamiento hasta encontrar una secuencia que concluya una prueba válida. La compañía lo entrenó con grandes colecciones de problemas matemáticos formalizados y generó nuevos problemas para ampliar ese entrenamiento.
AlphaGeometry 2 tiene otro diseño. Combina un modelo neuronal, útil para proponer construcciones y relaciones geométricas, con un motor simbólico que aplica reglas explícitas. La combinación importa porque la geometría olímpica suele exigir descubrir una idea auxiliar —por ejemplo, una línea o una circunferencia que no aparece en el enunciado— y después encadenar deducciones exactas.
El resultado mejora el nivel que DeepMind había mostrado con AlphaGeometry a comienzos de 2024. Entonces, el sistema resolvía una parte relevante de los problemas geométricos históricos de la IMO; ahora la compañía presenta una actuación conjunta que se acerca a las medallas más altas de la prueba completa.
Un hito real, pero no una matemática generalista
La comparación con una medalla debe leerse con precisión. Los participantes humanos reciben los enunciados en lenguaje natural, disponen de dos jornadas de examen y elaboran sus respuestas sin contar con una traducción formal preparada. AlphaProof, en cambio, necesita que el ejercicio se exprese en Lean antes de iniciar la búsqueda. Además, DeepMind repartió la prueba entre sistemas diseñados para áreas concretas.
Por eso este anuncio no prueba que una IA tenga la flexibilidad matemática de un olimpista, ni mucho menos que pueda investigar de forma autónoma. Sí demuestra algo importante: los métodos de IA ya pueden producir demostraciones rigurosas de problemas que hasta hace poco se consideraban un terreno reservado a razonadores humanos muy entrenados.
La utilidad más inmediata está fuera de las olimpiadas. Herramientas como AlphaProof podrían ayudar a formalizar teoremas, detectar errores en pruebas largas y asistir a investigadores en áreas donde la verificación exacta es crucial. El siguiente reto será reducir la dependencia de la formalización manual y lograr que estos sistemas comprendan mejor los enunciados y las ideas matemáticas expresadas en lenguaje ordinario.
