noticias

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

Nuevo informe de sabiduría

Editor: Departamento Editorial

[Introducción a la Nueva Sabiduría] ¡Justo ahora, el último modelo matemático de Google DeepMind ganó la medalla de plata de la Olimpiada de Matemáticas de la OMI! No solo resolvió 4 de las 6 preguntas con puntaje perfecto, a solo 1 punto de la medalla de oro, sino que también tomó solo 19 segundos para resolver la cuarta pregunta. La calidad y velocidad de resolución del problema sorprendieron a los jueces humanos que calificaron. .

¡La IA ha ganado la medalla de plata de la Olimpiada de Matemáticas de la OMI!

Hace un momento, Google DeepMind anunció que las verdaderas preguntas de la Olimpiada Internacional de Matemáticas de este año fueron producidas por su propio sistema de inteligencia artificial.

Entre ellos, AI no solo completó con éxito 4 de las 6 preguntas, sino que también recibió la máxima puntuación en cada pregunta, lo que equivale a la puntuación más alta de una medalla de plata: 28 puntos.

¡Este resultado está a sólo 1 punto de la medalla de oro!

Entre 609 concursantes, sólo 58 ganaron medallas de oro.

En la competición oficial, los concursantes humanos presentarán sus respuestas en dos sesiones, con un límite de tiempo de 4,5 horas cada vez.

Curiosamente, la IA solo tardó unos minutos en responder una de las preguntas, pero las preguntas restantes tardaron tres días completos, lo que se puede decir que es un tiempo de espera grave.

Esta vez las grandes contribuciones fueron dos sistemas de inteligencia artificial: AlphaProof y AlphaGeometry 2.

Punto importante: 2024 IMO no está en los datos de entrenamiento de estas dos IA.

Scott Wu, uno de los fundadores del ingeniero de IA Devin (tres veces medallista de oro del IOI) se lamentó: “Cuando era niño, lo único que tenía eran las Olimpiadas, nunca pensé que, apenas 10 años después, serían reemplazadas por la IA. . solucionado".

En la competencia de la OMI de este año, hay seis preguntas que involucran álgebra, combinatoria, geometría y teoría de números. Seis caminos son cuatro, sintamos el nivel de IA——

La capacidad de razonamiento matemático de la IA sorprende al profesor

Todos sabemos que la IA anterior se ha visto limitada a la hora de resolver problemas matemáticos debido a limitaciones en las capacidades de razonamiento y los datos de entrenamiento.

Los dos jugadores de IA que aparecieron juntos hoy rompieron esta limitación. son, respectivamente--

- AlphaProof, un nuevo sistema de razonamiento matemático formal basado en el aprendizaje por refuerzo

- AlphaGeometry 2, el sistema de resolución de problemas geométricos de segunda generación

Las respuestas dadas por las dos IA fueron calificadas de acuerdo con las reglas de los famosos matemáticos Profesor Timothy Gowers (medallista de oro de la OMI y medallista Fields) y Dr. Joseph Myers (dos veces medallista de oro de la OMI y presidente del Comité de selección de preguntas de la OMI para 2024). .

Al final, AlphaProof resolvió correctamente dos preguntas algebraicas y una pregunta de teoría de números. Una de las preguntas más difíciles fue resuelta por solo 5 concursantes humanos en AlphaGeometry 2 de este año;

Sólo hay dos problemas de matemáticas combinatorias que no han sido resueltos.

El profesor Timothy Gowers también quedó profundamente conmocionado durante el proceso de calificación——

Que un programa pueda encontrar una solución tan poco obvia es realmente impresionante y va mucho más allá de lo que esperaba dado el estado actual de la técnica.

Prueba alfa

AlphaProof es un sistema capaz de probar proposiciones matemáticas en el lenguaje formal Lean.

Combina un modelo de lenguaje grande previamente entrenado con el algoritmo de aprendizaje por refuerzo AlphaZero, que aprendió por sí solo a dominar el ajedrez, el shogi y el Go.

Una ventaja clave de los lenguajes formales es que pueden verificarse formalmente para pruebas que impliquen razonamiento matemático. Sin embargo, su aplicación en el aprendizaje automático ha sido limitada debido a la cantidad muy limitada de datos relevantes escritos por humanos.

Por el contrario, los enfoques basados ​​en el lenguaje natural, a pesar de tener acceso a grandes cantidades de datos, pueden producir pasos de razonamiento y soluciones intermedios plausibles, pero incorrectos.

Para superar esto, los investigadores de Google DeepMind perfeccionaron el modelo Gemini para traducir automáticamente enunciados de problemas en lenguaje natural en enunciados formales, creando una gran biblioteca que contiene problemas formales de diversa dificultad, construyendo así un puente entre los dos campos complementarios.

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

