AlphaGeometry, el sistema de IA para geometría a nivel de olimpiada
(deepmind.google)- Mientras la Olimpiada Internacional de Matemáticas se ha convertido en una prueba clave para el razonamiento matemático de la IA, AlphaGeometry resolvió 25 de 30 problemas de geometría dentro del tiempo límite, acercándose al promedio de 25.9 de los medallistas de oro humanos
- La clave está en combinar un modelo de lenguaje neuronal con un motor de razonamiento simbólico basado en reglas, procesando en un mismo ciclo tanto propuestas de construcciones intuitivas como la verificación mediante lógica formal
- Los 100 millones de ejemplos sintéticos únicos creados sin demostraciones humanas redujeron el cuello de botella del entrenamiento, y 9 millones de ellos incluyen construcciones auxiliares necesarias para las pruebas
- Todas las soluciones de olimpiada fueron verificadas por computadora, y Evan Chen evaluó que la salida es verificable por máquina, legible para humanos y sigue las reglas clásicas de geometría que usan los estudiantes
- Como en una edición de la IMO normalmente solo 2 de 6 problemas son de geometría, su alcance de aplicación es limitado, pero aun así se convirtió en el primer modelo de IA que, solo con su desempeño en geometría, puede superar el umbral de medalla de bronce de la IMO de 2000 y 2015
Resultados en el benchmark de geometría de la IMO
- AlphaGeometry, presentado en Nature, resuelve problemas complejos de geometría a un nivel cercano al de los medallistas de oro humanos en olimpiadas
- El benchmark consiste en 30 problemas de geometría IMO-AG-30 seleccionados de olimpiadas entre 2000 y 2022
- AlphaGeometry: 25 resueltos dentro del tiempo límite
- Método de Wu, el mejor enfoque previo: 10 resueltos
- Promedio de medallistas de oro humanos: 25.9 resueltos
- Google DeepMind publicó como código abierto el código y modelo de AlphaGeometry
Arquitectura del sistema neuro-simbólico
- AlphaGeometry es un sistema neuro-simbólico en el que un modelo de lenguaje neuronal y un motor de razonamiento simbólico trabajan juntos para encontrar pruebas de teoremas geométricos complejos
- El modelo de lenguaje identifica rápidamente patrones y relaciones generales en los datos para predecir construcciones que probablemente sean útiles
- Sin embargo, puede carecer de capacidad para razonamientos rigurosos o para explicar sus decisiones
- El motor de razonamiento simbólico llega a conclusiones siguiendo lógica formal y reglas claras
- Es explicable y racional, pero puede ser lento y menos flexible cuando enfrenta problemas grandes por sí solo
- Al usar ambos componentes juntos, el modelo de lenguaje propone elementos auxiliares de construcción como nuevos puntos, líneas o círculos, y el motor de razonamiento deriva a partir de ellos conclusiones adicionales sobre la figura
Ciclo de resolución para encontrar construcciones auxiliares
- Los problemas de geometría de olimpiada a veces no se resuelven directamente con la figura dada, sino que requieren agregar nuevos elementos geométricos necesarios para la solución
- El proceso de resolución de AlphaGeometry alterna entre razonamiento simbólico y propuestas del modelo de lenguaje
- A partir de la figura dada y las premisas del teorema, el motor de razonamiento simbólico deriva nuevas proposiciones
- Si no encuentra la respuesta o ya no puede generar nuevas proposiciones, el modelo de lenguaje agrega un elemento auxiliar que probablemente sea útil
- El elemento añadido abre una nueva ruta para el motor de razonamiento, y el proceso se repite hasta encontrar la solución
- En el problema 3 de la Olimpiada Internacional de Matemáticas de 2015, la solución de AlphaGeometry está compuesta por 109 pasos lógicos
Generación de 100 millones de datos sintéticos
- La geometría se basa en comprender el espacio, la distancia, la forma y la posición relativa, y es una base para áreas como el arte, la arquitectura y la ingeniería
- El método de generación de datos sintéticos de AlphaGeometry imita a gran escala el proceso por el cual una persona observa una figura y encuentra nuevas propiedades y relaciones geométricas usando conocimiento previo
- El sistema genera 1,000 millones de figuras aleatorias mediante cómputo altamente paralelizado
- En cada figura, deriva exhaustivamente todas las relaciones entre puntos y líneas
- Encuentra todas las pruebas contenidas en cada figura
- Rastrea en sentido inverso qué elementos auxiliares son necesarios para llegar a esas pruebas
- A este proceso se le llama deducción simbólica y traceback
- El enorme conjunto de datos se filtra para excluir ejemplos similares, y el resultado final son 100 millones de ejemplos de entrenamiento únicos de diversas dificultades
- De ellos, 9 millones son casos con elementos auxiliares añadidos
- El modelo de lenguaje aprende muchos ejemplos en los que una construcción auxiliar conduce a una prueba, lo que le permite proponer nuevas construcciones también en problemas de olimpiada
Verificabilidad y límites de aplicación
- Todas las soluciones de AlphaGeometry para los problemas de olimpiada fueron comprobadas y verificadas por computadora
- Los resultados se compararon con métodos de IA anteriores y con el desempeño humano en olimpiadas
- Evan Chen, entrenador de matemáticas y exmedallista de oro en olimpiadas, evaluó algunas de las soluciones
- La salida de AlphaGeometry es verificable y limpia
- En métodos de IA anteriores para problemas de competencia basados en pruebas, las respuestas a veces eran correctas y a veces no, por lo que podían requerir revisión humana
- Las soluciones de AlphaGeometry tienen una estructura verificable por máquina y al mismo tiempo legible para humanos
- En lugar de forzar enormes cálculos algebraicos con sistemas de coordenadas, usa reglas clásicas de geometría como ángulos y triángulos semejantes, igual que los estudiantes
- Una edición de la IMO consta de 6 problemas, y normalmente solo 2 se centran en geometría
- Por lo tanto, AlphaGeometry solo puede aplicarse a aproximadamente un tercio de los problemas de una edición
- Aun así, se convirtió en el primer modelo de IA que, solo por su capacidad en geometría, puede alcanzar el umbral de medalla de bronce de la IMO de 2000 y 2015
Expansión hacia la IA de razonamiento matemático
- AlphaGeometry muestra que la IA está ampliando su capacidad para razonar lógicamente y descubrir y verificar nuevo conocimiento
- Resolver problemas de geometría a nivel de olimpiada es un hito importante hacia un razonamiento matemático más profundo y sistemas de IA general más avanzados
- El enfoque de entrenar IA desde cero con grandes volúmenes de datos sintéticos podría influir en cómo se descubre nuevo conocimiento en ciencia e IA más allá de las matemáticas
- AlphaGeometry se apoya en la línea de trabajo de Google DeepMind y Google Research sobre IA para razonamiento matemático
- Explorando la belleza de las matemáticas puras de nuevas maneras
- Resolver problemas de matemáticas y ciencia con modelos de lenguaje mediante Minerva
- FunSearch logra el primer descubrimiento en un problema abierto de ciencias matemáticas usando modelos de lenguaje a gran escala
- El objetivo a largo plazo es generalizar a múltiples áreas de las matemáticas, desarrollar la resolución sofisticada de problemas y el razonamiento necesarios para sistemas de IA general, y crear sistemas de IA que expandan las fronteras del conocimiento humano
1 comentarios
Opiniones de Hacker News
Como alguien que fue autor de problemas en competencias como la IMO, leí este artículo con mucho interés. Al mismo tiempo, creo que la geometría tenía que ser el primer tema en caer ante la IA, es decir, ante índices inteligentes de conocimiento y de métodos de razonamiento.
Entre los temas de las olimpiadas de matemáticas, los problemas de geometría suelen ser los más “mecánicos”. Si se puede expresar un problema en coordenadas, por ejemplo coordenadas XY o el plano complejo, aparece un conjunto finito de pasos que una computadora puede usar para encontrar la solución. Claro que en la IMO, en la práctica, el límite de tiempo y los errores humanos impiden que sea viable. Antes solía verificar con WolframAlpha las demostraciones de problemas de geometría y conjeturas que yo mismo creaba usando ese enfoque.
El álgebra, especialmente las desigualdades, es parecida: muchas veces se llega a la respuesta si se empuja con suficiente cálculo.
Las áreas donde realmente quiero ver avanzar a los sistemas inteligentes son la teoría de números y la combinatoria. El espacio de búsqueda es mucho más complejo, y muchas veces exigen demostrar que algo es imposible. Esos problemas son difíciles de resolver por cálculo de fuerza bruta.
Estoy de acuerdo en que la geometría sería la primera. Por lo que vi aquí, no es “fuerza bruta” en el sentido de depender de geometría algebraica, vectores o soluciones con números complejos, pero sí se acerca a una búsqueda exhaustiva en el sentido de buscar por todos lados construcciones auxiliares “interesantes”.
La geometría siempre fue mi peor materia, pero sentía que, si me daban la construcción correcta, el problema se volvía mucho más fácil. El tema es que nunca desarrollé la intuición para que esas construcciones se me ocurrieran rápido. Esta IA tampoco parece tener esa intuición, pero puede producirlas muchísimo más rápido. Al final, los candidatos que se pueden construir —como rectas perpendiculares, paralelas o bisectrices— son limitados, y se pueden evaluar de forma bastante mecánica desplegando todos los ángulos y razones, o probando la potencia de un punto.
Es muy impresionante, pero en el sentido de “motor vs. IA” parece algo como DeepMind:Kasparov::AlphaGeo:Terry Tao.
Estoy de acuerdo en que el álgebra probablemente sea lo siguiente. Como en geometría, por lo general basta con encontrar una, dos o tres sustituciones ingeniosas, y las opciones son limitadas.
Algunos problemas de combinatoria también podrían encajar con esta estrategia de búsqueda. Por ejemplo, los de contar un mismo objeto de dos maneras. Pero ese es un puente más lejano y solo cubriría una parte del total de problemas.
Creo que la teoría de números será la última frontera antes de llegar a una puntuación perfecta de 42.
También me da curiosidad cómo eligen, después de verificar que se puedan resolver, qué problemas concretos entran al conjunto final. ¿Es por votación o por algún otro método de evaluación?
Alguien debería convertir la geometría sintética en un juego de aventura. Podría usar un lenguaje de escritura de demostraciones más simple que Lean, y además se podría hacer visualmente atractivo.
Si leí bien el paper, esto parece un trabajo de verdad. Es mucho más legítimo que aquel paper de matemáticas con IA que DeepMind promocionó erróneamente el mes pasado como si hubiera resuelto un problema abierto de investigación matemática. Aun así, llama bastante la atención lo diferente que es su estructura de lo que normalmente se piensa como razonamiento/inteligencia automática
Entendí que entrenan un Transformer con millones de teoremas de geometría elemental y lo usan para hacer una búsqueda por fuerza bruta de demostraciones. Por el contexto de la geometría elemental, la estructura es necesariamente elemental, y se puede decidir simbólicamente con facilidad si algo es verdadero o falso. Si la búsqueda por fuerza bruta falla, agregan aleatoriamente construcciones geométricas auxiliares, como añadir un punto medio, para ver si con ese material adicional la búsqueda funciona
Edición: como corrigió Imnimo, lo entendí al revés. La búsqueda por fuerza bruta es una búsqueda por fuerza bruta pura, y el Transformer se usa para predecir qué construcción auxiliar agregar
Además, aunque no aparece en la entrada del blog, los enunciados reales de los problemas también tuvieron que modificarse/adaptarse. Por ejemplo, una frase original como “Sean AH1, BH2, CH3 las alturas del triángulo ABC…” se cambió por una lista de definiciones mucho más explícita, como “Sea ABC un triángulo. La IA define el punto I de modo que sea la bisectriz del ángulo BAC y que CI sea la bisectriz del ángulo ACB…”, y al final queda en la forma “demuestre que T1I=IZ”
El proceso que describes es exactamente el mismo que usan las personas. Uno conjetura algo que parece útil y resuelve mecánicamente los detalles. Si se atasca, hace otra conjetura. Al final es parecido a explorar un árbol
La gente ya había identificado este proceso en 1955, e incluso hizo un prototipo funcional capaz de demostrar teoremas: https://en.wikipedia.org/wiki/Logic_Theorist La clave depende de usar buenas heurísticas. Las redes neuronales pueden extraer heurísticas de los datos, así que tienen sentido aquí
Me da curiosidad qué consideras que es la idea general de “razonamiento automático”. ¿Un dispositivo mágico que resuelve cualquier problema en una sola pasada lineal?
Solo al entrar a la carrera de matemáticas en la universidad aprendí la forma correcta de hacerlo y pude disfrutarla
Este campo todavía está en una etapa temprana y parece que queda mucho trabajo inconcluso. La parte de búsqueda debería reemplazarse con una red neuronal pequeña, y la parte de razonamiento no es difícil ni parece necesitar grandes mejoras
Ahora es momento de mejorar el rendimiento con auto-juego. En problemas de geometría plana, se puede ver la conclusión que hay que demostrar como un punto de la figura y las condiciones como otro punto, y hacer que dos jugadores se muevan lo más posible uno hacia el otro compartiendo datos. En ese proceso, la contribución de cada jugador podría usarse para mejorar el rendimiento, por analogía con el cálculo de victorias y derrotas en Go
No parece que este modelo específico sea generalizable, pero el enfoque neuro-simbólico parece muy prometedor
Consiste en conectar herramientas de “Sistema 1” cada vez más potentes, que constituyen la mayor parte del aprendizaje automático actual, con herramientas estructuradas de “Sistema 2”, como la generación de demostraciones lógicas. El Sistema 2 puede planear y verificar la veracidad o el valor de la salida
El Sistema 2 avanza hasta que se atasca; cuando se atasca, el Sistema 1 ofrece una conjetura intuitiva sobre qué parte del espacio de estados conviene revisar a continuación
Aquí aprovecharon que se pueden generar demostraciones por computadora para crear un dataset de 100 millones de demostraciones, lo que permitió aprendizaje autosupervisado escalable. Los dominios simbólicos parecen prestarse bien a este tipo de generación de datos. Aunque el valor de cada instancia individual sea bajo, en conjunto pueden permitir un preentrenamiento útil
Si se combinan estos elementos, es un enfoque que puede llegar bastante lejos
El hito clave es dejar atrás la necesidad de depender de dominios formales/simbólicos específicos y crear un sistema de preentrenamiento capaz de generalizar las técnicas aprendidas en ese dominio
Además, dentro de los dominios donde se puede aplicar, resuelve por completo uno de los problemas fundamentales que en la ola actual de IA llamamos “alucinaciones”. Pero esa solución es posible porque existe un sistema no IA que demuestra la corrección
En términos generales, este enfoque no es tan nuevo. En bioquímica se ha usado IA para encontrar moléculas candidatas y experimentos físicos para verificarlas
La IA para juegos combinatorios también lleva tiempo usando IA como entrada para la búsqueda Monte Carlo de la vieja escuela
Se agradece que hayan publicado el código y los pesos junto con el paper. Hasta donde recuerdo, esta es la primera vez que un paper famoso de DeepMind publica código de inferencia ejecutable y checkpoints. Me gustaría que me corrigieran si hay un caso anterior
Todavía no veo un conjunto de entrenamiento público ni código de entrenamiento de ejemplo, pero aun así es un buen avance porque les dieron a otros investigadores algo sobre lo cual construir. Al fin y al cabo, ese también es el propósito de los artículos académicos
Si no me equivoco, ¿usa un modelo t5? Al menos parece usar el vocabulario SentencePiece de t5
También me da curiosidad cuánto tiempo de GPU se usó para entrenar este modelo y qué parámetros de entrenamiento utilizaron
No quisiera que se malinterprete. Este sistema es fascinante y muestra cómo debería verse la ingeniería aplicada. Solo quisiera saber más sobre los detalles del entrenamiento, los datos iniciales y el método de generación de datos sintéticos
Me da mucha curiosidad saber con qué frecuencia el modelo de lenguaje genera construcciones útiles. Seguro que es mejor que algo aleatorio, pero no sé si lanza miles de construcciones hasta encontrar una buena, o si hace sugerencias útiles en una proporción similar a la de un experto humano.
El paper dice: “Como el proceso de decodificación del modelo de lenguaje devuelve k secuencias distintas que describen k construcciones auxiliares alternativas, usamos la puntuación de cada beam como función de valor para hacer búsqueda beam sobre estas k opciones. Esta configuración es muy fácil de paralelizar entre beams, por lo que se acelera mucho cuando hay recursos de cómputo paralelo. En los experimentos usamos un tamaño de beam k=512, un máximo de 16 iteraciones y un factor de ramificación por nodo, es decir, un tamaño de lote de decodificación, de 32”.
Pero no termino de entender cómo 512 y 16 se traducen en la cantidad total de construcciones propuestas. También dicen que, incluso quitando el tamaño de beam y el máximo de iteraciones, el rendimiento solo baja hasta cierto punto. ¿Eso significa que el modelo en realidad logra poner construcciones útiles bastante arriba, y que solo en los problemas más difíciles hacen falta miles?
Aun así, si lo intento, el resumen es 262,144, pero no hay que tomarlo literalmente.
La salida de la función de decodificación son tokens, que son más o menos 3/4 de una palabra, pero digamos que es 1 palabra.
La cantidad de tokens considerados por cada token de salida es
beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262,144.Basta contar la cantidad de palabras de la solución de ejemplo: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
La solución tiene 2289 tokens en total, y el total de tokens considerados es
262,144 * 2289 = 600,047,616.Si, forzando la cuenta, definimos “cantidad de soluciones consideradas” como tokens totales considerados / tokens totales de la solución, da 262,144. Tiene sentido decir que es el mismo valor que la cantidad de tokens vistos en cada paso de iteración.
Es interesante que el Transformer usado sea pequeño. Según el paper, se entrenó con la configuración predeterminada de la biblioteca Meliad, y tiene 12 capas, dimensión de embedding 1,024, 8 cabezas de atención y una capa densa entre atenciones de dimensión 4,096 con activación ReLU.
Excluyendo las capas de embedding de entrada y de la cabeza de salida, todo el Transformer tiene 151 millones de parámetros. El tokenizador personalizado se entrenó en modo ‘word’ de SentencePiece y el tamaño del vocabulario es 757. La longitud máxima de contexto se limitó a 1,024 tokens y se usaron embeddings de posición relativa al estilo T5. Como más del 90% de las secuencias tienen longitud menor a 200, también se usó empaquetado de secuencias.
Lo que para mí sí fue realmente nuevo es que el sistema anterior de mejor nivel ya podía resolver 10 de estos problemas. Había oído que existían algoritmos de decisión para problemas de geometría plana, pero no sabía que fueran algoritmos prácticos. Buscando, aparece como referencia http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf.
Estaba preparado para sospechar de este tipo de resultados, porque suelen ser del estilo “no se parece a una demostración humana”, pero cambié de opinión al ver que Evan Chen dijo que en realidad son demostraciones limpias y legibles para personas.
Evan Chen es una figura conocida en la comunidad de matemáticas de olimpiadas y también autor de un famoso libro de geometría de olimpiadas[1], así que esta vez hay que admitir que la máquina realmente conquistó una parte de los problemas de la IMO.
[1]: https://web.evanchen.cc/geombook.html
Aun así, la idea de que O2 está sobre el círculo de nueve puntos es correcta.
Edición: retiro lo dicho. Parece que están usando ángulos dirigidos[2], y entonces esa frase es correcta.
[1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
[2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...
Relacionado con esto, también vale la pena ver https://www.nytimes.com/2024/01/17/science/ai-computers-math...
Viene de https://news.ycombinator.com/item?id=39030186, y ese hilo se fusionará aquí
Relacionado: https://aimoprize.com/
Es un premio de 10 millones de dólares para modelos que tengan buen desempeño en la IMO