La visión de un matemático sobre la capacidad matemática de la IA

• El nuevo modelo de lenguaje de OpenAI, o3, obtuvo 25% en el difícil benchmark matemático FrontierMath, reabriendo el debate sobre si la IA matemática puede superar el nivel de licenciatura
• FrontierMath es un conjunto de datos privado creado por Epoch AI, compuesto por cientos de problemas matemáticos difíciles que, más que “demostrar un teorema”, exigen respuestas numéricas verificables automáticamente
• Las 5 muestras publicadas no fueron fáciles ni siquiera para matemáticos de investigación; Tao las calificó como “extremadamente desafiantes”, pero Borcherds considera que dar una respuesta numérica no equivale a una prueba original
• Como Elliot Glazer de Epoch AI indicó que el 25% de los problemas eran de estilo IMO/licenciatura, es difícil confirmar, dada la naturaleza privada del dataset, a qué nivel de dificultad corresponde realmente el 25% logrado por o3
• Para los matemáticos, la meta más importante no es “encuentra este número”, sino demostrar correctamente un teorema y explicarlo de forma comprensible para los humanos; los modelos de lenguaje y los enfoques basados en Lean tienen limitaciones distintas

---

o3 y FrontierMath movieron la línea base

• o3 es el nuevo modelo de lenguaje de OpenAI y obtuvo 25% en FrontierMath
• Desde ChatGPT, los modelos de lenguaje públicos han mejorado rápidamente, y su capacidad para resolver problemas matemáticos también se evalúa dentro de esa tendencia
• FrontierMath es un dataset privado de problemas matemáticos creado por Epoch AI; en el resumen del paper se dice que contiene “cientos” de problemas difíciles
• Si el dataset se hiciera público, los modelos de lenguaje podrían aprenderse los problemas y las respuestas, por lo que incluso información básica como la cantidad exacta de preguntas se maneja con cuidado
  • Si se publican los problemas y sus respuestas, el modelo puede simplemente reproducir respuestas que ya vio
  • Por eso, desde fuera es difícil verificar la dificultad real y la representatividad de un benchmark privado

Formato y dificultad de los problemas de FrontierMath

• Los problemas de FrontierMath no son del tipo “demuestra este teorema”, sino más bien del tipo “encuentra este número”
• El problema debe tener una respuesta clara y computable, y esta debe poder verificarse automáticamente
• Las respuestas de las 5 muestras publicadas son todas enteros positivos
  • Entre las respuestas de ejemplo están 9811 y 367707
  • Las otras tres respuestas son más grandes, diseñadas para que sea difícil acertarlas al azar
• Las muestras publicadas no son triviales ni siquiera para matemáticos de investigación
  • El autor entendió los enunciados de los 5 problemas
  • El tercer problema podía resolverse relativamente rápido, y del quinto sabía un método estándar usando las Weil conjectures for curves, aunque no calculó la respuesta de 13 dígitos
  • Consideró que no podía resolver el primero ni el segundo, y pensó que en el cuarto quizá podría avanzar con esfuerzo, pero prefirió leer la explicación
• Incluso a un estudiante brillante de licenciatura en matemáticas podría costarle resolver cualquiera de estos problemas
  • El primer problema probablemente requiere nivel de doctorado o más en teoría analítica de números

Ventajas y límites de un benchmark de respuestas numéricas

• La razón principal por la que FrontierMath usa problemas con respuesta numérica es el costo de evaluación
• Para evaluar cientos de respuestas del tipo “demuestra este teorema” se necesitarían expertos humanos
  • A juicio del autor, en 2024 aún es difícil dejar ese nivel de corrección a una máquina
• En cambio, una lista de respuestas numéricas puede compararse muy rápido con una computadora
• Borcherds considera que los matemáticos de investigación pasan la mayor parte del tiempo buscando no números, sino pruebas e ideas
• Aun así, FrontierMath tiene valor dentro del campo de la IA matemática
  • Hay muy pocos datasets realmente difíciles
  • Crear este tipo de datasets es muy difícil o muy costoso
  • Un texto reciente de Frieder y otros profundiza más en las limitaciones de los datasets de IA matemática

Por qué sorprendió el 25% de o3

• La percepción previa era que la IA matemática estaba cerca de un nivel de licenciatura o inferior
• La IA se está volviendo muy fuerte en problemas estilo olimpiada, del tipo que resuelven estudiantes sobresalientes de preparatoria
• Parece claro que dentro de un año la IA podrá aprobar exámenes universitarios de matemáticas
  • Los exámenes de licenciatura suelen incluir problemas estándar que un estudiante que entendió el curso de manera básica puede aprobar
  • Una máquina puede resolver este tipo de problemas con facilidad
