AlphaProof: de jugar juegos a dominar las matemáticas

Varios años antes de que ChatGPT de OpenAI comenzara a parlotear, Google desarrolló un programa de Inteligencia Artificial (IA) muy diferente denominado AlphaGo que aprendió a jugar al juego de mesa Go con una habilidad sobrehumana mediante una práctica incansable. Los investigadores de la compañía han publicado una investigación que combina las capacidades de un gran modelo de lenguaje (la IA detrás de los chatbots actuales) con las de AlphaZero, un sucesor de AlphaGo también capaz de jugar al ajedrez, para resolver pruebas matemáticas muy complicadas. Vale la pena destacar que, su nueva creación bautizada “AlphaProof”, ha demostrado su destreza al abordar diversos problemas de la Olimpiada Internacional de Matemáticas (OIM) de 2024, una prestigiosa competencia para estudiantes de secundaria.

AlphaProof dominando las matemáticas…

AlphaProof usa el modelo de lenguaje Gemini para convertir preguntas matemáticas formuladas de forma natural en un lenguaje de programación denominado Lean. Es de resaltar que esto proporciona el material de entrenamiento para un segundo algoritmo que aprende, mediante ensayo y error, cómo hallar pruebas que puedan confirmarse como correctas.

A principios de este año, Google DeepMind reveló otro algoritmo matemático denominado “AlphaGeometry” que también combina un modelo de lenguaje con un enfoque de Inteligencia Artificial (IA) diferente. AlphaGeometry usa Gemini para convertir problemas de geometría en una forma que pueda ser manipulada y probada por un programa que maneja elementos geométricos. Por su parte, Google también anunció recientemente una versión nueva y optimizada de AlphaGeometry.

Los investigadores descubrieron que sus 2 programas matemáticos podían suministrar pruebas para los acertijos de la OMI tan bien como lo podría hacer un medallista de plata. Cabe aclarar que, los programas resolvieron 2 problemas de álgebra y 1 problema de teoría de números de un total de 6. Resolvió un problema en tan solo minutos, pero tardó varios días en resolver otros. Desde Google DeepMind no han revelado cuánta potencia informática utilizó para resolver los problemas.

Google DeepMind llama al enfoque utilizado tanto para AlphaProof como para AlphaGeometry “neuro-simbólico” puesto que combinan el aprendizaje automático puro de una red neuronal artificial, con el lenguaje de la programación convencional.

“Lo que hemos visto aquí es que se puede combinar el enfoque que tuvo tanto éxito, y cosas como AlphaGo, con grandes modelos de lenguaje y producir algo que es extremadamente capaz”, señala David Silver, el investigador de Google DeepMind que dirigió el trabajo en AlphaZero.

Silver ha manifestado que las técnicas demostradas con AlphaProof deberían, en teoría, extenderse a otras áreas de las matemáticas.

De hecho, la investigación plantea la posibilidad de abordar las peores tendencias de los grandes modelos de lenguaje aplicando la lógica y así mismo, el razonamiento de una forma más fundamentada. Por prodigiosos que puedan ser los grandes modelos de lenguaje, frecuentemente poseen dificultades para comprender incluso las matemáticas básicas o para razonar los problemas de manera lógica.

Según se informa, en el futuro, el método “neural-simbólico” podría suministrar un medio para que los sistemas de Inteligencia Artificial conviertan las preguntas o tareas en una forma sobre la que se pueda razonar de una manera que produzca resultados confiables. Igualmente se rumorea que OpenAI se encuentra trabajando en un sistema de este tipo, cuyo nombre en código viene siendo “Strawberry”.

Sin embargo, si hay algo importante que señalar es que los sistemas revelados recientemente, tienen una limitación clave, tal y como reconoce Silver. Las soluciones matemáticas son correctas o incorrectas, lo que permite que AlphaProof y AlphaGeometry trabajen para hallar la respuesta correcta. Numerosos problemas del mundo real tienen muchas soluciones posibles, y puede que no esté claro cuál es la ideal. Silver señala que la solución para preguntas más ambiguas puede ser que un modelo de lenguaje intente determinar qué constituye una respuesta “correcta” durante el entrenamiento.

Según comenta, “Hay un espectro de cosas diferentes que se pueden probar”.

Silver también es cuidadoso al señalar que Google DeepMind no dejará sin trabajo a los matemáticos humanos.

Señala, “Nuestro objetivo es proporcionar un sistema que pueda demostrar cualquier cosa, pero ese no es el final de lo que hacen los matemáticos. Una gran parte de las matemáticas es plantear problemas y encontrar cuáles son las preguntas interesantes que se deben hacer. Podrías pensar en esto como otra herramienta similar a una regla de cálculo, una calculadora o una herramienta computacional”.