La 61a Olimpiada Internacional de Matemática (OIM) empezó el 21 de septiembre y acaba de terminar. Puede que pase a la historia por al menos dos razones: por la pandemia de la COVID-19 es la primera vez que se celebra vía remota y quizá sea la última en que no compite una inteligencia artificial (IA).
Para los investigadores, es el campo de pruebas ideal para unas máquinas diseñadas de modo que piensen como un ser humano. Si un sistema de IA destaca ahí, habrá alcanzado una dimensión importante de la cognición humana. «La OIM representa para mí el tipo más difícil de problema que se puede enseñar a una persona inteligente a resolver con cierta fiabilidad», dice Daniel Selsam, de Microsoft Research. Selsam es el fundador del Gran Reto OIM, cuyo objetivo es entrenar a un sistema de IA para que gane una medalla de oro en la más importante de las competiciones matemáticas mundiales.
Desde 1959, la OIM ha reunido a los mejores estudiantes de matemáticas preuniversitarios. En cada uno de los dos días de la competición, los participantes tienen cuatro horas y media para resolver cuatro problemas de dificultad creciente. Ganan hasta siete puntos por problema; los que más suman ganan medallas, como en los Juegos Olímpicos. Los participantes más condecorados en las OIM se convierten en leyendas entre los matemáticos. Algunos llegaron luego a ser matemáticos investigadores superlativos.
Los problemas de la OIM son simples, pero solo en el sentido de que no requieren matemáticas avanzadas. También son endiabladamente difíciles. Por ejemplo, este es el quinto problema de la competición de 1987, que se celebró en Cuba:
Sea un entero n mayor o igual que 3. Demuéstrese que hay un conjunto de n puntos del plano tales que la distancia entre dos cualesquiera de ellos es irracional y cada conjunto de tres puntos determina un triángulo no degenerado de área racional.
Como muchos problemas de la OIM, este puede parecer imposible a primera vista. «Lees la pregunta y piensas que no puedes con ella», dice Kevin Buzzard, del Colegio Imperial de Londres, miembro del Gran Reto OIM y ganador de la medalla de oro en la OIM de 1987. «Son preguntas dificilísimas, accesibles a los alumnos de bachillerato si conjugan con brillantez todas las ideas que saben».
Resolver los problemas de la OIM suele requerir un destello de ingenio, un primer paso trascendente que para las inteligencias artificiales de hoy resulta difícil, cuando no imposible.
Por ejemplo, uno de los resultados más antiguos de las matemáticas es la prueba que Euclides enunció hace unos 2300 años de que hay infinitos números primos. Empieza por constatar que siempre se puede encontrar un nuevo número primo multiplicando todos los conocidos y sumando uno al resultado. A partir de ahí la prueba es simple, pero haber dado con la primera idea hacia ella fue arte.
«No se puede hacer que los ordenadores den con ella», dice Buzzard, o al menos no por ahora.
El equipo del Gran Reto OIM se vale de un progama informático llamado Lean. Lo sacó un investigador de Microsoft, Leonardo de Moura, en 2013. Lean es un «ayudante para demostraciones» que comprueba el trabajo de los matemáticos y automatiza algunas de las partes más tediosas de escribir una prueba.
De Moura y sus colaboradores quieren usar Lean como un «solucionador», capaz de concebir sus propias pruebas de los problemas de la OIM. Pero en estos momentos ni siquiera entiende los conceptos que aparecen en algunos de esos problemas. Para que mejore hay que cambiar dos cosas.
La primera es que Lean tiene que saber más matemáticas. El programa bebe de mathlib, una biblioteca de matemáticas que no para de crecer. Hoy contiene casi todo lo que un estudiante de matemáticas sabe al final del segundo año de la carrera, pero con lagunas elementales que tienen su importancia en la OIM.
La segunda tarea, de mayor magnitud, consiste en enseñarle a Lean lo que tiene que hacer con los conocimientos que tiene. El equipo del Gran Reto OIM quiere entrenarle a enfocar una demostración matemática tal y como las IA ya enfocan, y con éxito, juegos complicados (el ajedrez, el Go): siguiendo un árbol de decisiones hasta que se encuentra el mejor movimiento.
«Si podemos conseguir que un ordenador llegue a la idea brillante por el mero hecho de que tiene miles y miles de ideas y las rechaza todas hasta que tropieza con la buena, quizá podamos vencer en el Gran Reto OIM», dice Buzzard.
Pero ¿qué son las ideas matemáticas? Es sorprendente lo difícil que resulta decirlo. A un nivel alto, mucho de lo que hacen los matemáticos cuando abordan un problema nuevo es inefable.
«Un paso clave en muchos problemas consiste básicamente en jugar con el problema y buscar patrones», según Selsam. Claro está, no es evidente cómo se le dice a un ordenador que «juegue» con un problema.
A un nivel bajo, las demostraciones matemáticas son solo una serie de pasos muy concretos y lógicos. Los investigadores del Gran Reto OIM podrían intentar entrenar a Lean mostrándole con todo detalle demostraciones anteriores de la OIM, pero en ese nivel granular las pruebas individuales están demasiado especializadas en el problema dado.
«No hay nada que funcione en el problema siguiente», explica Selsam.
Para salir del atolladero, el equipo del Gran Reto OIM necesita que primero unos matemáticos escriban demostraciones formales detalladas de los problemas anteriores de la OIM. El equipo tomará entonces esas pruebas e intentará destilar las técnicas, o estrategias, que hacen que funcionen. A continuación, entrenarían a un sistema de IA para que busque entre esas estrategias una combinación «ganadora» que resuelve problemas de la OIM que no ha visto antes. El quid, observa Selsam, está en que ganar en matemáticas es mucho más arduo que ganar incluso en los juegos de mesa más complicados. En estos, al menos se sabe cuáles son las reglas a que hay que atenerse.
«Puede que en el go el objetivo sea encontrar el mejor movimiento, mientras que en matemática consiste en encontrar la mejor partida y a continuación el mejor movimiento en esa partida», dice.
El Gran Reto OIM es actualmente una apuesta arriesgada. Si Lean hubiese participado en la competición de este año, «seguramente habríamos sacado un cero», dice De Moura.
Pero los investigadores tienen unos criterios que sirven de referencia e intentarán satisfacerlos antes del certamen del año que viene. Tienen pensado colmar los huecos de mathlib de modo que Lean pueda entender todas las preguntas. También esperan contar con las demostraciones detalladas formalizadas para docenas de problemas de la OIM anteriores; con ellas empezará el proceso de ofrecer a Lean un manual básico de formas de jugar para que se prepare con él.
Puede que en ese momento la medalla de oro esté aún muy lejos, pero al menos Lean podría ya participar.
Según Selsam, «ahora mismo están pasando un montón de cosas, pero no hay nada en concreto que pueda señalarse de un modo particular. El año [que viene] se convertirá en un auténtico empeño».
Kevin Hartnett / Quanta Magazine
Artículo traducido por Investigación y Ciencia con el permiso de QuantaMagazine.org, una publicación independiente promovida por la Fundación Simons para potenciar la comprensión pública de la ciencia.
Más información en la hoja Web de la Olimpiada Internacional de Matemática y del Gran Reto IMO.
