OpenAI afirma que un modelo secreto de IA resolvió cientos de problemas matemáticos abiertos con un solo prompt, y los matemáticos exigen pruebas

OpenAI publicó 722 manuscritos matemáticos en GitHub el martes, todos producidos por un modelo interno que la compañía no ha lanzado. Un portavoz de OpenAI dijo que casi todo provino de un único prompt entregado a un único agente de IA, aunque algunos pueden haber requerido múltiples intentos.

Es una afirmación audaz y un avance potencialmente significativo en el campo de las matemáticas. Pero no todos son fans, ni se creen el hype.

“Hasta que no publiquen el modelo y la gente pueda replicar sus resultados, creo que deberías tratar cualquier afirmación sobre resolver problemas de un solo golpe con un único agente como no verificada”, Andrew Sutherland, un matemático del MIT, dijo a Scientific American. “Deberíamos pedir recibos”, dijo.

Los artículos están agrupados en 372 “familias” de resultados relacionados, y una familia puede incluir un teorema principal junto con argumentos complementarios, consecuencias o pruebas alternativas. Eso hace que 722 sea un recuento de manuscritos, no de problemas resueltos. OpenAI dice que planteó aproximadamente 4.000 problemas al modelo y conservó los resultados que consideró lo suficientemente significativos como para publicarlos.

El resultado promedio utilizó el equivalente a aproximadamente tres horas de cómputo de pensamiento de ChatGPT Pro, según OpenAI. La afirmación sobre Navier-Stokes del mes pasado se veía muy diferente, con 10.000 agentes coordinadores trabajando durante 88 horas.

OpenAI publicó resúmenes abreviados de razonamiento para 10 de los resultados. Dicho esto, solo 162 de los 722 artículos vienen con un resultado principal verificado por computadora, según un catálogo de formalización en el repositorio. Eso es aproximadamente el 22% de la colección, traducido a Lean, un software que verifica cada paso lógico mecánicamente.

OpenAI mismo dice que no todos los manuscritos tienen formalizaciones en Lean y que "algunos de los resultados no formalizados podrían tener problemas". En otras palabras, mucho de lo que publicaron podría estar equivocado.

Una verificación de Lean superada confirma únicamente que la prueba se deriva del enunciado tal como está escrito en Lean. No demuestra que el enunciado coincida con el problema original, ni que el resultado sea nuevo o importante, que es la parte que los matemáticos ahora tienen que juzgar.

Y aquí es donde los investigadores levantan las cejas.

"Ahora ocurre que la IA puede producir argumentos matemáticos en situaciones en las que el humano que la instó no es capaz de entender los argumentos, verificarlos o asumir responsabilidad por ellos", dijo en un comunicado el Instituto de Estudios Avanzados de Princeton, Nueva Jersey. "Creemos que la comprensión humana de las matemáticas sigue siendo de suma importancia. ¿Cómo, en esta nueva era, podemos trabajar hacia un nuevo paradigma que incluya la comprensión humana de las matemáticas como parte de una producción académica responsable?".

Otros, sin embargo, como el profesor Abhishek Saha, están bastante entusiasmados. "Es un día muy importante para las matemáticas", escribió, pero señaló que la mayoría de los problemas encajan en las categorías de "avances excepcionales dentro de un programa existente" o de "avances sorprendentes".

Esto significa que la mayoría de los problemas del conjunto son interesantes, pero no imposibles ni revolucionarios como los problemas del milenio. Ese lugar está reservado para exactamente un problema de los 722: la Hipótesis Cuasi-Riemann.

El lanzamiento también se queda corto respecto a lo que un grupo asesor del Institute for Advanced Study recomendó el 29 de septiembre: el nombre del modelo, los prompts, una cadena de pensamiento resumida, el tiempo empleado y el coste computacional de cada resultado. OpenAI publicó cifras medias de cómputo y 10 resúmenes de razonamiento, pero ningún prompt, y afirma que sigue trabajando para publicar el modelo de forma responsable.

Daniel Litt, un matemático de la Universidad de Toronto, adoptó la postura opuesta, argumentando que no hay razón para pedir a la empresa que mantenga en secreto las respuestas a estas preguntas de matemáticas.

Anthropic tomó una ruta diferente con su prueba del Último Teorema de Fermat verificada con Lean el mes pasado, publicando las 13 millones de líneas públicamente en GitHub. Esa prueba formalizó un teorema que Andrew Wiles publicó en 1995, en lugar de reclamar resultados nuevos.

OpenAI dice que añadirá formalizaciones en Lean a medida que las obtenga; por ahora, 162 de los 722 manuscritos tienen una.