La IA de DeepMind resuelve problemas de la Olimpiada Internacional de Matemáticas a nivel de medalla de plata
(deepmind.google)- En IMO 2024, una prueba de referencia para el razonamiento matemático de alta dificultad, AlphaProof y AlphaGeometry 2 de Google DeepMind resolvieron 4 de 6 problemas y alcanzaron por primera vez para una IA un rendimiento de nivel medalla de plata
- Obtuvieron 28 puntos de un total de 42, y todos los problemas resueltos recibieron puntaje perfecto; se quedaron a 1 punto del umbral de oro de 2024, que fue de 29 puntos
- La evaluación fue realizada por matemáticos siguiendo las reglas de calificación de la IMO; AlphaProof se encargó de álgebra y teoría de números, y AlphaGeometry 2 de geometría, combinando distintos enfoques de razonamiento
- Primero, los problemas se tradujeron manualmente a un lenguaje matemático formal; mientras que en la competencia los estudiantes disponen de dos sesiones de 4.5 horas, el sistema tardó desde unos minutos para un problema hasta 3 días para otros
- Este resultado muestra que la IA matemática ya va más allá del cálculo simple y se acerca a la exploración y verificación de demostraciones, aunque la entrada formalizada y los largos tiempos de resolución siguen siendo limitaciones importantes
Resultado de nivel medalla de plata en IMO 2024
- Google DeepMind presentó su sistema de razonamiento matemático AlphaProof y la versión mejorada de su sistema para resolver problemas de geometría, AlphaGeometry 2
- Los dos sistemas resolvieron 4 de los 6 problemas de la International Mathematical Olympiad 2024
- AlphaProof: resolvió 2 problemas de álgebra y 1 de teoría de números
- AlphaGeometry 2: demostró 1 problema de geometría
- No pudieron resolver los 2 problemas de combinatoria
- Cada problema vale 7 puntos y el total es de 42 puntos
- El sistema obtuvo puntaje perfecto en los 4 problemas resueltos y alcanzó 28 puntos
- Esto corresponde a la parte alta del rango de medalla de plata de la IMO 2024
- El umbral de medalla de oro en 2024 fue de 29 puntos, y en la competencia oficial 58 de 609 participantes alcanzaron ese nivel
- Es el primer caso en que un sistema de IA logra un resultado equivalente al de un medallista de plata en la IMO
Método de evaluación y condiciones de resolución
- Se usaron los problemas de la competencia proporcionados por los organizadores de la IMO
- Las respuestas se evaluaron según las reglas de asignación de puntaje de la IMO
- Los evaluadores fueron Prof Sir Timothy Gowers, medallista de oro de la IMO y ganador de la Medalla Fields, y Dr Joseph Myers, doble medallista de oro de la IMO y presidente del Problem Selection Committee de IMO 2024
- Para que el sistema pudiera entender los problemas, todos se tradujeron primero manualmente a un lenguaje matemático formal
- En la competencia oficial, los estudiantes entregan sus respuestas en dos sesiones de 4.5 horas cada una
- El sistema de IA resolvió un problema en pocos minutos y otros tardaron hasta 3 días
- Entre los problemas que resolvió AlphaProof estuvo el más difícil de IMO 2024, que solo pudieron resolver 5 participantes
AlphaProof: razonamiento formal basado en Lean
- AlphaProof es un sistema entrenado para demostrar proposiciones matemáticas en el lenguaje formal de Lean
- Combina un modelo de lenguaje preentrenado con el algoritmo de aprendizaje por refuerzo AlphaZero
- AlphaZero es el algoritmo usado para aprender por sí solo ajedrez, shogi y Go
- El uso de lenguaje formal permite la verificación exacta de demostraciones que incluyen razonamiento matemático
- Antes, había muy pocos datos de demostraciones formales escritas por humanos, lo que limitaba el uso de lenguaje formal en machine learning
- Los enfoques basados en lenguaje natural pueden usar muchos más datos, pero también pueden generar pasos intermedios o soluciones que parecen plausibles y aun así son incorrectos
- DeepMind ajustó finamente el modelo Gemini para traducir automáticamente problemas en lenguaje natural a proposiciones formales, y creó una biblioteca de problemas formales de distintas dificultades
- Cuando recibe un problema, AlphaProof genera candidatos de solución y luego intenta demostrarlos o refutarlos explorando pasos de prueba posibles en Lean
- Las demostraciones encontradas y verificadas se usan para reforzar el modelo de lenguaje de AlphaProof
- Este proceso iterativo se utiliza para aumentar la capacidad de resolver problemas más difíciles
- Durante la preparación para la IMO, entrenó durante varias semanas demostrando o refutando millones de problemas
- Incluso durante la competencia, se aplicó un ciclo de aprendizaje que reforzaba demostraciones sobre variantes autogeneradas de los problemas para encontrar soluciones completas
AlphaGeometry 2: expansión hacia problemas de geometría más difíciles
- AlphaGeometry 2 es una versión ampliamente mejorada de AlphaGeometry
- Este sistema tiene una arquitectura híbrida neuro-simbólica que combina redes neuronales y razonamiento simbólico
- El modelo de lenguaje está basado en Gemini
- Fue entrenado desde cero con un orden de magnitud más de datos sintéticos que la versión anterior
- Gracias a más datos y a un modelo mejorado, ahora puede abordar problemas geométricos más difíciles que incluyen movimiento de objetos y ecuaciones de ángulos, proporciones y distancias
- El motor simbólico de AlphaGeometry 2 es decenas de veces más rápido que el de la versión anterior
- Al recibir un nuevo problema, usa un nuevo mecanismo de compartición de conocimiento para aprovechar combinaciones avanzadas entre distintos árboles de búsqueda y manejar problemas más complejos
- Tasa de resolución de problemas de geometría de la IMO de los últimos 25 años:
- Antes de la competencia de 2024, AlphaGeometry 2 podía resolver el 83% de los problemas de geometría de la IMO de los últimos 25 años
- La tasa de resolución del AlphaGeometry anterior era del 53%
- En IMO 2024 resolvió Problem 4 en 19 segundos tras recibir la entrada formalizada
Razonamiento en lenguaje natural y usos futuros
- Como parte del trabajo para la IMO, DeepMind también experimentó con un sistema de razonamiento en lenguaje natural basado en Gemini y en investigación reciente
- Este sistema no necesita traducir los problemas a lenguaje formal y puede combinarse con otros sistemas de IA
- También probaron este enfoque con los problemas de la IMO 2024 y evaluaron los resultados como prometedores
- La metodología más técnica de AlphaProof fue publicada en un artículo de Nature
- DeepMind apunta a un futuro en el que los matemáticos exploren hipótesis junto con herramientas de IA, prueben nuevos enfoques para problemas antiguos y completen rápidamente las partes más demandantes en tiempo dentro de las demostraciones
3 comentarios
Cuantas más personas matemáticas contribuyan al desarrollo de bibliotecas de matemática formal, más fácil será crear una IA matemática de alto rendimiento. Hasta donde yo sé, actualmente hay 3 personas coreanas que están trasladando a Mathlib, la biblioteca matemática de Lean, teorías matemáticas que ellas mismas formalizaron directamente en el lenguaje del asistente de pruebas Lean.
El año pasado participé un poco en el trabajo de migrar Mathlib de Lean 3 a Lean 4, y este año demostré uno de los teoremas no resueltos de la biblioteca Batteries de Lean 4.
Opiniones de Hacker News
Esta noticia me entusiasma muchísimo, pero no queda claro cuánto trabajo está cargando la frase “primero una persona tradujo manualmente los problemas a un lenguaje matemático formal para que el sistema pudiera entenderlos”.
Todos los problemas que no eran de geometría tenían la forma “encontrar todos los X tales que...”, y los enunciados de los teoremas tenían la forma “demostrar que el conjunto de todos los X es {foo}”.
Viendo solo las soluciones descargables de https://storage.googleapis.com/deepmind-media/DeepMind.com/B..., es difícil saber si en la etapa de traducción una persona determinó {foo} o si lo encontró la computadora. Quiero creer que lo encontró la computadora, pero no encuentro una base para confirmarlo.
{1,1}, y en P62; en cada caso también presentó una demostración en Lean.A los humanos también les pasa a menudo cuando trabajan directamente con métodos formales, así que los investigadores probablemente concluyeron que, ya sea con LLM u otras herramientas, de todos modos habría que auditar todas las traducciones.
Sin embargo, no queda claro qué formalización inicial se le dio al agente para que esa etapa fuera posible.
Es decir, sea cual sea la forma de “problema” que reciba AlphaProof, y sea como sea que haya formalizado “encontrar todos los X tales que...”, probablemente genera teoremas candidatos en Lean. Por ejemplo, podría ser algo del estilo de que el conjunto tiene la forma
{n: P(n)}para alguna fórmula P. Después explora la demostración.Si AlphaProof no encontró {foo}, sino que se le dio de antemano, afirmar que resolvió el problema sería bastante absurdo. Aun así, este resultado me entusiasma mucho.
Sin duda es impresionante, pero cuando se menciona la IMO hace falta una salvedad. Las medallas se otorgan al 50% de los participantes, es decir, estudiantes de secundaria, y la proporción oro:plata:bronce es 1:2:3, por lo que los ganadores de oro y plata están en el 25% superior de todos los participantes.
Por lo tanto, sería más bien decir que “la IA resolvió problemas de la IMO mejor que el 75% de los estudiantes”, lo cual de hecho también podría sonar más impresionante.
Pero las condiciones de “un problema en unos minutos y cada uno de los demás en hasta 3 días” son distintas de las 9 horas que reciben los estudiantes, así que es difícil verlo como una comparación real. Si a los estudiantes también se les dieran hasta 15 días en vez de 9 horas, habría más personas que igualarían o superarían ese puntaje.
En la práctica, la IA solo resolvió un problema dentro de las 9 horas dadas a los estudiantes, así que probablemente habría quedado lejos de zona de medallas. Me pregunto si hacía falta empañar un resultado tan impresionante con una comparación de peras con manzanas.
De forma más objetiva, bastaría con informar que, aunque tardó más, resolvió X% de todos los problemas o obtuvo X puntos de un máximo de N.
Aquí el tiempo no es un eje tan interesante. Los humanos no usan CPUs equivalentes a enormes clústeres de GPU. La dicotomía más interesante es “si se le dan suficientes recursos, ¿puede llegar a la solución?”, y la respuesta de GPT/Claude era claramente no.
Estuvo muy cerca del corte, y normalmente incluso un pequeño avance puede valer 1 punto. Pero por razones técnicas no habría sido bueno que la prensa dijera que ganó una medalla de oro, así que parece que se conformaron con una plata sin controversia.
Esto es real. AlphaGeometry resolvía un conjunto de problemas muy limitado con mucha búsqueda por fuerza bruta.
Este método es mucho más amplio, y creo que tendrá un gran impacto en la forma de hacer matemáticas. Va de matemáticas en lenguaje natural a matemáticas formalizadas, y ahí realmente implementa un pipeline autosuficiente en el que se pueden entrenar tanto la formalización como las demostraciones.
En principio, este pipeline también puede aprender construcción teórica básica, como generar definiciones auxiliares y lemas. Está cerca del santo grial de la asistencia para demostraciones, y creo que permitirá formalizar gran parte de las matemáticas que producimos de manera natural. Los humanos trabajarán con un enfoque de rigurosización a posteriori, y las máquinas ayudarán a completar los detalles.
En cambio, este tipo de formalización abierta era un área en la que el progreso había sido muy lento y gradual. Hace 5 años trabajaba en un campo cercano, y creo que este resultado puede considerarse inalcanzable con las técnicas tradicionales de razonamiento automático.
La demostración automática de teoremas de verdad es útil en un ámbito mucho más amplio que las matemáticas puras. Por ejemplo, se podría escribir en Lean la semántica axiomática de un lenguaje de programación pequeño y plantear preguntas como “demuestra que existe un programa que satisface esta especificación”.
Si este enfoque escala, será más importante que cualquier otra aplicación de machine learning surgida en los últimos años.
La evolución que nos produjo también es una búsqueda basada en una cantidad enorme de intentos por fuerza bruta, y la investigación del método científico es, en esencia, búsqueda.
https://leandojo.org/
https://machine-learning-for-theorem-proving.github.io/
https://www.youtube.com/watch?v=P5ew0BrRm_I
https://paperswithcode.com/task/automated-theorem-proving
https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
https://github.com/RiccardoBiosas/LeanGPT
Para hacer cosas útiles no hace falta demostrar problemas extremadamente difíciles. Muchas veces basta con demostrar cosas simples. Si le pides a un modelo de lenguaje que complete tareas, ordene elementos, coordine horarios o escriba código que haga X, es difícil confiar de inmediato en el resultado; pero si el sistema puede traducir parte del problema a lógica y encontrar una solución, se vuelve mucho más confiable.
El punto central queda un poco enterrado: están usando Lean.
Esto es importante más allá de los problemas matemáticos. Hacer que los modelos de machine learning lidien con sistemas de demostración es una buena forma de evitar las tonterías habituales.
Espero que en el futuro más gente escriba tipos en Lean o sistemas similares y los use como una forma mucho mejor de escribir prompts.
polyrithse escribe con solo ocho caracteres. También vi que AlphaProof usabanlinarith.Hay un buen resumen breve de Tim Gowers que explica las principales advertencias y lo pone en contexto. Es medallista Fields y también participó en este trabajo: https://x.com/wtgowers/status/1816509803407040909
Es cierto, pero entrar al equipo nacional de cada país ya es en sí mismo un proceso muy difícil. En cada etapa, como las olimpiadas regionales de matemáticas y las nacionales, hay una selección brutal.
Después viene entrenamiento adicional para este grupo de élite, y en algunos casos también puede haber más rondas de selección.
En resumen, ser elegido para el equipo de la IMO de un país ya es algo enorme, y ganar una medalla de oro o plata dentro de ese grupo es simplemente un logro impresionante.
Fuente: un amigo que ganó medalla de plata en la IMO.
Envidio muchísimo a la gente a la que le pagan por hacer esto. Parece divertidísimo, y debe ser muy satisfactorio impulsar así el estado del arte
En la satisfacción laboral, creo que el entorno de trabajo importa más que el tema. Aunque trabajes en algo que cambia el mundo, si el equipo es un desastre, la vas a pasar mal. Hay gente que tiene talento para absorber toda la diversión, y la política interna existe en todas partes, especialmente en temas que cambian el mundo
En cambio, incluso en algo que parece de lo más aburrido, como meter datos de clientes en una base de datos, si tienes un equipo amable, una arquitectura bien diseñada y tiempo para experimentar y compartir conocimiento, puedes pasarla increíble. Cada vez valoro más la belleza de las cosas simples que simplemente funcionan bien. Eso puede ser incluso más raro que un avance científico
Claro que un gran entorno de trabajo y un gran tema pueden venir juntos, y eso se parece bastante a ganarse la lotería, así que sí da envidia
Debería emocionarme y sentirme agradecido de poder hacer este tipo de trabajo, pero las herramientas toscas le quitan mucha diversión
(/s)
Hace décadas que las máquinas juegan ajedrez mejor que los humanos
Aun así, a nadie le importa. Todos están ocupados viendo a Magnus Carlsen
Como somos humanos, nos interesa lo que hacen otros humanos. Las máquinas nos interesan solo en la medida en que nos ayudan
Este principio se extiende ampliamente al trabajo y al arte. Mientras existan los humanos, siempre habrá un lugar para lo humano en estos ámbitos
Pero dudo muchísimo que en el futuro cercano queden matemáticos que publiquen nuevos avances matemáticos que la IA no haya descubierto en su mayor parte o por completo. Un humano podría recibir crédito por la demostración por haber planteado la pregunta inicial, pero casi no existe un mundo en el que, si una computadora puede resolver fácilmente problemas matemáticos significativos, insistamos en que los humanos los resuelvan de forma más lenta y costosa
Este principio definitivamente aplica al arte, pero al trabajo solo en parte o en la mayoría de los casos
Entonces no hace falta entender la demostración, y a nadie le importa si algún matemático en alguna parte la entiende por completo. Que las máquinas sean mejores que nosotros para encontrar y verificar demostraciones está bien y, de hecho, se vuelve esperable
Muchos matemáticos no van a querer dedicarse a eso. Dicho esto, todavía hay una gran distancia entre la IMO y la frontera de la matemática de investigación
Siempre pensé que la demostración de teoremas es un juego de un solo jugador con un espacio de búsqueda absurdamente grande, así que se resolvería mucho antes que la AGI
Personalmente, creo que quienes más contribuyeron a AlphaProof son las personas detrás de Lean y Mathlib, porque asumieron la tarea abrumadora de formalizar toda la matemática
La falta de formalización en los artículos matemáticos ha matado una y otra vez los intentos de automatización, porque los investigadores de IA tenían que lidiar con elementos humanos como la notación propia de cada autor, el conocimiento implícito y los pasos de demostración omitidos
Creo que el término AGI en sí no está definido, pero no entiendo por qué alguien esperaría que crear “algo generalmente inteligente”, es decir, con inteligencia al nivel de la mediana humana, sea mucho más difícil que “ser mejor que Terrence Tao en matemáticas”
La mejor discusión está aquí: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...
Esa mejor discusión se puede ver aquí: https://leanprover.zulipchat.com/#narrow/stream/219941-Machine-Learnin…