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. Uno era una conjetura de Zanello relacionada con las llamadas funciones de Hilbert. Los autores subrayan que la demostración utilizó una estrategia que, hasta donde saben, no aparece en la literatura previa.
Es decir, la IA reformuló el problema para demostrar el resultado. Los investigadores aseguran que estos cálculos se pueden conseguir con agentes básicos y que no es necesario construir sistemas cada vez más especializados. Atribuyen el éxito a la capacidad de los modelos actuales y, sobre todo, al feedback de Lean, que reduce la necesidad de supervisión humana.
Eso sí, la IA también se equivoca. Cuando los investigadores analizaron los problemas que no consiguió resolver, encontraron un comportamiento típico de los modelos de lenguaje. A veces la IA dejaba un 'sorry' escondido dentro de una demostración, una forma de reconocer que no había demostrado que un paso es cierto pero que lo soltaba por si 'colaba'.
También produjo 'alucinaciones', como afirmar que un resultado era un teorema conocido cuando, en realidad, se lo había inventado. Lean supone un cortafuego a todos estos problemas. DeepMind cree que su IA no es un rival de los matemáticos humanos , sino que, más bien al contrario, puede ayudarles en sus investigaciones.
Según dice, los matemáticos que colaboraron con los investigadores encontraron que los intentos de demostración de la IA les ayudaron a comprender mejor los problemas aunque la IA no lograra resolverlos. Como las pruebas están formalizadas, el matemático puede mirar directamente qué parte sigue sin resolverse en lugar de tener que revisar toda la demostración desde cero.El resultado de Google DeepMind supone un avance hacia sistemas capaces no solo de resolver ejercicios matemáticos, sino de participar en la investigación y descubrir nuevas demostraciones, aunque la mayoría de los problemas abiertos siguen fuera de su alcance.Problema del milenio«Este trabajo se enmarca en todo el desarrollo que se lleva haciendo con el uso de la IA en matemática, que empezó a tener sus frutos a principios de año», afirma a ABC Pablo Haya Coll, investigador del Laboratorio de Lingüística Informática de la Universidad Autónoma de Madrid.
La catarsis de esta carrera llegó en septiembre, cuando OpenAI anunció, no sin polémica , la resolución de uno de los 'problemas del milenio' , las ecuaciones de Navier-Stokes, ciencia de frontera y por cuya solución se ofrece una recompensa de un millón de dólares.Aunque considera que el anuncio de OpenAI del martes ha dejado «un poco eclipsados» los resultados de DeepMind, la compañía de San Francisco «no ha dado mucho detalle, más allá de que ha utilizado un modelo frontera interno que es mejor en matemáticas que la última versión pública».
Por el contrario, «DeepMind publica una arquitectura abierta que, de alguna manera, abre la posibilidad de replicar los resultados y se aleja de hermetismo de OpenAI». Josep Curto Díaz, director académico del Máster en Inteligencia de Negocios y Big Data en la Universidad Abierta de Cataluña (UOC), la Universitat Oberta de Catalunya (UOC), se expresa de manera similar.
Mientras "DeepMind diseña sistemas complejos e híbridos y los presenta a través de publicaciones estelares en revistas como 'Science' o ''Nature', OpenAI apuesta por la fuerza bruta del 'thinking compute' en modelos de lenguaje masivos y libera sus resultados directamente un repositorio abierto (`openai/math`) con cientos de manuscritos en PDF/LaTeX, trazas de razonamiento y código en Lean para que la comunidad matemática global los ponga a prueba y encuentre las fallas".
Además, "existen potenciales controversias en la autoría u origen de los descubrimientos. Al menos, reconocen abiertamente que sus resultados informales pueden tener errores, confían en la formalización progresiva y el contraste con la comunidad científica".Dependencia humanaA pesar de que se habla de autonomía, la IA matemática sigue teniendo "una dependencia humana estructural", según Curto Díaz.
En el caso de AlphaProof Nexus, "si el enunciado no está perfectamente formalizado por un experto, el agente puede demostrar variantes incorrectas o eludir pasos críticos declarando sub-lemas mediante el comando `sorry` y alucinando que son teoremas de la literatura.
Además, requirió reorientación humana en casos prácticos (como el problema #57 de Green) para dirigir la búsqueda hacia contraejemplos", señala.En cuanto al repositorio de OpenAI, "advierte explícitamente a los investigadores que sus resultados no formalizados en Lean pueden contener errores o fallos lógicos y requieren revisión humana o edición para ser legibles".
Como explica Curto, "ninguno de los sistemas formula las preguntas de investigación desde cero; ambos dependen de colecciones curadas por matemáticos (el catálogo de Bloom para Erdős, el OEIS o datasets de investigación)".
💬 Debate de la Comunidad 0