Google DeepMind está cada vez más cerca de descifrar las matemáticas de más alto nivel | Inteligencia artificial (IA)

Aunque las computadoras fueron diseñadas para hacer cálculos matemáticos más rápido que cualquier ser humano, el nivel superior de las matemáticas formales sigue siendo un dominio exclusivamente humano. Pero un avance de los investigadores de Google DeepMind ha acercado más que nunca a los sistemas de inteligencia artificial a vencer a los mejores matemáticos humanos en su propio terreno.

Un par de nuevos sistemas, llamados AlphaProof y AlphaGeometry 2, trabajaron juntos para abordar las preguntas de la Olimpiada Internacional de Matemáticas, una competencia mundial de matemáticas para estudiantes de secundaria que se lleva a cabo desde 1959. La Olimpiada consiste en seis preguntas increíblemente difíciles cada año, que abarcan campos como el álgebra, la geometría y la teoría de números. Ganar una medalla de oro te coloca entre los mejores matemáticos jóvenes del mundo.

Los esfuerzos combinados de los dos sistemas de DeepMind no estaban a la altura. Después de que sus respuestas fueran calificadas por el profesor Timothy Gowers (ganador del equivalente matemático al premio Nobel, la medalla Fields y medallista de oro en las olimpiadas), el equipo de DeepMind obtuvo 28 puntos de 42, suficiente para una medalla de plata, pero un punto menos que la de oro.

A diferencia de un matemático humano, los sistemas eran perfectos o inútiles. En cada una de las preguntas que resolvieron, obtuvieron la puntuación perfecta, pero en dos de las seis preguntas ni siquiera pudieron empezar a trabajar para encontrar una respuesta. Además, a diferencia de sus competidores humanos, DeepMind no tenía límite de tiempo. Mientras que los estudiantes tienen nueve horas para resolver los problemas, los sistemas de DeepMind tardaron tres días trabajando sin descanso para resolver una pregunta, a pesar de resolver otra en cuestión de segundos.

Los dos sistemas que funcionaron en el desafío eran muy diferentes entre sí. AlphaProof, que resolvió tres de los problemas, funciona combinando un gran modelo de lenguaje (del tipo que se aplica en los chatbots de consumo) con un enfoque especializado de “aprendizaje de refuerzo”, como el que utilizó DeepMind para abordar el juego de mesa Go. El truco está en aprovechar un enfoque preexistente llamado “matemática formal”, un conjunto de reglas que permite escribir una prueba matemática como un programa que puede ejecutarse solo si es verdadero.

“Lo que intentamos hacer es construir un puente entre estas dos esferas”, dijo Thomas Hubert, el líder de AlphaProof, “para que podamos aprovechar las garantías que vienen con las matemáticas formales y los datos que están disponibles en las matemáticas informales”. Después de entrenarlo con una gran cantidad de problemas matemáticos escritos en inglés, AlphaProof utilizó su conocimiento para intentar generar pruebas específicas en el lenguaje formal. Como esas pruebas pueden ser verificables o no, es posible enseñarle al sistema a mejorarse a sí mismo. El enfoque puede resolver problemas difíciles, pero no siempre es rápido: si bien es mucho mejor que el simple ensayo y error, tomó tres días encontrar el modelo formal correcto para una de las preguntas más difíciles del desafío.

El otro sistema, AlphaGeometry 2, combina de forma similar un modelo de lenguaje con un enfoque más matemático, pero su éxito en el campo más restringido de los problemas de geometría fue sorprendente: resolvió su problema en solo 16 segundos. Y, dice Gowers, eligió una ruta sorprendente para hacerlo. “Ha habido algunos ejemplos legendarios de demostraciones (asistidas por computadora) que son más largas que Wikipedia. Este no fue así: estamos hablando de un resultado muy breve, de estilo humano”.

El responsable de AlphaGeometry 2, Thang Luong, describió el resultado como similar al famoso “movimiento 37” de la histórica victoria de DeepMind en Go, cuando el sistema de IA realizó un movimiento que ningún humano habría pensado y ganó. La prueba de AlphaGeometry 2 implicó construir un círculo alrededor de otro punto y luego usar ese círculo para demostrar la respuesta general. “Al principio, nuestro experto no entendía muy bien por qué construía ese punto”, dijo Luong. “Pero después de ver la solución, realmente conecta muchos triángulos entre sí y pensaron que la solución era realmente bastante elegante”.

La pregunta más fácil de AlphaGeometry 2…

Dejar A B C ser un triangulo con De < C.A. < antes de CristoSea el incentro y el círculo inscrito del triángulo A B C ser I y Vayarespectivamente. Sea X Sé el punto en la línea antes de Cristo diferente de C de tal manera que la línea que pasa por X Paralelo a C.A. es tangente a Vaya. De manera similar, sea Y Sé el punto en la línea antes de Cristo diferente de B de tal manera que la línea que pasa por Y Paralelo a De es tangente a Vaya. Dejar AI intersecar el círculo circunscrito del triángulo A B C De nuevo en P ≠ A. Dejar K y yo ser los puntos medios de C.A. y Derespectivamente.

Demuestre que ∠QUITAR + ∠YPX = 180◦.

Resuelto en 19 segundos.

…y el más difícil de AlphaProof

Turbo, el caracol, juega en un tablero con 2024 filas y 2023 columnas. En 2022 celdas hay monstruos ocultos. Al principio, Turbo no sabe dónde están los monstruos, pero sabe que en cada fila, excepto en la primera y la última, hay exactamente un monstruo y que cada columna contiene como máximo un monstruo.

Turbo hace una serie de intentos para ir desde la primera fila hasta la última. En cada intento, elige comenzar en cualquier celda de la primera fila y luego se mueve repetidamente a una celda adyacente que comparte un lado común. (Se le permite regresar a una celda visitada anteriormente). Si llega a una celda con un monstruo, su intento termina y es transportado de regreso a la primera fila para comenzar un nuevo intento. Los monstruos no se mueven y Turbo recuerda si cada celda que ha visitado contiene o no un monstruo. Si llega a cualquier celda de la última fila, su intento termina y el juego termina.

Determinar el valor mínimo de norte para lo cual Turbo tiene una estrategia que garantiza llegar a la última fila de la norteintento o antes, independientemente de la ubicación de los monstruos.

No resuelto.