AlphaGeometry: un sistema de inteligencia artificial para geometría a nivel de Olimpiada

Investigación

Publicado
Autores

Trieu Trinh y Thang Luong

Nuestro sistema de IA supera el enfoque de última generación para problemas de geometría, avanzando el razonamiento de la IA en matemáticas.

Como reflejo del espíritu olímpico de la antigua Grecia, la Olimpiada Internacional de Matemáticas es un escenario moderno para los matemáticos de secundaria más brillantes del mundo. La competencia no solo muestra talentos jóvenes, sino que se ha convertido en un campo de pruebas para sistemas avanzados de inteligencia artificial en matemáticas y razonamiento.

En un artículo publicado hoy en Naturaleza, presentamos AlphaGeometry, un sistema de IA que resuelve problemas geométricos complejos a un nivel cercano al de un medallista de oro humano en una Olimpiada: un gran avance en el rendimiento de la IA. En una prueba comparativa de 30 problemas de geometría de la Olimpiada, AlphaGeometry resolvió 25 dentro del límite de tiempo estándar de la Olimpiada. A modo de comparación, el sistema de última generación anterior resolvió 10 de estos problemas de geometría, y el medallista de oro humano promedio resolvió 25,9 problemas.

En nuestro conjunto de evaluación comparativa de 30 problemas de geometría de las Olimpiadas (IMO-AG-30), compilados a partir de las Olimpiadas de 2000 a 2022, AlphaGeometry resolvió 25 problemas dentro de los límites de tiempo de la competencia. Esto se acerca al puntaje promedio de los medallistas de oro humanos en estos mismos problemas. El método de vanguardia anterior, conocido como “método de Wu”, resolvió 10.

Los sistemas de IA a menudo luchan con problemas complejos en geometría y matemáticas debido a la falta de habilidades de razonamiento y datos de entrenamiento. El sistema de AlphaGeometry combina el poder predictivo de un modelo de lenguaje neuronal con un motor de deducción sujeto a reglas, que funcionan en conjunto para encontrar soluciones. Y al desarrollar un método para generar un vasto conjunto de datos de entrenamiento sintéticos (100 millones de ejemplos únicos), podemos entrenar AlphaGeometry sin ninguna demostración humana, evitando el cuello de botella de los datos.

Con AlphaGeometry, demostramos la creciente capacidad de la IA para razonar lógicamente y descubrir y verificar nuevos conocimientos. Resolver problemas de geometría a nivel de Olimpiada es un hito importante en el desarrollo de un razonamiento matemático profundo en el camino hacia sistemas de IA más avanzados y generales. Estamos abriendo el código fuente Código y modelo AlphaGeometryy esperamos que, junto con otras herramientas y enfoques en la generación y capacitación de datos sintéticos, ayude a abrir nuevas posibilidades en matemáticas, ciencia e inteligencia artificial.

Para mí tiene mucho sentido ahora que los investigadores en IA estén probando primero los problemas de geometría de la OMI porque encontrar soluciones para ellos funciona un poco como el ajedrez en el sentido de que tenemos una cantidad bastante pequeña de movimientos sensatos en cada paso. Pero todavía me sorprende que hayan podido hacerlo funcionar. Es un logro impresionante.

Ngô Bảo Châu, medallista Fields y medallista de oro de la OMI

AlphaGeometry adopta un enfoque neurosimbólico

AlphaGeometry es un sistema neurosimbólico compuesto por un modelo de lenguaje neuronal y un motor de deducción simbólica, que trabajan juntos para encontrar pruebas de teoremas de geometría complejos. Similar a la idea de “pensando, rápido y lento”, un sistema proporciona ideas rápidas e “intuitivas” y el otro, una toma de decisiones más deliberada y racional.

Debido a que los modelos de lenguaje 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. Los motores de deducción simbólica, por otro lado, se basan en la lógica formal y utilizan reglas claras para llegar a conclusiones. Son racionales y explicables, pero pueden ser “lentos” e inflexibles, especialmente cuando se enfrentan por sí solos a problemas grandes y complejos.

El modelo de lenguaje de AlphaGeometry guía su motor de deducción simbólica hacia posibles soluciones a problemas de geometría. Los problemas de geometría olímpica se basan en diagramas a los que es necesario agregar nuevas construcciones geométricas antes de poder resolverlos, como puntos, líneas o círculos. El modelo de lenguaje de AlphaGeometry predice qué nuevas construcciones sería más útil agregar, entre un número infinito de posibilidades. Estas pistas ayudan a llenar los vacíos y permiten que el motor simbólico haga más deducciones sobre el diagrama y se acerque a la solución.

AlphaGeometry resolviendo un problema simple: dado el diagrama del problema y las premisas de su teorema (izquierda), AlphaGeometry (centro) primero usa su motor simbólico para deducir nuevas afirmaciones sobre el diagrama hasta que se encuentra la solución o se agotan las nuevas afirmaciones. Si no se encuentra ninguna solución, el modelo de lenguaje de AlphaGeometry agrega una construcción potencialmente útil (azul), abriendo nuevos caminos de deducción para el motor simbólico. Este ciclo continúa hasta que se encuentra una solución (derecha). En este ejemplo, sólo se requiere una construcción.

