Introducción
Durante mucho tiempo, las matemáticas se han considerado una de las fronteras más difíciles para la inteligencia artificial.
Son altamente formales, densas en símbolos y dependen de cadenas de razonamiento largas. Además, exigen una corrección extrema en los pasos intermedios, lo que crea una tensión natural con aquello en lo que los grandes modelos de lenguaje suelen destacar: la generación fluida de texto.
Por eso, cada avance sustancial de la IA en matemáticas rara vez consiste solo en acertar algunas preguntas más. Casi siempre implica un salto de paradigma en el razonamiento y en la arquitectura del sistema.
En los dos últimos años, AI for Math ha pasado de ser una idea de moda a una realidad de ingeniería.
Por un lado, las puntuaciones en competición no dejan de subir. Por otro, cada vez hay más reflexión sobre la distorsión de las evaluaciones, la contaminación de datos y el razonamiento imposible de verificar.
Desde la perspectiva de alguien que lleva años construyendo productos educativos y desplegando sistemas de IA, este ensayo revisa:
- cómo ha cambiado la credibilidad real de los principales benchmarks matemáticos,
- cómo se estratifica en la práctica la capacidad matemática de los modelos punteros,
- por qué los sistemas de resolución basados en arquitectura están sustituyendo al prompting con un solo modelo,
- y qué direcciones merecen de verdad inversión en producto e investigación.
Si estás creando productos de IA relacionados con las matemáticas, este texto está escrito para ti.
1. La capacidad matemática de los LLM: de resolver ejercicios a manejar estructura
1.1 La evolución real de los benchmarks
Las primeras evaluaciones matemáticas giraban sobre todo alrededor de GSM8K / MATH / AIME.
Para 2025, ese conjunto ya se había fragmentado claramente.
GSM8K: casi saturado y con riesgo de contaminación ya demostrado
GSM8K fue durante un tiempo el benchmark de referencia para saber si un modelo realmente podía resolver problemas aritméticos verbales, pero hoy sus limitaciones son evidentes:
- el conjunto es pequeño y lleva mucho tiempo publicado,
- se solapa mucho con soluciones públicas,
- y varios trabajos ya han mostrado evidencia de contaminación del conjunto de entrenamiento.
Comparaciones controladas como GSM1k sugieren que un modelo con muy buena puntuación en GSM8K puede caer entre un 10% y un 15% en conjuntos limpios pero isomorfos. Ese patrón aparece de forma bastante consistente en estudios independientes.
AIME / AMC / MATH: siguen siendo útiles, pero hay que indicar la frescura
AIME sigue siendo uno de los benchmarks de competición escolar más usados, pero el consenso actual cambió:
- hay que indicar con claridad el año exacto del examen,
- y también el protocolo de evaluación: número de muestreos, uso de herramientas y mezcla o no con problemas antiguos.
En varias plataformas de evaluación, los modelos de primer nivel ya se acercan al 100% en AIME 2025.
Eso no significa que las matemáticas estén resueltas. Significa que los problemas estándar de competición están perdiendo rápidamente poder de discriminación frente a los sistemas punteros.
Nuevas direcciones más fiables: concursos en tiempo real y benchmarks anti-leaderboard
Para reducir la ilusión del ranking, en 2025 empezaron a ganar fuerza dos enfoques:
- flujos de competición en tiempo real como MathArena, que evalúan solo problemas recién publicados,
- subconjuntos duros como Apex, que filtran de forma deliberada los ítems demasiado favorables para los modelos.
En los problemas de demostración de la IMO 2025, los mejores modelos siguen por debajo del 40%.
En los subconjuntos más difíciles del estilo Apex, incluso los mejores sistemas rondan apenas el 5%.
Esos dos números describen mucho mejor el techo real que cualquier puntuación perfecta en AIME.
1.2 Niveles de capacidad en 2025
Nivel 1: Final Answer
En tareas del estilo AIME o AMC, modelos como GPT-5.x y Gemini 3 Pro ya están cerca de saturar el benchmark.
Ese nivel sigue teniendo valor para productos educativos, pero ya diferencia poco entre los sistemas líderes.
Nivel 2: Proof Writing
La escritura de demostraciones al nivel de la IMO sigue siendo una frontera dura. Los modelos suelen producir pruebas plausibles a primera vista, pero con huecos lógicos, así que la revisión humana sigue siendo necesaria.
Ese es el principal cuello de botella para aplicaciones educativas y de investigación.
Nivel 3: Formal Proof
Dentro de sistemas como Lean o Coq, los provers basados en arquitectura ya han alcanzado 80%+ en tareas como PutnamBench.
Pero el factor decisivo no es el tamaño del modelo, sino el bucle de ingeniería de generación -> verificación -> localización del fallo -> reparación local.
2. Evolución de la arquitectura: de Chain-of-Thought a sistemas de resolución
2.1 La capa de prompting cambió
Chain-of-Thought ayudó a hacer explícito el razonamiento intermedio, pero en matemáticas deja ver tres defectos estructurales:
- la estructura del razonamiento queda escondida en lenguaje natural y es difícil de verificar,
- un solo error contamina todo lo que sigue,
- no se alinea bien con las herramientas formales.
Por eso se ha vuelto más común otro patrón: Sketch-Proof.
- Primero se genera un esquema estructural: objetivos, lemas y ramas.
- Luego se completa el razonamiento de forma gradual y verificable.
2.2 Los sistemas basados en arquitectura se volvieron la norma
Los sistemas matemáticos más representativos de 2025 empezaron a parecerse bastante entre sí:
- pipelines de resolución por etapas,
- representaciones intermedias explícitas,
- uso profundo de verificadores externos.
El patrón típico se parece a esto:
- analizar el enunciado e inferir la intención matemática,
- generar un boceto de solución y descomponer subproblemas,
- invocar lemas o herramientas de cálculo,
- verificar, reparar localmente y recomponer.
El éxito de estos sistemas proviene más de la ingeniería de software que del número de parámetros por sí solo.
3. Garantías de corrección: cómo cerrar el bucle lógico
3.1 La verificación formal es la verdadera línea divisoria
Cuando Lean o Coq entran en el circuito, la IA matemática cambia de forma cualitativa:
- cada paso debe superar el chequeo de tipos,
- el lenguaje vago y los saltos lógicos quedan forzados fuera,
- los errores pueden localizarse en afirmaciones concretas.
Eso obliga a los modelos a abandonar las pruebas largas y difusas en lenguaje natural para acercarse a un razonamiento estructurado.
3.2 La autoreparación y la crítica del proceso pasaron a ser capacidades centrales
Los sistemas más nuevos suelen compartir tres capacidades:
- conciencia del fallo: detectar qué paso salió mal,
- reescritura local: cambiar solo lo necesario,
- ajuste de estrategia: evitar empezar desde cero sin criterio.
Módulos como Process Critic y Verifier-Formalizer están convirtiendo gradualmente a los modelos en sus propios revisores preliminares.
3.3 Una cadena de verificación madura se parece aproximadamente a esto
salida estructurada
-> comprobación computacional con herramientas
-> generación de aserciones formales
-> verificación SMT / simbólica
-> replanificación a partir del feedback y reintentos
Sin esa cadena completa, es muy difícil usar IA matemática en contextos serios.
4. Aplicaciones reales: qué ya está ocurriendo
4.1 Educación matemática
- La tutoría personalizada está pasando de la respuesta final a la ruta de resolución.
- Los sistemas de análisis de errores empiezan a guardar puntos de fallo estructural en lugar de solo respuestas.
- La corrección con IA empieza a combinar comprobaciones simbólicas y lógicas, no solo evaluación lingüística.
El valor real no es sonar humano, sino detectar dónde falló el razonamiento, por qué falló y qué conviene practicar después.
4.2 Investigación y producción de contenido matemático
- Las herramientas formales están reconfigurando los flujos de investigación.
- Los artículos antiguos se están estructurando y los lemas empiezan a reutilizarse.
- El conocimiento matemático empieza a volverse ejecutable.
En ese contexto, la IA realmente se parece más a un asistente de investigación paciente.
4.3 Consejos prácticos para quienes construyen productos
- Estandariza los datos del proceso de resolución.
- Trata a los verificadores como componentes de primera clase.
- Separa con claridad modelos de pensamiento, herramientas de ejecución y módulos de comprobación.
- No supongas que un solo modelo debe hacerlo todo.
Cierre
El valor de la IA en matemáticas nunca ha sido solo resolver ejercicios por las personas.
Lo importante es si puede ayudarnos a descomponer la estructura y volver el razonamiento trazable, verificable y reutilizable como parte del pensamiento humano, en lugar de un sistema opaco.
Si la primera etapa de los modelos de lenguaje consistió en hacer que las máquinas hablaran, entonces el objetivo a largo plazo de AI for Math debería ser enseñarles a pensar con responsabilidad, paso a paso.
Ese puede ser el verdadero comienzo de la entrada de la IA en el núcleo de la educación y de la ciencia fundamental.
Lecturas recomendadas
- AlphaGeometry: Symbol-free geometric theorem proving El sistema de DeepMind para demostración geométrica, centrado en modelado estructural y razonamiento coordinado
- ProofNet: Language Modeling for Theorem Proving in Lean Un trabajo representativo que combina modelos de lenguaje con demostración formal en Lean
- Seed-Prover: Multistage Math Problem Solving with Tool-augmented LLMs Un sistema multietapa y asistido por herramientas para resolver problemas matemáticos
- DeepSeek-Prover-V2 Technical Report Un LLM matemático especializado construido alrededor de bucles de generación-verificación y mezcla de expertos
- Lean Dojo Una plataforma abierta para entrenar modelos de lenguaje que interactúan con entornos de demostración en Lean