- El modelo Gemini Deep Think de Google DeepMind logró en 2025 el puntaje de medalla de oro en la Olimpiada Internacional de Matemáticas (IMO) (35 puntos)
- Este modelo resolvió perfectamente 5 de 6 problemas, y la evaluación del jurado oficial de la IMO reconoció la claridad y precisión de sus demostraciones matemáticas
- Representa un gran salto frente al nivel de medalla de plata del año pasado (28 puntos) de AlphaProof y AlphaGeometry 2: comprendió problemas oficiales en lenguaje natural y completó demostraciones como un humano en 4.5 horas
- El modo Deep Think aplica pensamiento paralelo (parallel thinking) y el más reciente aprendizaje por refuerzo para explorar y sintetizar múltiples soluciones al mismo tiempo, optimizado para resolver problemas de estilo IMO
- Google planea ampliar la colaboración con matemáticos y avanzar hacia el desarrollo de una próxima generación de AGI que combine razonamiento matemático y verificación formal
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Gemini Deep Think de Google DeepMind obtuvo 35 puntos en total (resolviendo perfectamente 5 de 6 problemas) en la Olimpiada Internacional de Matemáticas (IMO) de 2025, alcanzando oficialmente el estándar de medalla de oro
- El jurado oficial de la IMO valoró altamente la claridad, precisión y facilidad de comprensión de las soluciones, y el presidente de la IMO, Prof. Dr. Gregor Dolinar, publicó una declaración oficial afirmando: "Google DeepMind ha alcanzado el puntaje de oro de 35 puntos"
- El año pasado, AlphaGeometry y AlphaProof requerían que expertos tradujeran los problemas de lenguaje natural a lenguajes específicos de dominio (como Lean), y los cálculos tomaban más de dos días. Este año, Gemini completó todo el proceso, desde la comprensión del problema hasta la redacción de la demostración, en lenguaje natural y dentro del tiempo de competencia de la IMO (4.5 horas)
Making the most of Deep Think mode
- Gemini Deep Think es un modo de razonamiento mejorado que aplica técnicas de investigación recientes, como el pensamiento paralelo (parallel thinking), para explorar varias rutas de solución al mismo tiempo y derivar la mejor respuesta
- El modelo fue entrenado con técnicas de aprendizaje por refuerzo para resolver problemas matemáticos complejos y con diversos datos de demostraciones de estilo IMO; además, se le incorporaron pistas y consejos generales sobre cómo abordar problemas de la IMO
- Está previsto que este modelo Deep Think se ofrezca primero en versión de prueba a algunos matemáticos y expertos de confianza, y más adelante se publique para suscriptores de Google AI Ultra
The Future of AI and Mathematics
- Google DeepMind mantiene su colaboración continua con la comunidad matemática y, además del razonamiento basado en lenguaje natural, sigue trabajando en investigación basada en sistemas formales, como AlphaGeometry y AlphaProof
- En el futuro, se espera que una IA que combine comprensión del lenguaje natural con capacidades de razonamiento matemático formal y verificable se convierta en una herramienta clave en matemáticas, ciencia, ingeniería e investigación
- DeepMind considera este logro un avance importante en el camino hacia la AGI (inteligencia artificial general), y planea afrontar en adelante problemas matemáticos aún más complejos y de mayor nivel
Verificación de respuestas y postura oficial de la IMO
- El comité organizador de la IMO confirmó oficialmente que las respuestas enviadas eran soluciones completas y correctas
- Sin embargo, también aclaró que la revisión de la IMO no incluye la validación del sistema, del proceso ni del modelo base en sí
- Para más detalles y para evitar interpretaciones exageradas, puede consultarse la declaración oficial de la IMO (Ver más)
5 comentarios
OpenAI anuncia haber logrado un rendimiento de nivel medalla de oro en la Olimpiada Internacional de Matemáticas (IMO) 2025
OpenAI lo anunció primero hace dos días, así que ya le quitó algo de emoción, pero también se comenta que fue una falta de etiqueta que Alexander Wei de OpenAI hablara antes sin siquiera discutirlo con la IMO.
Como ni siquiera había un reconocimiento oficial por parte de la IMO, dicen que al anunciarlo así se apropiaron de las felicitaciones y del mérito que correspondían a los participantes humanos, no a la IA.
Así que, al final, OAI solo logró que lo validara su propio panel, y quedó en una situación en la que ni siquiera recibió la calificación oficial de la IMO. Además, viendo que muchos opinan que la calidad de las respuestas de Gemini es un poco mejor... da la impresión de que la situación les deja todavía peor parados. No asumir ningún riesgo reputacional, anunciarlo si sale bien (encima sin una calificación oficial) y, si el resultado es malo, tomar distancia, podrá funcionar en benchmarks, pero no me parece la actitud correcta para mostrar en una competencia donde los participantes compiten poniendo su propio nombre en juego.
Aunque Google y OpenAI estén más o menos parejos en rendimiento de los LLM, aquí es donde se nota la diferencia en la experiencia de una empresa.
Opiniones en Hacker News
AlphaGeometry y AlphaProof primero traducían los problemas en lenguaje natural a un lenguaje especializado de dominio como Lean, y luego convertían de nuevo los resultados de la prueba a lenguaje natural; además, el cómputo tomaba entre 2 y 3 días. El modelo Gemini de este año, en cambio, usó un enfoque end-to-end que genera directamente pruebas matemáticas a partir de la descripción oficial del problema solo en lenguaje natural; es decir, no pasó primero por Lean. Aun así, no está claro si internamente usó herramientas como Lean, búsqueda en internet, calculadora o Python. OpenAI dijo que su modelo no usó ese tipo de herramientas, pero no estoy seguro de si eso aplica exactamente igual a Gemini. También me gustaría saber el nivel aproximado de cómputo, es decir, el costo, que usa cada sistema. Si el precio es enorme, eso significaría que todavía tiene poca utilidad práctica. Como aún no hay información pública, supongo que debe ser carísimo. Y compartieron un enlace donde se confirma “sin uso de herramientas, sin conexión a internet”: https://x.com/FredZhang0/status/1947364744412758305
El modelo Gemini de este año genera pruebas matemáticas a partir de la descripción oficial del problema usando solo lenguaje natural, y todo el proceso ocurre dentro de las 4.5 horas del concurso, sin usar herramientas externas.
Oficialmente se dice que herramientas de verificación formal como Lean no se usan al resolver realmente los problemas de la IMO, pero me pregunto si sí se usan durante el entrenamiento del modelo. En la investigación de Google sobre la IMO de 2024 existe una técnica para convertir pruebas en lenguaje natural a un lenguaje formalmente verificable, y me parece que el siguiente paso natural es usar eso para entrenamiento RLVR (verification-reward mediante aprendizaje por refuerzo). Si se pudiera traducir y verificar todo el razonamiento generado por un LLM matemático y usarlo como señal de recompensa, esa señal sería mucho más densa. Obtener una prueba formal perfecta seguiría siendo difícil, pero serviría para inducir al modelo a evitar razonamientos incorrectos o frases imposibles de interpretar. Con una cantidad enorme de cómputo, eso podría volver resolubles incluso problemas de dificultad IMO. AlphaProof ya mostró que es posible resolver problemas de nivel IMO explorando de manera eficiente el espacio de razonamiento entre pruebas en Lean y salidas de LLM. Me pregunto si, al saltarse los pasos intermedios y enseñar al LLM a imitar razonamiento formal con RLVR, no se podría lograr una eficiencia y capacidad de resolución parecidas.
También me pregunto por qué no usan Lean. ¿Significa que con Lean hoy en día resolver problemas se vuelve demasiado fácil, o que Lean en sí termina siendo más bien un obstáculo?
También me pregunto si eso de “sin uso de herramientas, sin conexión a internet” significa que realmente podría ejecutarse offline sin la infraestructura de Google, es decir, si sería posible desplegarlo localmente si fuera necesario.
Este año dicen que un Gemini más avanzado generó directamente pruebas matemáticas a partir de la descripción oficial del problema usando solo lenguaje natural, pero a mí me da algo de pena que eso implique alejarse de las técnicas de formalización. Creo que, para automatizar de verdad las matemáticas o llegar por ejemplo al nivel de producir mecánicamente pruebas de miles de páginas, no hay otro camino que la formalización. De lo contrario, seguirán haciendo falta revisores humanos y no habrá manera real de confiar en la prueba.
Si un LLM puede producir una prueba rigurosa en lenguaje natural, entonces demostrarla en un lenguaje formal como Lean tampoco debería ser tan difícil. En AlphaProof, el uso de Lean era bastante limitado y especializado para ciertos problemas matemáticos. En cambio, si con métodos RL y lenguaje natural se logra lo mismo, eso podría escalar a campos diversos donde la verificación es más complicada.
También compartieron que DeepMind actualmente está reuniendo repositorios que registran problemas formalizados aún no resueltos: https://github.com/google-deepmind/formal-conjectures
Soy matemático, aunque ya no hago investigación, y quisiera dar algo de contexto sobre por qué muchos matemáticos no son tan entusiastas con los métodos formales. En la práctica, para producir una prueba de miles de páginas obviamente es imposible prescindir de la formalización, y estoy de acuerdo en que, si uno quiere “confiar” en algo, hace falta verificarlo formalmente. Pero lo que los matemáticos realmente quieren es una explicación de por qué ese resultado es cierto. El verdadero producto no es una respuesta de sí o no, sino su interpretación y su razón de ser. Por ejemplo, casi todos creen que la hipótesis de Riemann probablemente es cierta, pero no se trata solo de esperar la respuesta final. Incluso hay muchos resultados del tipo “si la hipótesis de Riemann es cierta, entonces se cumple este nuevo teorema”. Lo que se espera de una prueba es, en el fondo, una intuición realmente nueva o una manera de brindar una comprensión profunda de la teoría de números. Si algo como Lean solo verifica formalmente que es verdadero pero los humanos ni siquiera pueden entenderlo, entonces eso casi no tiene sentido.
Como una formalización exacta suele ser más fácil que resolver el problema en sí, también es posible primero resolverlo y luego formalizarlo para confirmarlo.
Los problemas de la IMO están diseñados desde el inicio para que los humanos los resuelvan sin herramientas. Si se pone al modelo a resolver problemas más difíciles, entonces sí se le podrían dar herramientas sin problema. Como mínimo, me parece buena idea reproducir primero una capacidad de nivel humano sin herramientas.
Al comparar las respuestas de OpenAI y Gemini, la forma de escribir de Gemini se siente mucho más clara. La presentación podría mejorar un poco, pero el contenido de la prueba en sí es fácil de seguir, y está compuesto por frases más cortas y ordenadas que la respuesta de OpenAI.
La prueba de Google tal vez sea un resultado resumido a posteriori, y también es posible que el proceso de resumen sea parte de un mecanismo tipo Tree of Thoughts. No parece simplemente el resultado de una instrucción pasiva y directa de “da la respuesta final”.
Los resultados de las pruebas IMO mencionados de OpenAI y Google pueden verse respectivamente en PDF de la prueba de Google y repositorio con ejemplos de pruebas de OpenAI.
Tanto OpenAI como Google enfatizaron que “todo el proceso terminó dentro de las 4.5 horas del concurso”, pero no estoy seguro de que esa restricción tenga un significado importante. En la práctica, podrían haber ejecutado al mismo tiempo millones de procesos de razonamiento en paralelo para encontrar la prueba. Claro, eso requeriría también mucho cómputo en un modelo evaluador que valore los resultados y seleccione la prueba a entregar al final. En realidad, podría haber costado cientos de años de tiempo de GPU. Aun así, impresiona que este enfoque encuentre soluciones y que la paralelización sea posible hasta ese nivel. Al final, se logre o no AGI con más cómputo, el cerebro humano no escala así de fácil, así que el resultado claramente tiene importancia.
Es muy interesante que hayan pasado del sistema especializado en Lean del año pasado a un LLM generalista basado en lenguaje natural + RL. Espero que este enfoque también contribuya a mejorar el rendimiento fuera del ámbito de las competencias matemáticas, y tengo curiosidad por ver hasta dónde podrá escalar. Además, este sistema no parece diferir tanto del modelo/función “DeepThink” que planean lanzar en verano.
Ahora se siente como si estuviéramos viviendo un momento tipo Deep Blue vs. Kasparov en la competencia matemática entre máquinas. Ha habido un avance enorme respecto de hace apenas unos años, pero aun así creo que todavía falta muchísimo para un verdadero matemático de IA. De todos modos, vivimos en una época realmente asombrosa.
En un podcast reciente, Terrence Tao también mostró mucho interés en trabajar con herramientas de este tipo. Dijo que, por un tiempo, la mejor manera de usarlas probablemente sea que los humanos definan las ideas o parámetros y que el LLM haga en paralelo la exploración, las pruebas y demás. La analogía con los motores de ajedrez también encaja bien: antes, incluso los mejores ajedrecistas recibían ayuda analítica de equipos de expertos, pero hoy se analizan innumerables posiciones con supercomputadoras y software para extraer las mejores ideas y entregárselas al jugador.
Yo diría que se parece más a Deep Blue enfrentándose a un niño prodigio. Los participantes de la IMO no son matemáticos de clase mundial, sino estudiantes de secundaria.
La diferencia aquí es que no se puede sacar una puntuación alta dentro del tiempo límite solo con brute force. Es un verdadero hito técnico, y no como en la época de Deep Blue, donde era algo “posible en principio”.
El problema 6 resulta extraño. Ni OpenAI ni DeepMind pudieron dar una respuesta. Los humanos al menos entregan soluciones parciales, así que es raro que la IA no produzca nada. Eso me hace preguntarme si el LLM reconoció por sí mismo que no logró resolverlo. Uno de los límites de los LLM es que “no saben que no saben”, y en ese caso me parece casi imposible verificar consistencia lógica sin un solver.
Lo más probable es que no haya terminado de “pensar” dentro del límite de tiempo del concurso y por eso ni siquiera haya pasado a la etapa de “salida”.
Esa limitación aplica solo a la generación de texto de un LLM preentrenado en su forma más básica. También se podría entrenar adicionalmente un linear probe (una capa neuronal simple) para que emita un confidence score. Claro, eso no sería 100% confiable, pero al menos en un dominio acotado como matemáticas podría ser bastante útil.
Sin herramientas de verificación formal, todavía puede ser muy arriesgado usar esto en la práctica. o3, aunque ya no sea lo más reciente, antes era fuerte para encontrar bibliografía y proponer nuevas desigualdades. Pero en la etapa real de demostración podía dar respuestas que sonaban convincentes aunque incluyeran afirmaciones incorrectas o errores algebraicos en los detalles. Y a medida que los modelos mejoren, ese tipo de errores sutiles incluso podría volverse más difícil de detectar.
Me pregunto por qué enfatizan tanto que no usaron un theorem prover. Al final, cualquier herramienta que mejore el rendimiento del modelo debería ser bienvenida, ¿no? Además, Gemini también fue especializado para la IMO. Entrenaron el modelo con aprendizaje por refuerzo usando datos de razonamiento de varios pasos, resolución de problemas y demostración de teoremas, y también le dieron colecciones de explicaciones matemáticas de alta calidad y pistas sobre cómo abordar problemas de la IMO.
Supongo que la “versión avanzada de Gemini Deepthink” en realidad será distinta del Deepthink que vendrá en el producto de suscripción Gemini Ultra cuando se lance, o que habrá usado mucho más cómputo en tiempo de prueba (
test-time compute). Igual, es divertido ver competir a OpenAI y Google.Voy a compartir el enlace del system prompt de ingeniería de contexto que resolvió por completo los problemas 1 al 6; se puede usar con o3 o Gemini 2.5, solo hay que poner todo el prompt, agregar la pregunta y pedirle que resuelva el problema. https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf