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 logró resolver 25 de los 30 problemas de geometría extraídos del Olimpiada Internacional de Matemáticas entre 2000 y 2022.
Eso coloca al software por delante de la gran mayoría de los jóvenes matemáticos y apenas por debajo de los medallistas de oro de la OMI. DeepMind estima que el medallista de oro promedio habría resuelto 26 de 30 problemas. Muchos ven la OMI como la competencia de matemáticas para estudiantes de secundaria más prestigiosa del mundo.
«Debido a que los modelos de lenguaje se destacan en la identificación de patrones y relaciones generales en los datos, pueden predecir rápidamente construcciones potencialmente útiles, pero a menudo carecen de la capacidad de razonar rigurosamente o explicar 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 a la vez verificable y limpio». Mientras que algunos programas anteriores generaban pruebas de geometría 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 el 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 una afirmación dada 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 se pueden resolver mediante “fuerza bruta”: enumerar mecánicamente todos los hechos posibles que se pueden inferir a partir de la suposición dada, 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 factible para un problema de geometría de 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 tienen en cuenta 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 probablemente conducirán a un resultado exitoso. El gran avance de DeepMind fue utilizar un modelo de lenguaje para proporcionar el mismo tipo de guía intuitiva a un proceso de búsqueda automatizado.
La desventaja de un modelo de lenguaje es que no es bueno en 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. Hay un motor de deducción simbólica 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 de geometría diseñados por humanos, Trinh y sus colegas de DeepMind generaron una enorme base de datos de problemas de geometría desafiantes desde cero.
Para ello, el software generaría una serie de figuras geométricas aleatorias como las ilustradas arriba. Cada uno tenía un conjunto de suposiciones iniciales. El motor 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 la conclusión y, por 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 esos casos, el software podría eliminar ese 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 prueba. Estos ejemplos ayudaron al modelo de lenguaje a aprender cuándo y cómo era útil agregar nuevos puntos para completar una prueba.
En total, DeepMind generó 100 millones de pruebas de geometría sintética, incluidos casi 10 millones que requirieron la introducción de «puntos auxiliares» como parte de la solución. Durante el proceso de capacitación, DeepMind puso especial énfasis en ejemplos que involucraban puntos auxiliares para alentar al modelo a tomar estos pasos más creativos al resolver problemas reales.
