Un sistema desarrollado por DeepMind de Google ha establecido un nuevo récord de rendimiento de la IA en problemas de geometría. AlphaGeometry de DeepMind pudo resolver 25 de 30 problemas de geometría extraídos de Olimpiada Internacional de Matemáticas entre 2000 y 2022.
Esto sitúa al software por delante de la gran mayoría de los jóvenes matemáticos y justo detrás de los medallistas de oro de la OMI. DeepMind estima que el medallista de oro promedio habría resuelto 26 de 30 problemas. Muchos consideran que la OMI es la competición de matemáticas para estudiantes de secundaria más prestigiosa del mundo.
«Debido a que los modelos de lenguaje son excelentes para identificar patrones y relaciones generales en los datos, pueden predecir rápidamente construcciones potencialmente útiles, pero a menudo carecen de la capacidad de razonar o explicar rigurosamente sus decisiones». mente profunda escribe. Para superar esta dificultad, DeepMind combinó un modelo de lenguaje con un motor de deducción simbólica más tradicional que realiza razonamiento algebraico y geométrico.
La investigación fue dirigida por Trieu Trinh, un científico informático que recientemente obtuvo su doctorado en la Universidad de Nueva York. Fue residente de DeepMind entre 2021 y 2023.
Evan Chen, ex medallista de oro olímpico que evaluó algunos de los resultados de AlphaGeometry, lo elogió como «impresionante porque es verificable y limpio». Si bien algunos software anteriores generaban pruebas geométricas complejas que eran difíciles de entender para los revisores humanos, el resultado de AlphaGeometry es similar a lo que escribiría un matemático humano.
AlphaGeometry es parte del proyecto más amplio de DeepMind para mejorar las capacidades de razonamiento de grandes modelos de lenguaje combinándolos con algoritmos de búsqueda tradicionales. DeepMind ha publicado varios artículos en esta área durante el último año.
Cómo funciona AlphaGeometry
Comencemos con un ejemplo simple que se muestra en Papel AlphaGeometryque fue publicado por Nature el miércoles:
El objetivo es demostrar que si un triángulo tiene dos lados iguales (AB y AC), entonces los ángulos opuestos a esos lados también serán iguales. Podemos hacer esto creando un nuevo punto D en el punto medio del tercer lado del triángulo (BC). Es fácil demostrar que los tres lados del triángulo ABD tienen la misma longitud que los lados correspondientes del triángulo ACD. Y dos triángulos de lados iguales siempre tienen ángulos iguales.
Los problemas de geometría de la OMI son mucho más complejos que este problema de juguete, pero fundamentalmente tienen la misma estructura. Todos comienzan con una figura geométrica y algunos datos sobre la figura, como “el lado AB tiene la misma longitud que el lado AC”. El objetivo es generar una secuencia de inferencias válidas que concluyan con un enunciado dado como “el ángulo ABC es igual al ángulo BCA”.
Durante muchos años hemos tenido software que puede generar listas de conclusiones válidas que pueden extraerse de un conjunto de suposiciones iniciales. Los problemas de geometría simples pueden resolverse mediante “fuerza bruta”: enumerar mecánicamente todos los hechos posibles que se pueden inferir a partir de una suposición determinada, luego enumerar todas las inferencias posibles a partir de esos hechos, y así sucesivamente, hasta llegar a la conclusión deseada.
Pero este tipo de búsqueda por fuerza bruta no es viable para un problema de geometría a nivel IMO porque el espacio de búsqueda es demasiado grande. Los problemas más difíciles no sólo requieren demostraciones más largas, sino que las demostraciones sofisticadas a menudo requieren la introducción de nuevos elementos en la figura inicial, como ocurre con el punto D en la demostración anterior. Una vez que se permiten este tipo de “puntos auxiliares”, el espacio de posibles pruebas explota y los métodos de fuerza bruta se vuelven poco prácticos.
Por lo tanto, los matemáticos deben desarrollar una intuición sobre qué pasos de demostración pueden conducir a un resultado exitoso. La innovación de DeepMind fue utilizar un modelo de lenguaje para proporcionar el mismo tipo de guía intuitiva para un proceso de búsqueda automatizado.
La desventaja de un modelo de lenguaje es que no es bueno en el razonamiento deductivo: los modelos de lenguaje a veces pueden “alucinar” y llegar a conclusiones que en realidad no se derivan de las premisas dadas. Entonces, el equipo de DeepMind desarrolló una arquitectura híbrida. Existe un mecanismo de deducción simbólico que deriva mecánicamente conclusiones que se derivan lógicamente de las premisas dadas. Pero periódicamente el control pasará a un modelo de lenguaje que dará un paso más “creativo”, como añadir un nuevo punto a la figura.
Lo que hace que esto sea complicado es que se necesitan muchos datos para entrenar un nuevo modelo de lenguaje y no hay suficientes ejemplos de problemas de geometría difíciles. Entonces, en lugar de depender de problemas geométricos diseñados por humanos, Trinh y sus colegas de DeepMind generaron una enorme base de datos de problemas geométricos desafiantes desde cero.
Para ello, el software generaría una serie de figuras geométricas aleatorias como las que se ilustran arriba. Cada uno tenía un conjunto de suposiciones iniciales. El mecanismo de deducción simbólica generaría una lista de hechos que se derivan lógicamente de los supuestos iniciales, luego más afirmaciones que se derivan de esas deducciones, y así sucesivamente. Una vez que hubiera una lista lo suficientemente larga, el software elegiría una de las conclusiones y «trabajaría hacia atrás» para encontrar el conjunto mínimo de pasos lógicos necesarios para llegar a la conclusión. Esta lista de inferencias es una prueba de finalización y, por lo tanto, puede convertirse en un problema en el conjunto de entrenamiento.
A veces, una prueba hacía referencia a un punto de la figura, pero la prueba no dependía de ninguna suposición inicial sobre ese punto. En estos casos, el software podría eliminar este punto del planteamiento del problema pero luego introducirlo como parte de la prueba. En otras palabras, podría tratar este punto como un “punto auxiliar” que debía introducirse para completar la demostración. Estos ejemplos ayudaron al modelo de lenguaje a aprender cuándo y cómo era útil agregar nuevos puntos para completar una demostración.
En total, DeepMind generó 100 millones de pruebas de geometría sintética, incluidos casi 10 millones que requirieron la introducción de «puntos de ayuda» como parte de la solución. Durante el proceso de capacitación, DeepMind puso especial énfasis en ejemplos que involucraban puntos de ayuda para alentar al modelo a tomar estos pasos más creativos para resolver problemas del mundo real.
