DeepMind alcanza nivel de plata en la Olimpiada Matemática con IA

El 25 de julio de 2024, Google DeepMind comunicó que AlphaProof y AlphaGeometry 2 habían resuelto cuatro problemas de la Olimpiada Internacional de Matemáticas y obtenido 28 puntos sobre 42, nivel de plata. El informe de DeepMind también revela las condiciones que limitan la comparación: formalización manual, sistemas especializados y tiempos de hasta varios días.

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. Fuente

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. Fuente

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. Fuente

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.

La medalla es una equivalencia de puntuación

La frase correcta no es que una IA se sentó a competir como estudiante. El sistema recibió problemas formalizados por expertos, repartió áreas entre herramientas distintas y dispuso de tiempos que no coincidían con el examen humano. La puntuación permite situar la dificultad de las soluciones; no borra las diferencias del procedimiento.

Una demostración formal aporta una ventaja fuerte: el verificador comprueba que cada paso deriva de reglas aceptadas. Sin embargo, esa corrección se refiere a la traducción formal. Si el enunciado se codifica mal, puede existir una prueba impecable de otro problema. Por eso deben conservarse tanto la formalización como la correspondencia con el lenguaje original.

Cómo evaluar un sistema que razona matemáticamente

Separa formulación, búsqueda y verificación. Anota quién tradujo el problema, qué biblioteca de teoremas estaba disponible, cuánto cómputo se usó y si hubo selección entre varios intentos. Después verifica la prueba con una instalación independiente y revisa qué idea matemática descubrió el sistema, no solo que el archivo compiló.

La prueba de transferencia cambia una condición: notación, dominio o necesidad de un lema nuevo. Un sistema que memoriza patrones de una biblioteca puede rendir bien y fallar ante una formulación equivalente. Los casos inéditos y la inspección del rastro de dependencias revelan mejor la generalidad.

La capacidad transferible es leer una comparación humano-máquina por condiciones, no por metáfora. Conserva entradas, ayuda, herramientas, tiempo, verificador y criterio. La medalla sigue siendo un hito cuando se describe con precisión; exagerarla la vuelve menos informativa.

Encontrar una prueba y comprobarla son trabajos distintos

Un verificador formal puede rechazar una derivación inválida con enorme precisión, pero no encuentra por sí solo el camino hacia la solución. El sistema de búsqueda elige lemas, construye pasos y explora alternativas; el verificador decide si el resultado cumple las reglas. Mezclar ambas funciones hace parecer que la certeza del comprobador se extiende a toda la estrategia.

La comparación debe conservar los intentos fallidos. Si solo se publica la prueba elegida, no sabemos cuántas trayectorias consumió el sistema ni cómo se seleccionó la ganadora. Tiempo de cálculo, número de candidatos y ayuda humana forman parte del resultado. También hay que registrar si el problema o lemas cercanos estaban representados en los datos de entrenamiento.

La explicación sigue siendo una evaluación separada

Una prueba que compila puede ser difícil de leer para una persona. Pedir una explicación en lenguaje natural mide otra capacidad: identificar la idea central, justificar el giro decisivo y relacionarlo con conocimientos previos sin inventar pasos. La explicación se contrasta después con el objeto formal, porque una narración convincente puede no describir la demostración real.

Para usar el sistema como apoyo educativo, el criterio no es solo llegar a la respuesta. Se comprueba si ofrece una pista proporcional, detecta el punto de bloqueo del estudiante y evita revelar toda la solución de inmediato. Resolver una olimpiada y enseñar matemáticas no son la misma tarea.

El método general sirve fuera de las matemáticas: separa el generador del comprobador y pregunta qué parte admite verificación automática. Cuando no existe un verificador fuerte, la seguridad de la salida disminuye aunque el razonamiento aparente sea igual de fluido.

Un informe completo entrega enunciados, traducciones formales, pruebas, dependencias, tiempo y configuración. Eso permite a especialistas localizar el mérito y el límite sin fiarse del resumen corporativo. Si una parte no puede abrirse por seguridad o licencia, debe declararse: la imposibilidad de reproducir reduce la fuerza de la conclusión, aunque no invalide el avance observado. Publicar los fallos y problemas no resueltos evita que la muestra seleccionada funcione como una demostración comercial.