Cada prueba que se encuentra y verifica se utiliza para fortalecer el modelo de lenguaje de AlphaProof para que pueda resolver problemas más difíciles en el futuro.

Para entrenar AlphaProof, los investigadores probaron o refutaron millones de preguntas que cubrían una amplia gama de dificultades y áreas temáticas matemáticas desde las semanas previas a la competencia y durante ella.

Durante la competición, también aplicaron un ciclo de entrenamiento reforzando las pruebas sobre variaciones autogeneradas del problema de la competición hasta encontrar una solución completa.

Infografía del flujo del ciclo de entrenamiento de aprendizaje por refuerzo AlphaProof: la red formal traduce aproximadamente un millón de problemas matemáticos informales a un lenguaje matemático formal y luego la red de resolución se entrena gradualmente utilizando el algoritmo AlphaZero buscando pruebas o refutaciones de estos problemas; , para resolver problemas más desafiantes

Geometría alfa 2

AlphaGeometry 2, la versión mejorada de AlphaGeometry, es un sistema híbrido neuronal-simbólico entrenado desde cero basado en el modelo de lenguaje de Gemini.

Basado en un orden de magnitud más de datos sintéticos que la generación anterior, puede resolver problemas geométricos más difíciles, incluidas ecuaciones que involucran movimiento de objetos, ángulos, proporciones, distancias, etc.

Además, cuenta con un motor simbólico que es dos órdenes de magnitud más rápido que su predecesor. Cuando se encuentran nuevos problemas, utiliza un novedoso mecanismo de intercambio de conocimientos que permite combinaciones avanzadas de diferentes árboles de búsqueda para resolver problemas más complejos.

Antes de participar en IMO este año, AlphaGeometry 2 ya había logrado mucho éxito: podía resolver el 83% de los problemas de geometría de IMO en los últimos 25 años, mientras que la primera generación solo podía resolver el 53%.

En esta OMI, la velocidad de AlphaGeometry 2 sorprendió a todos: ¡a los 19 segundos de recibir la pregunta formal, resolvió la pregunta 4!

La pregunta 4 requiere prueba de que la suma de ∠KIL y ∠XPY es igual a 180°. AlphaGeometry 2 recomienda construir un punto E en la línea BI tal que ∠AEB=90°.El punto E ayuda a determinar el punto medio L de AB, formando muchos pares de triángulos similares, como ABE ~ YBI y ALE ~ IPC, demostrando así la conclusión.

Proceso de resolución de problemas de IA

Vale la pena mencionar que estas preguntas primero se traducirán manualmente al lenguaje matemático formal antes de enviarlas a AI.
P1

En términos generales, la primera pregunta (P1) de cada prueba IMO es relativamente sencilla.

Los internautas dijeron: "P1 solo requiere conocimientos de matemáticas de la escuela secundaria y los jugadores humanos generalmente lo completan en 60 minutos".

La primera pregunta de IMO 2024 examina principalmente las propiedades del número real α y requiere encontrar un número real α que satisfaga ciertas condiciones.

AI dio la respuesta correcta: α es un número entero par. Entonces, ¿cómo se responde exactamente?

En el primer paso para resolver el problema, AI primero dio un teorema de que los conjuntos izquierdo y derecho son iguales.

El conjunto de la izquierda representa que todos los números reales α que cumplen las condiciones, para cualquier entero positivo n, n puede dividir ⌊i*α⌋ de 1 a n; el conjunto de la derecha representa que hay un entero k, k es; un número par y el número real α es igual a k.

La siguiente prueba se divide en dos direcciones.

Primero demuestre que el conjunto de la derecha es un subconjunto (dirección simple) del conjunto de la izquierda.

Luego, demuestre que el conjunto de la izquierda es un subconjunto del conjunto de la derecha (dirección difícil).

Hasta el final del código, a la IA se le ocurrió una ecuación clave ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋), usando la ecuación para demostrar que α debe ser un número par.

Finalmente, DeepMind resumió los tres axiomas en los que se basa la IA en el proceso de resolución de problemas: propext, Classical.choice y Quot.sound.

El siguiente es el proceso completo de resolución de problemas de P1: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

P2

La segunda pregunta examina la relación entre el par de números enteros positivos (a, b), que involucra la propiedad del máximo común divisor.

La respuesta resuelta por la IA es:

El teorema es que para un par de enteros positivos (a, b) que satisfacen ciertas condiciones, su conjunto solo puede contener (1,1).

En el siguiente proceso de resolución de problemas, la estrategia de prueba adoptada por AI es probar primero que (1,1) satisface las condiciones dadas y luego demostrar que ésta es la única solución.

Demuestre que (1,1) es la solución final, usando g=2, N=3.

Demuestre que si (a,b) es la solución, entonces ab+1 debe dividir g.

