Diez problemas, 4.802 páginas de respuestas
El Ramanujan Challenge puso en público diez problemas de teoría de números de nivel investigador. Ocho habían sido demostrados por los organizadores pero nunca publicados, lo que los mantiene fuera de cualquier conjunto de entrenamiento; dos eran conjeturas abiertas. Cada problema era una fórmula concreta para una constante matemática, de modo que la corrección podía comprobarse numéricamente aun cuando la demostración exigiera matemáticas no obvias.
Los participantes enviaron 228 propuestas. Entre todas contenían 4.802 páginas de demostraciones en lenguaje natural y 1.079.380 líneas de código en Lean, Python, Mathematica y Sage. El artículo de resultados, publicado el 29 de octubre por el grupo Ramanujan Machine del Technion de Haifa con coautores en la Universidad de Gante, el Research Institute for Symbolic Computation de Linz y la Toronto Metropolitan University, trata tanto de leer ese montón como de lo que hay en él.
Quién los resolvió
Las propuestas que produjeron demostraciones correctas en lenguaje natural usaron con más frecuencia modelos de las familias Claude y GPT. Las propuestas que combinaron Lean con un sistema de álgebra computacional superaron a las que se apoyaban en una sola herramienta, lo que los autores leen como un beneficio de diversificar la evidencia de apoyo más que como mérito de un demostrador concreto.
Una de las dos conjeturas abiertas publicadas recibió varias demostraciones correctas. Algunas de las demostraciones completas vinieron de matemáticos aficionados. Un participante no tenía educación matemática superior, y se halló que su solución a uno de los problemas era más simple que la de los propios organizadores. Un estudiante de secundaria avanzó de forma significativa hacia la demostración de una de las conjeturas.
Ese es el resultado que conviene separar de la puntuación del banco de pruebas. El reto se diseñó para medir modelos, y lo que midió fue un cambio en quién puede llegar siquiera a la teoría de números de nivel investigador.
El segundo problema que creó el reto
Juzgar las propuestas resultó ser la tarea más difícil. Los autores describen un auge de las matemáticas asistidas por IA que produce “una avalancha de afirmaciones matemáticas”, un problema que va mucho más allá de su propio banco de pruebas: 4.802 páginas no pueden arbitrarse como se arbitran diez artículos.
Los bancos de pruebas existentes lo abordan de distintas maneras: un único modelo de lenguaje como juez, un modelo que comprueba la equivalencia frente a una verdad de referencia conocida, o código determinista que verifica la respuesta de un modelo. El equipo construyó en su lugar una tubería asistida por IA que evalúa la corrección semántica y lógica en los tres formatos de entrega: lenguaje natural, código de álgebra computacional y formalizaciones en Lean.
Frente al juicio convencional de un modelo en una sola pasada, la tubería redujo los falsos positivos en demostraciones en lenguaje natural del 23% al 6%. La exactitud del juicio sobre el código de apoyo pasó del 46% al 58%.
Leídas al revés, esas son las cifras que importan. Un juez de una sola pasada dejaba pasar aproximadamente una de cada cuatro demostraciones erróneas en lenguaje natural, y acertaba con el código de apoyo menos de la mitad de las veces. Cualquier clasificación puntuada así informa tanto de su juez como de sus modelos.
Qué vigilar
Si los bancos de pruebas de matemáticas de nivel investigador publican su tasa de error de arbitraje junto a sus puntuaciones. El 6% residual sigue siendo un falso positivo en una propuesta de cada dieciséis, y el 58% sobre código es una mejora desde una base baja, no un problema resuelto. Los organizadores proponen su método como metodología para evaluar matemáticas de nivel investigador a escala, con aplicaciones en la IA para la ciencia. El artículo es un preprint y no ha sido revisado por pares; se publica bajo CC BY-SA 4.0.
