Google crea una IA que ya probó 1200 teoremas matemáticos
Puede que algunas inteligencias artificiales sufran con exámenes de matemática de secundaria, pero otras están superando a los humanos. De acuerdo a una investigación publicada en ArXiv, una IA creada por un equipo en Google ha demostrado más de 1200 teoremas matemáticos. Los matemáticos ya conocían estos teoremas, este avance es una indicación que la IA podría comenzar a trabajar en problemas más difíciles.
Para entrenar su inteligencia artificial, el equipo de Google comenzó con una base de datos de más de 10,000 pruebas matemáticas escritas por humanos, junto con el razonamiento detrás de cada paso. Estos pasos, también llamados “tácticas”, podrían incluir el uso de una propiedad conocida sobre los números, como el hecho de que multiplicar x por y es lo mismo que multiplicar y por x, o aplicar la regla de la cadena.
Luego, probaron la IA en 3225 teoremas que no había visto antes y probaron con éxito 1253 de ellos. Los que no pudo probar fueron porque solo tenía 41 tácticas a su disposición. Para probar cada teorema, la IA los divide en componentes cada vez más pequeños utilizando la lista de tácticas. Eventualmente, cada uno de los componentes más pequeños podría probarse con una sola táctica, lo que demuestra el teorema más grande.
«La mayoría de las pruebas que utilizamos son relativamente cortas, por lo que no requieren un razonamiento largo y complicado, pero esto es un comienzo», dijo a New Scientist, Christian Szegedy de Google. «A donde queremos llegar es a un sistema que puede probar todos los teoremas que los humanos pueden probar, y tal vez incluso más».
Matemáticas más difíciles
Aunque este algoritmo se enfoca en el álgebra lineal y el cálculo complejo, cambiar su conjunto de entrenamiento podría permitirle hacer cualquier tipo de matemáticas, dice Szgedy. Por ahora, la aplicación principal de AI está completando los detalles de pruebas largas y arduas con extrema precisión.
Los matemáticos humanos suelen hacer saltos intelectuales en sus pruebas sin explicar las tácticas exactas que se utilizan para ir de un paso a otro, y los probadores de este tipo podrían recorrer el trabajo intermedio automáticamente, sin necesidad de que un humano complete cada táctica exacta utilizada.
«Uno obtiene el máximo de precisión y corrección, todo explicado realmente, pero no tiene que hacer el trabajo de completar los detalles», dice Jeremy Avigad de la Universidad Carnegie Mellon en Pennsylvania. «Tal vez descargar algunas cosas que solíamos hacer a mano nos libera para buscar nuevos conceptos y hacer nuevas preguntas», añade.
Por eso, las IA de este tipo podrían incluso resolver problemas de matemáticas que no sabemos cómo resolver o que son demasiado largos y complicados. Pero eso requerirá un conjunto de entrenamiento mucho más grande, más tácticas y una forma más sencilla de conectar los teoremas a la computadora. «Eso está lejos, pero creo que podría suceder en nuestra vida», dice Szgedy.
Aunque este avance es indudablemente impresionante, no todas las IA son iguales. Hace poco DeepMind, también de Google, entrenó una inteligencia artificial para tomar un examen de matemáticas de secundaria y lo terminó reprobando.
Fuente: nmas1.org