Hace cinco años, los matemáticos Dawei Chen y Quentin Gendron trataban de desentrañar un difícil campo de la geometría algebráica relacionado con las diferenciales, elementos del cálculo utilizados para medir distancias a lo largo de superficies curvas. Mientras trabajaban en un teorema, se encontraron con un obstáculo inesperado. Su argumento dependía de una extraña fórmula de la teoría de números, pero fueron incapaces de resolverla o justificarla. Al final, Chen y Gendron escribieron un artículo en el que presentaban su idea como una conjetura, en lugar de un teorema.
Hace poco, Chen se pasó horas incitando a ChatGPT con la esperanza de que la IA diera con una solución al problema aún sin resolver, pero no funcionaba. El mes pasado, durante una recepción en una conferencia de matemáticas en Washington, Chen se encontró con Ken Ono, un conocido matemático que acababa de dejar su trabajo en la Universidad de Virginia para unirse a Axiom, una empresa de inteligencia artificial cofundada por una de sus alumnas, Carina Hong.
Chen le contó el problema a Ono y, a la mañana siguiente, Ono le presentó una prueba, cortesía de AxiomProver, la IA de resolución matemática de su startup. “A partir de ese momento, todo encajó de forma natural”, explica Chen, quien trabajó con Axiom para redactar la prueba, ya publicada en arXiv, un repositorio público de artículos académicos.
La herramienta de IA de Axiom encontró una conexión entre el problema y un fenómeno numérico estudiado por primera vez en el siglo XIX. A continuación, ideó una prueba que verificó por sí misma. “Lo que AxiomProver encontró fue algo que todos los humanos habían pasado por alto”, explica Ono a WIRED.
Resoluciones en semanas
La demostración es una de las varias soluciones a problemas matemáticos sin resolver que Axiom afirma que su sistema ha encontrado en las últimas semanas. La IA aún no ha resuelto ninguno de los problemas más famosos (o lucrativos) del campo de las matemáticas, pero ha encontrado respuestas a preguntas que han dejado perplejos a expertos en distintas áreas durante años. Estas pruebas demuestran que la inteligencia artificial avanza a pasos agigantados en el campo de las matemáticas. En los últimos meses, otros matemáticos han informado sobre el uso de herramientas de IA para explorar nuevas ideas y resolver problemas existentes.
Las técnicas desarrolladas por Axiom pueden resultar útiles fuera del mundo de las matemáticas avanzadas. Por ejemplo, podrían utilizarse para desarrollar software más resistente a determinados tipos de ataques de ciberseguridad. Esto implicaría utilizar la IA para verificar que el código es demostrablemente fiable y digno de confianza.
“Las matemáticas son el gran campo de pruebas y la caja de arena de la realidad”, manifiesta Hong, CEO de Axiom. “Creemos que hay muchos casos de uso bastante importantes y de gran valor comercial”.
El enfoque de Axiom consiste en combinar grandes modelos de lenguaje con un sistema de IA patentado llamado AxiomProver que está entrenado para razonar a través de problemas matemáticos y llegar a soluciones que sean probadamente correctas. En 2024, Google demostró una idea similar con un sistema llamado AlphaProof. Hong resalta que AxiomSolver incorpora varios avances significativos y técnicas más novedosas.
Ono indica que la demostración de la conjetura de Chen-Gendron generada por la IA muestra cómo ésta puede ayudar ahora de forma significativa a los matemáticos profesionales. “Se trata de un nuevo paradigma para demostrar teoremas”, agrega.
Más que un modelo estándar
El sistema de Axiom es más que un modelo normal de IA, ya que es capaz de verificar pruebas utilizando un lenguaje matemático especializado llamado Lean. En lugar de limitarse a buscar en la literatura, esto permite a AxiomProver desarrollar formas realmente novedosas de resolver problemas.
Otra de las nuevas pruebas generadas por AxiomProver demuestra que la IA es capaz de resolver problemas matemáticos por sí sola. Esta demostración, que también se ha descrito en un artículo publicado en arXiv, ofrece una solución a la conjetura de Fel, que se refiere a las ‘sizigias’, expresiones matemáticas en las que los números se alinean en álgebra. Sorprendentemente, la conjetura implica fórmulas que se encontraron por primera vez en el cuaderno del legendario matemático indio Srinivasa Ramanujan hace más de 100 años. En este caso, AxiomProver no se limitó a completar una pieza que faltaba en el rompecabezas, sino que ideó la demostración de principio a fin.
