Una IA de Google investiga de forma autónoma y resuelve nueve problemas matemáticos de hace décadas

Desde principios de año los progresos de la inteligencia artificial en matemáticas se suceden uno tras otro.

Si el miércoles, OpenAI afirmaba que su modelo avanzado ha resuelto cientos de problemas matemáticos, este jueves un equipo de Google DeepMind presenta en la revista 'Science' un nuevo sistema basado en grandes modelos de lenguaje capaz de investigar de forma autónoma (hasta cierto punto) y comprobar, paso a paso, que sus demostraciones no contienen errores.

Llamado AlphaProof Nexus, ha resuelto nueve problemas de la célebre colección de Paul Erdős que llevaban décadas sin respuesta —dos de ellos, desde hace 56 años— y otras 44 conjeturas abiertas de la Enciclopedia en Línea de Secuencias de Enteros (OEIS), con un coste de unos pocos cientos de dólares por problema.

AlphaProof Nexus, cuyos resultados fueron adelantados en mayo en el depositorio Arxiv , escribe sus demostraciones en un lenguaje matemático formal llamado Lean.

Y Lean comprueba automáticamente, paso a paso, que la propuesta es correcta.

De esta forma, el ordenador actúa como un árbitro estricto: si la prueba tiene flecos pendientes, no es correcta y la IA debe proponer otra estrategia.

El sistema puede repetir este proceso miles de veces, explorando diferentes caminos hasta encontrar uno que funcione.

Los investigadores seleccionaron 353 problemas abiertos de Erdős, uno de los matemáticos más prolíficos del siglo XX.

El sistema consiguió resolver nueve que han supuesto un quebradero de cabeza para los investigadores durante décadas.

Dos de ellos tienen 56 años.

Además, la IA fue probada con 492 conjeturas abiertas de la OEIS, la enorme base de datos de secuencias de números enteros.

Encontró demostraciones formales para 44.

Los investigadores revisaron manualmente esos resultados y comprobaron que todas las demostraciones estaban correctamente formalizadas y que eran válidas y previamente no demostradas.'Sorry'Según DeepMind, su agente no se limitó a copiar demostraciones existentes, sino que investigó por sí mismo.

También probaron el sistema con cuatro problemas abiertos de geometría algebraica, de los que resolvió dos.