Astra de OpenAI logra hitos matemáticos con verificación automática

  • Astra, el próximo modelo de OpenAI, ha resuelto diez problemas matemáticos abiertos de larga duración.
  • Los resultados están verificados con Lean, un sistema que comprueba cada paso automáticamente.
  • El coste computacional fue inferior a 2.000 dólares, aunque solo se cuentan los éxitos.
  • La comunidad matemática recibe el anuncio con asombro y cautela, con reacciones encontradas.

OpenAI Astra modelo de inteligencia artificial

OpenAI ha vuelto a poner el foco en la inteligencia artificial con un anuncio que ha sacudido a la comunidad matemática. Su próximo modelo, Astra, ha logrado resolver diez problemas abiertos que llevaban décadas sin respuesta, y lo ha hecho con un método que permite verificar cada paso de forma automática. No es un logro menor: hablamos de cuestiones que han resistido los intentos de los mejores especialistas durante años, y que ahora han caído gracias a un sistema entrenado para razonar de forma autónoma.

La compañía ha publicado los resultados en una colección de manuscritos que incluye 249 páginas de argumentos y certificados formales generados con Lean, un software que comprueba la validez de las demostraciones paso a paso. Además, el coste computacional de estos hallazgos ha sido sorprendentemente bajo: menos de 2.000 dólares en tokens de su API. Pero, ¿qué significa realmente este avance? ¿Estamos ante un punto de inflexión en la investigación matemática o hay que tomarlo con cautela?

OpenAI duplicará su plantilla para 2026
Artículo relacionado:
OpenAI planea duplicar su plantilla para impulsar la carrera de la IA

Diez problemas matemáticos de décadas resueltos

Los resultados abarcan áreas tan diversas como la geometría de alta dimensión, la teoría de códigos, la complejidad de circuitos aritméticos, la teoría de grupos, la complejidad cuántica, la criptografía reticular y la combinatoria extremal. Entre los hitos más destacados se encuentra la refutación de la conjetura de rigidez de Connes, un problema histórico en álgebras de operadores, y la construcción de grupos no sóficos, una cuestión que llevaba años ocupando a los especialistas. También se ha mejorado el límite superior para la densidad de empaquetamiento de esferas en altas dimensiones, una cota que permanecía sin cambios desde 1978.

Además, Astra ha resuelto tres problemas del catálogo de Paul Erdős, incluyendo el conocido como Problema 21, que ha sido calificado por el matemático Thomas Bloom como «el más sorprendente de toda la lista». En total, son diez problemas que llevaban al menos una década sin avances significativos, y en la mayoría de los casos mucho más tiempo. La comunidad matemática ha recibido la noticia con una mezcla de asombro y escepticismo, como era de esperar.

OpenAI Astra inteligencia artificial

Verificación automática con Lean

Lo que hace diferente este anuncio de otros similares es la verificación. Cada demostración ha sido formalizada en Lean, un asistente que comprueba cada paso lógico de forma automática. Los certificados están disponibles públicamente en GitHub, y cualquiera puede descargarlos y ejecutar el verificador. Si un solo paso no se deduce correctamente, el software lo rechaza. Esto elimina la necesidad de confiar en la palabra de OpenAI: la validez de los resultados se puede comprobar de forma independiente.

Nvidia entra en el capital de Intel
Artículo relacionado:
Nvidia entra en el capital de Intel y sella una alianza estratégica en IA

Este método contrasta con la forma tradicional de validar demostraciones matemáticas, que requiere un proceso de revisión por pares que puede durar meses. Con Lean, la verificación se reduce a unos minutos. Los investigadores han destacado que esta es la primera vez que un sistema de IA presenta resultados con un nivel de transparencia tan alto. Sin embargo, algunos expertos como Bharath Ramsundar advierten que «estamos construyendo rápidamente una torre de resultados de IA ‘quizás verdaderos’» y piden que los matemáticos humanos revisen los hallazgos antes de integrarlos en el corpus establecido.

OpenAI Astra modelo de IA

El coste y la selección de problemas

Otro dato que ha llamado la atención es el coste. OpenAI asegura que el número total de tokens necesarios para encontrar soluciones a estos problemas costaría aproximadamente 2.000 dólares según las tarifas de su API. Pero esta cifra solo refleja las ejecuciones que tuvieron éxito, no los intentos fallidos. Como señala un experto, «es como si me toca la lotería y digo que habiéndome gastado 20 euros en un billete he ganado 20.000, pero no cuento los 5.000 euros que me gasté en décimos anteriores». El coste real del proceso de descubrimiento es mucho mayor.

Además, OpenAI ha seleccionado los problemas que decidió publicar. No se sabe cuántos problemas intentó Astra y falló. Si seleccionó 10 éxitos de 1.000 intentos, la interpretación es muy diferente que si fueron 10 de 12. Hasta que no se conozca el denominador, el «momento Deep Blue de las matemáticas» sigue siendo más titular que conclusión. Aun así, los resultados son verificables, y eso es un avance cualitativo respecto a anuncios anteriores.

OpenAI Astra tecnología

Reacciones de la comunidad matemática

El ganador de la Medalla Fields, Tim Gowers, ha afirmado que habría recomendado sin dudarlo la publicación de la demostración en una de las principales revistas de matemáticas. Un equipo de nueve matemáticos, entre ellos Gowers y Noga Alon, ha publicado un artículo complementario que explica la demostración de forma más accesible. Thomas Bloom, responsable del catálogo de problemas de Erdős, ha calificado los resultados como «una noticia de gran importancia» y asegura que son incluso más relevantes que la resolución de la conjetura de la distancia unitaria, lograda por Astra en mayo.

Pero también hay voces críticas. Gary Marcus, conocido escéptico de la IA, ha calificado el anuncio de «asombroso» pero considera que su alcance ha sido exagerado. Algunos especialistas creen que solo unas pocas de las diez demostraciones se considerarán realmente sorprendentes, mientras que las demás corresponden a problemas cuya resolución estaba al alcance de la comunidad, aunque nadie se hubiera dedicado a abordarlos. A pesar de las críticas, el hecho de que los resultados sean verificables automáticamente marca una diferencia fundamental con otros anuncios de IA.

En definitiva, el anuncio de OpenAI con Astra representa un hito en la aplicación de la inteligencia artificial a la investigación matemática. Por primera vez, un sistema de IA ha resuelto problemas abiertos de larga duración y ha proporcionado pruebas verificables por máquina. Aunque quedan dudas sobre la selección de los problemas y el coste real, la transparencia del proceso y la posibilidad de comprobar cada paso abren la puerta a una nueva era en la que la IA colaborará con los matemáticos humanos. La comunidad científica tendrá que adaptarse a esta nueva realidad, pero lo que está claro es que la frontera del conocimiento se ha movido, y Astra ha sido la herramienta que lo ha conseguido.

Novo Nordisk se asocia con OpenAI
Artículo relacionado:
Novo Nordisk se asocia con OpenAI para impulsar la IA en salud

Añadir como fuente preferida en Google