La IA de DeepMind resuelve problemas de la Olimpiada Internacional de Matemáticas a nivel de medalla de plata

(deepmind.google)

3 puntos por GN⁺ 2024-07-26 | 3 comentarios | Compartir por WhatsApp

AlphaProof y AlphaGeometry 2 de Google DeepMind resolvieron problemas de la Olimpiada Internacional de Matemáticas
- AlphaProof: sistema de razonamiento matemático basado en aprendizaje por refuerzo
- AlphaGeometry 2: sistema mejorado para resolver problemas de geometría
- Ambos sistemas resolvieron 4 de los 6 problemas de la Olimpiada Internacional de Matemáticas (IMO) de este año, logrando un desempeño de nivel medalla de plata

Logros de la IA en la resolución de problemas matemáticos complejos

Introducción a la IMO
- La competencia juvenil de matemáticas más antigua y prestigiosa, celebrada cada año desde 1959
- Los problemas del concurso abarcan álgebra, combinatoria, geometría y teoría de números
- Muchos ganadores de la Medalla Fields participaron antes en la IMO
El reto de la IMO para los sistemas de IA
- AlphaProof y AlphaGeometry 2 resolvieron los problemas de la IMO de este año
- Los problemas se calificaron según las reglas oficiales del concurso
- AlphaProof resolvió 2 problemas de álgebra y 1 de teoría de números
- AlphaGeometry 2 resolvió 1 problema de geometría
- No lograron resolver los 2 problemas de combinatoria
- Obtuvieron 28 puntos de un total de 42, alcanzando un desempeño de nivel medalla de plata

AlphaProof: un enfoque de razonamiento formal

Cómo funciona AlphaProof
- Demuestra proposiciones matemáticas en el lenguaje formal Lean
- Combina un modelo de lenguaje preentrenado con el algoritmo de aprendizaje por refuerzo AlphaZero
- Traduce problemas en lenguaje natural a proposiciones formales para resolver problemas de distinta dificultad
- Cuando se le presenta un problema, AlphaProof genera candidatos de solución y los prueba o refuta
- Los resultados demostrados refuerzan el modelo de lenguaje de AlphaProof, mejorando su capacidad para resolver problemas más difíciles
Proceso de entrenamiento
- Fue entrenado demostrando o refutando millones de problemas
- Incluso durante el período del concurso se aplicó el ciclo de entrenamiento para demostrar variaciones de los problemas

AlphaGeometry 2, aún más competitivo

Mejoras de AlphaGeometry 2
- Un modelo de lenguaje basado en Gemini y un sistema híbrido neuro-simbólico
- Entrenado con 10 veces más datos sintéticos que la versión anterior
- Mejoras en velocidad y precisión para resolver problemas de geometría
- Usa un mecanismo de intercambio de conocimiento al resolver nuevos problemas
Resultados en la IMO 2024
- Resolución del 83% de los problemas de geometría de la IMO de los últimos 25 años
- En la competencia de este año resolvió el problema 4 en 19 segundos

Una nueva frontera del razonamiento matemático

Experimentos con sistemas de razonamiento en lenguaje natural
- Experimentos con un sistema de razonamiento en lenguaje natural basado en Gemini
- Puede resolver problemas sin traducirlos a un lenguaje formal
- Se explora la posibilidad de combinarlo con otros sistemas de IA
Perspectivas futuras
- Los matemáticos podrían colaborar con herramientas de IA para explorar nuevas hipótesis, probar enfoques de resolución y acortar procesos de demostración
- Sistemas de IA como Gemini pueden mejorar las capacidades matemáticas y de razonamiento general

Resumen de GN⁺

AlphaProof y AlphaGeometry 2 muestran el potencial de la IA en el razonamiento matemático
Al alcanzar un desempeño de nivel medalla de plata en la Olimpiada Internacional de Matemáticas, demuestran la capacidad de la IA para resolver problemas matemáticos
Abren la posibilidad de que los matemáticos colaboren con la IA para explorar nuevos enfoques de resolución de problemas
Un proyecto con funciones similares son los modelos de procesamiento de lenguaje natural como GPT-3 de OpenAI

3 comentarios

chabulhwi 2024-07-26

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.

GN⁺ 2024-07-26

Opiniones de Hacker News

Primera opinión
- Este proyecto me entusiasma mucho, pero no está claro cuánto aportó la computadora en el proceso de traducir los problemas matemáticos a un lenguaje formal
- En la solución descargable no queda claro si algo fue decidido por humanos durante el proceso de traducción o si lo encontró la computadora
Segunda opinión
- En la IMO, las medallas se otorgan al 50% de los participantes, y la proporción de medallas de oro, plata y bronce es de 1:2:3
- Es impresionante que la IA lo haya resuelto mejor que el 75% de los estudiantes
- Sin embargo, como el tiempo que le tomó a la IA resolver los problemas no es el mismo que el tiempo dado a los estudiantes en el examen, no es apropiado hacer una comparación directa
Tercera opinión
- AlphaGeometry resolvía problemas limitados, pero este método impactará a las matemáticas de una forma más amplia
- Están implementando un pipeline que convierte matemáticas en lenguaje natural a matemáticas formalizadas, y esto también puede aprender a construir teoría básica
- Este es el santo grial de los asistentes de demostración, y ayudará a que los humanos puedan formalizar matemáticas de manera más natural
Cuarta opinión
- Si al sistema le tomó 3 días resolver el problema, entonces no es distinto de una simple búsqueda por fuerza bruta
- Eso no es razonamiento real
Quinta opinión
- Están usando Lean
- Esto es importante no solo para los problemas matemáticos, sino también para evitar en general resultados sin sentido
- Ojalá más personas escriban tipos en sistemas como Lean
Sexta opinión
- Envidio a las personas que participan en este proyecto
- Debe ser muy divertido y gratificante impulsar tecnología de vanguardia
Séptima opinión
- La mejor discusión está ocurriendo en el chat de Zulip de LeanProver
Octava opinión
- Tim Gowers, ganador de la Medalla Fields, ofrece una buena visión general que explica las principales salvedades y aporta contexto
Novena opinión
- La demostración de teoremas es un juego para un solo jugador con un espacio de búsqueda muy grande
- Quienes más contribuyeron a AlphaProof fueron los desarrolladores de Lean y Mathlib
- La falta de formalización en los artículos matemáticos ha obstaculizado los intentos de automatización
Décima opinión
- Las máquinas han sido mejores que los humanos en ajedrez durante décadas
- Pero la gente sigue viendo a Magnus Carlsen
- A los humanos les interesan las acciones de otros humanos
- Las máquinas solo interesan en la medida en que sean útiles para los humanos