La IA en la investigación matemática

En esta entrada reflexionaremos sobre el papel que la IA ha ido desempeñando en la propia investigación matemática, inspirados en el reciente artículo de Terence Tao en los Notices of the American Mathematical Society.

Usar instrumentos para facilitar sus cálculos ha sido siempre una ocupación de los matemáticos, culminada con la invención de los ordenadores y programas que son capaces no sólo de dar aproximaciones numéricas (MatLab), sino también de realizar cálculos simbólicos (Mathematica). Es más, con los ordenadores se han podido desarrollar las llamadas demostraciones asistidas por ordenador. Se usa algún programa para comprobar todos los casos posibles, lo que a mano no seríamos capaces de decidir en años. Dos ejemplos paradigmáticos han sido la prueba en 1976 del teorema de los cuatro colores («dado cualquier mapa geográfico con regiones continuas, éste puede ser coloreado con cuatro colores diferentes o menos, de forma que no queden regiones adyacentes con el mismo color») y la conjetura de Kepler («si apilamos esferas iguales, la densidad máxima se alcanza con un apilamiento piramidal de caras centradas»). El primer problema fue resuelto por Kenneth Appel y Wolfgang Haken, mientras que el segundo se debe a Thomas Hales, en 1998. En este último caso, la comunidad matemática expresó dudas sobre la validez de un teorema demostrado usando un programa de ordenador.

Como señala José Bonet (Demostraciones matemáticas y el ordenador, Real Academia de Ciencias de España, 2024): «Las principales objeciones a este tipo de pruebas son la posibilidad de errores en la programación y, sobre todo, la gran dificultad de entender y verificar estas demostraciones obtenidas por el ordenador».

En su artículo, Tao sugiere una serie de aplicaciones que ayudarían en la investigación matemática y que reproducimos textualmente:

– Los algoritmos de aprendizaje automático pueden utilizarse para descubrir nuevas relaciones matemáticas o generar ejemplos potenciales o contraejemplos de problemas matemáticos.

– Los asistentes de pruebas formales pueden utilizarse para verificar pruebas (así como la salida de grandes modelos de lenguaje), permitir colaboraciones matemáticas a gran escala y ayudar a construir conjuntos de datos para entrenar a los algoritmos de aprendizaje automático antes mencionados.

– Los modelos de lenguaje de gran escala, como ChatGPT, pueden utilizarse (potencialmente) para facilitar y agilizar el uso de otras herramientas; también pueden sugerir estrategias de demostración o trabajos relacionados, e incluso generar pruebas (sencillas) de forma directa.

Se avecina un futuro con tiempos interesantes, pero no está de más recordar aquí esta reflexión de G.H. Hardy. Cuando en 1928 David Hilbert planteó el siguiente problema: encontrar un procedimiento general que permita probar o refutar cualquier proposición matemática, es decir, mecanizar todas las matemáticas, Hardy escribió:

“Supongamos, por ejemplo, que pudiéramos encontrar un sistema finito de reglas que nos permitiera decir si una fórmula dada es demostrable o no. Este sistema constituiría un teorema metamatemático. Por supuesto, no existe tal teorema, lo cual es muy afortunado, ya que si existiera tendríamos un conjunto mecánico de reglas para la solución de todos los problemas matemáticos, y nuestras actividades como matemáticos llegarían a su fin.”

De momento, los matemáticos seguimos con nuestros trabajos y somos cada vez más necesarios para desentrañar las cajas negras que generan la IA. Confiemos en el futuro.

Nota: Esta entrada es parte de un artículo completo que se puede encontrar aquí.

_____________

Manuel de León (CSIC, Fundador del ICMAT, Real Academia de Ciencias, Real Academia Canaria de Ciencias, Real Academia Galega de Ciencias).