Google AI casi pierde la medalla de oro del IMO: resuelve problemas en 19 segundos asombrando a los jueces, habilidad geométrica supera a los humanos

El último modelo matemático de DeepMind obtuvo una medalla de plata en la Olimpiada Internacional de Matemáticas (IMO), demostrando un rendimiento excepcional. El modelo resolvió perfectamente 4 de los 6 problemas, quedándose a solo un punto de la medalla de oro. Particularmente en el problema 4, el modelo proporcionó una solución en tan solo 19 segundos, asombrando a los jueces humanos con su velocidad y calidad de resolución.

AlphaProof

AlphaProof es un sistema capaz de demostrar proposiciones matemáticas en el lenguaje formal Lean. Combina un modelo de lenguaje grande pre-entrenado con el algoritmo de aprendizaje por refuerzo AlphaZero.

Para superar las limitaciones de los lenguajes formales en el aprendizaje automático debido a los datos limitados escritos por humanos, los investigadores cerraron la brecha entre el lenguaje natural y las declaraciones formales mediante:

  1. El ajuste fino del modelo Gemini para traducir automáticamente los enunciados de problemas en lenguaje natural a declaraciones formales
  2. La creación de una gran biblioteca de problemas formalizados de diversa dificultad

Al resolver problemas, AlphaProof genera soluciones candidatas y las prueba o refuta buscando posibles pasos de prueba en Lean.

AlphaGeometry 2

AlphaGeometry 2 es un sistema híbrido neural-simbólico entrenado desde cero utilizando el modelo de lenguaje de Gemini. Puede resolver problemas de geometría más difíciles que su predecesor, incluyendo aquellos que involucran movimiento de objetos, ángulos, proporciones y ecuaciones de distancia.

Las mejoras clave incluyen:

  1. Entrenamiento con datos sintéticos un orden de magnitud mayor que la versión anterior
  2. Un motor simbólico dos órdenes de magnitud más rápido que antes
  3. Un novedoso mecanismo de intercambio de conocimientos que permite combinaciones avanzadas de diferentes árboles de búsqueda para resolver problemas más complejos

AlphaGeometry 2 ha demostrado capacidades impresionantes, resolviendo el 83% de los problemas de geometría de las IMO de los últimos 25 años, en comparación con el 53% de su predecesor. En la IMO de este año, resolvió el Problema 4 en solo 19 segundos después de recibir la pregunta formalizada.

El rendimiento de la IA en las IMO demuestra un progreso significativo en las capacidades de razonamiento matemático, acercando la IA a la resolución de problemas a nivel humano en matemáticas avanzadas.