AlphaGeometry resolviendo un problema de Olimpiada: Problema 3 de la Olimpiada Internacional de Matemáticas de 2015 (izquierda) y una versión condensada de la solución de AlphaGeometry (derecha). Los elementos azules son construcciones agregadas. La solución de AlphaGeometry tiene 109 pasos lógicos.

Generando 100 millones de ejemplos de datos sintéticos

La geometría se basa en la comprensión del espacio, la distancia, la forma y las posiciones relativas, y es fundamental para el arte, la arquitectura, la ingeniería y muchos otros campos. Los humanos pueden aprender geometría usando lápiz y papel, examinando diagramas y utilizando el conocimiento existente para descubrir propiedades y relaciones geométricas nuevas y más sofisticadas. Nuestro enfoque de generación de datos sintéticos emula este proceso de construcción de conocimiento a escala, lo que nos permite entrenar AlphaGeometry desde cero, sin demostraciones humanas.

Utilizando computación altamente paralelizada, el sistema comenzó generando mil millones de diagramas aleatorios de objetos geométricos y derivó exhaustivamente todas las relaciones entre los puntos y líneas de cada diagrama. AlphaGeometry encontró todas las pruebas contenidas en cada diagrama y luego trabajó hacia atrás para descubrir qué construcciones adicionales, si las hubiera, eran necesarias para llegar a esas pruebas. A este proceso lo llamamos “deducción y rastreo simbólicos”.

Representaciones visuales de los datos sintéticos generados por AlphaGeometry.

Ese enorme conjunto de datos se filtró para excluir ejemplos similares, lo que dio como resultado un conjunto de datos de entrenamiento final de 100 millones de ejemplos únicos de dificultad variable, de los cuales nueve millones presentaban construcciones adicionales. Con tantos ejemplos de cómo estas construcciones llevaron a pruebas, el modelo de lenguaje de AlphaGeometry puede hacer buenas sugerencias para nuevas construcciones cuando se le presentan problemas de geometría de Olimpiada.

Razonamiento matemático pionero con IA

La solución a cada problema de la Olimpiada proporcionada por AlphaGeometry fue revisada y verificada por computadora. También comparamos sus resultados con métodos de IA anteriores y con el desempeño humano en la Olimpiada. Además, Evan Chen, entrenador de matemáticas y ex medallista de oro olímpico, evaluó para nosotros una selección de soluciones de AlphaGeometry.

Chen dijo: “El resultado de AlphaGeometry es impresionante porque es verificable y limpio. Las soluciones anteriores de IA para problemas de competencia basados ​​en pruebas a veces han sido impredecibles (los resultados solo son correctos algunas veces y necesitan controles humanos). AlphaGeometry no tiene esta debilidad: sus soluciones tienen una estructura verificable por máquina. Sin embargo, a pesar de esto, su resultado sigue siendo legible por humanos. Uno podría haber imaginado un programa de computadora que resolviera problemas de geometría mediante sistemas de coordenadas de fuerza bruta: piense en páginas y páginas de tediosos cálculos de álgebra. AlphaGeometry no es eso. Utiliza reglas de geometría clásica con ángulos y triángulos similares tal como lo hacen los estudiantes”.

El resultado de AlphaGeometry es impresionante porque es verificable y limpio… Utiliza reglas de geometría clásica con ángulos y triángulos similares tal como lo hacen los estudiantes.

Evan Chen, entrenador de matemáticas y medallista de oro en los Juegos Olímpicos

Como cada Olimpiada presenta seis problemas, de los cuales sólo dos se centran típicamente en la geometría, AlphaGeometry solo se puede aplicar a un tercio de los problemas de una Olimpiada determinada. Sin embargo, su capacidad geométrica por sí sola lo convierte en el primer modelo de IA del mundo capaz de superar el umbral de la medalla de bronce de la OMI en 2000 y 2015.

En geometría, nuestro sistema se acerca al estándar de un medallista de oro de la OMI, pero tenemos el ojo puesto en un premio aún mayor: avanzar en el razonamiento para los sistemas de IA de próxima generación. Dado el mayor potencial de entrenar sistemas de IA desde cero con datos sintéticos a gran escala, este enfoque podría moldear cómo los sistemas de IA del futuro descubren nuevos conocimientos, en matemáticas y más.

AlphaGeometry se basa en el trabajo de Google DeepMind y Google Research para ser pionero en el razonamiento matemático con IA, desde explorando la belleza de las matemáticas puras a resolver problemas matemáticos y científicos con modelos de lenguaje. Y más recientemente, presentamos Búsqueda Divertidaque hizo los primeros descubrimientos en problemas abiertos en ciencias matemáticas utilizando modelos de lenguaje grandes.

Nuestro objetivo a largo plazo sigue siendo construir sistemas de IA que puedan generalizarse en todos los campos matemáticos, desarrollando la solución sofisticada de problemas y el razonamiento de los que dependerán los sistemas generales de IA, al tiempo que ampliamos las fronteras del conocimiento humano.