• Pero el salto desde reutilizar ideas estándar hasta llegar a ideas innovadoras de nivel avanzado de licenciatura o inicio de doctorado parece grande
• Las respuestas recientes de ChatGPT sobre el examen Putnam estuvieron por debajo de lo esperado
  • Parecía que la máquina respondió adecuadamente solo B4
  • La mayoría de las demás respuestas parecían de nivel 1 o 2 sobre 10
• Por estas razones, se esperaba que FrontierMath fuera casi inabordable durante varios años

La incertidumbre que deja un dataset privado

• Elliot Glazer de Epoch AI señaló en Reddit que el 25% de los problemas de FrontierMath eran de estilo IMO/licenciatura
• Esa afirmación no parece encajar bien con las 5 preguntas publicadas
  • Incluso el problema más fácil de las muestras publicadas admitía un enfoque usando Weil conjectures for curves
  • O también podría requerir una dolorosa búsqueda por fuerza bruta para factorizar un polinomio cúbico de grado 10^12 sobre un campo finito
• Esto deja dudas sobre la dificultad real del dataset privado y sobre si las 5 preguntas publicadas son una muestra representativa
• Como el dataset no es público, no es fácil comprobarlo
• Si ese 25% corresponde a problemas de nivel licenciatura, entonces el 25% de o3 podría ser menos sorprendente
• El gran avance esperado sería el momento en que la IA muestre un desempeño significativo en el siguiente 50% de problemas, descritos como de nivel “qual”

“Demuestra este teorema” sigue siendo otro problema

• En la investigación matemática, la pregunta importante suele ser “demuestra este teorema”
• Incluso si aparece una máquina con rendimiento sobrehumano en problemas de encontrar números, su aplicabilidad podría seguir siendo limitada en muchas áreas de la matemática de investigación
• El mayor caso de éxito de 2024 fue AlphaProof de DeepMind
  • AlphaProof resolvió 4 de los 6 problemas de la IMO 2024
  • Los problemas eran del tipo “demuestra este teorema” o “encuentra este número y demuestra que es correcto”
  • Tres de ellos se produjeron como pruebas completamente formalizadas en Lean
• Lean es un demostrador interactivo de teoremas, y mathlib es una biblioteca matemática que incluye muchas de las técnicas necesarias para resolver problemas de la IMO, y más
• Las soluciones del sistema de DeepMind fueron revisadas por humanos y verificadas como soluciones de “puntaje perfecto”
• Sin embargo, aunque los problemas de la IMO son muy difíciles, sus soluciones usan solo técnicas de nivel escolar, así que en cierto sentido esto sigue volviendo a problemas de nivel preparatoria
• Se espera que en 2025 una máquina muestre rendimiento de nivel medalla de oro en la IMO

¿Quién va a calificar la respuesta de una máquina?

• Es posible imaginar que en la IMO de julio de 2025 participen no solo estudiantes humanos, sino también máquinas
• Los sistemas de máquina podrían dividirse en dos tipos
  • Sistemas que entregan respuestas en lenguajes de verificadores de pruebas por computadora como Lean, Rocq o Isabelle
  • Modelos de lenguaje que entregan respuestas en lenguaje humano
• Las respuestas presentadas en lenguajes de verificadores de pruebas solo requieren comprobar que el enunciado del problema fue traducido correctamente
  • Después de eso, si la prueba compila, prácticamente ya se sabe que es una solución de “puntaje perfecto”
• Con los modelos de lenguaje que entregan respuestas en lenguaje natural, la situación es distinta
  • Aunque la respuesta parezca plausible, un corrector humano debe leerla y evaluarla con cuidado
  • No hay garantía de que sea una solución perfecta
• Se considera que los modelos de lenguaje son al menos un orden de magnitud menos precisos que un experto humano en razonamiento lógico
• Existe la preocupación de que una “prueba” generada por un modelo de lenguaje sobre la hipótesis de Riemann pueda mezclar afirmaciones vagas o imprecisas entre 10 páginas de matemáticas correctas
• En cambio, se considera que los demostradores de teoremas son al menos un orden de magnitud más precisos
  • En los casos que el autor ha visto donde Lean no aceptó un argumento de la literatura matemática humana, el lado humano estaba equivocado

Lo que falta: pruebas correctas y comprensión humana

• Lo que los matemáticos quieren no es simplemente “demuestra este teorema”, sino una prueba correcta y una explicación que los humanos puedan entender
• En el enfoque de modelos de lenguaje, la gran preocupación sigue siendo la “corrección”
• En el enfoque de demostradores de teoremas, la preocupación es si está presentado de una forma que los humanos puedan comprender
• Aún queda muchísimo por hacer
• El ritmo de avance es rápido, pero nadie sabe cuándo se superará la barrera de la licenciatura