En este proceso, la IA utilizó el teorema de Euler y las propiedades de las operaciones modulares para razonar.

Finalmente, demuestre que a=b=1 es la única solución posible.

El siguiente es el proceso completo de resolución de problemas de P2: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

P4 es una pregunta de prueba geométrica que requiere probar una relación de ángulo geométrico específica.

Como se mencionó anteriormente, AlphaGeometry 2 completó esto en 19 segundos, estableciendo un nuevo récord.

Dependiendo de la solución dada, como ocurre con AlphaGeometry de primera generación, el modelo de lenguaje genera automáticamente puntos auxiliares en todas las soluciones.

En la prueba, todo seguimiento de ángulos utiliza eliminación gaussiana, y d(AB)−d(CD) es igual al ángulo direccional de AB a CD (módulo π).

Durante el proceso de resolución de problemas, la IA marcará manualmente pares de triángulos similares y triángulos congruentes (marcados en rojo).

A continuación, se detallan los pasos para resolver el problema de AlphaGeometry, que se completa utilizando el "método de recontradicción".

Primero utilice Lean para formalizar las proposiciones que deben probarse y visualizar la construcción geométrica.

Los pasos clave en la prueba son los siguientes.

Vea la imagen a continuación para ver el proceso completo de resolución de problemas: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

La sexta pregunta de la OMI es el "jefe final", que explora las propiedades de las funciones y requiere demostrar conclusiones específicas sobre los números racionales.

AI resuelve, c=2.

Primero veamos el enunciado del teorema, que define las propiedades de la "función acuesuliana" y declara que para todas esas funciones, el conjunto de valores de f(r)+f(-r) tiene como máximo 2 elementos.

La estrategia de prueba es demostrar primero que para cualquier función acuesuliana, el conjunto de valores de f(r)+f(-r) tiene como máximo 2 elementos. Luego construya una función acuesuliana específica para que f(r)+f(-r) tenga exactamente 2 valores diferentes.

Demuestre que cuando f(0)=0, f(x)+f(-x) toma como máximo dos valores diferentes, y demuestre que no existe una función acuesuliana f(0)≠0.

Construya la función f(x)=-x+2⌈x⌉ y demuestre que es una función acuesuliana.

Finalmente, demuestre que para esta función, f(-1)+f(1) =0 y f(1/2)+f(-1/2)=2 son dos valores diferentes.

El siguiente es el proceso completo de resolución de problemas: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

Puedes hacer preguntas de matemáticas de la Olimpiada, pero ¿puedes decir cuál es más grande, 9,11 o 9,9?

Andrew Gao, investigador de la Universidad de Stanford y Sequoia, afirmó la importancia de este avance de la IA——

La clave es que las últimas preguntas de la prueba de la OMI no están incluidas en el conjunto de capacitación. Esto es importante porque demuestra que la IA puede manejar problemas nuevos e invisibles.

Además, los problemas geométricos resueltos con éxito por la IA siempre se han considerado extremadamente desafiantes debido a la naturaleza del espacio involucrado (que requiere pensamiento intuitivo e imaginación espacial).

Jim Fan, científico senior de Nvidia, publicó un largo artículo diciendo que los modelos grandes son existencias misteriosas——

Pueden ganar medallas de plata en olimpiadas de matemáticas y frecuentemente cometen errores en preguntas como "¿Qué número es mayor, 9,11 o 9,9?"

No solo Gemini, sino también GPT-4o, Claude-3.5 y Llama-3 no pueden responder 100% correctamente.

Al entrenar modelos de IA, estamos explorando vastas áreas más allá de nuestra propia inteligencia.En el proceso, descubrimos un área muy extraña: un exoplaneta que se parece a la Tierra pero está lleno de valles extraños.

Esto parece irrazonable, pero podemos explicarlo utilizando la distribución de datos de entrenamiento:

AlphaProof y AlphaGeometry 2 están entrenados en pruebas formales y motores simbólicos de dominio específico. Hasta cierto punto, son mejores para resolver problemas especializados de Olimpiada, aunque se basan en un LLM de propósito general. El conjunto de entrenamiento de GPT-4o se mezcla con una gran cantidad de datos de código de GitHub, que pueden exceder con creces los datos matemáticos. Entre las versiones de software, "v9.11 > v9.9" puede distorsionar gravemente la distribución de datos. Por tanto, este error es comprensible hasta cierto punto.

El jefe de desarrolladores de Google dijo que los modelos que pueden resolver problemas matemáticos y físicos difíciles son el camino clave hacia AGI, y hoy hemos dado un paso más en este camino.

Otros internautas dijeron que hubo demasiada información esta semana.

Referencias:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

https://x.com/DrJimFan/status/1816521330298356181