El coste de obtener nuevos resultados sobre diez problemas matemáticos abiertos desde hace décadas se ha reducido hasta 2.000 dólares, según OpenAI, que asegura que su modelo Astra ha generado demostraciones matemáticas verificables por máquina para cuestiones que habían resistido los avances de los investigadores durante décadas.
OpenAI publicó estos trabajos el 1 de agosto y los utilizó para presentar el nombre de su próxima gran familia de modelos: Astra. Los resultados abarcan áreas como la teoría de grupos, la geometría de altas dimensiones, la teoría de códigos, la complejidad cuántica, la criptografía basada en retículas y la combinatoria extremal.
Los avances se presentaron en una colección de manuscritos de 249 páginas y, junto a ellos, se incluyó algo inédito hasta ahora en una afirmación de este tipo por parte de un sistema de inteligencia artificial: un certificado verificable por máquina para cada uno de los resultados.
No se trataba de ejercicios académicos presentados como si fueran descubrimientos. Todos los problemas llevaban al menos diez años sin resolverse, la mayoría bastante más tiempo, y varios ocupan un lugar central dentro de sus respectivas áreas de investigación.
Entre los resultados destacan:
- Una construcción que demuestra la existencia de grupos no sóficos, una cuestión que ha ocupado a los especialistas en teoría de grupos durante años.
- Una refutación de la conjetura de rigidez de Connes, un problema histórico de la teoría de las álgebras de von Neumann.
- Una mejora del límite superior general para la densidad de empaquetamiento de esferas en altas dimensiones, una cota que permanecía sin cambios desde 1978.
- La resolución de tres problemas pertenecientes al catálogo de cuestiones abiertas dejado por el matemático Paul Erdős.
Este anuncio llega pocos meses después de otro resultado atribuido a la misma familia de modelos. En mayo, Astra habría refutado la conjetura de la distancia unitaria de Erdős, un problema de 80 años de antigüedad en geometría discreta que había resistido todos los intentos serios de resolución desde 1946.
El ganador de la Medalla Fields, Tim Gowers, afirmó que habría recomendado sin dudarlo la publicación de la demostración en una de las principales revistas de matemáticas. Posteriormente, un equipo de nueve matemáticos, entre ellos el propio Gowers y Noga Alon, publicó un artículo complementario en el que explica la demostración de una forma más accesible para la comunidad matemática.
Por su parte, Thomas Bloom, responsable del catálogo de problemas abiertos de Erdős, calificó los resultados publicados en agosto como «una noticia de gran importancia» y aseguró que son aún más relevantes que la anterior resolución de la conjetura de la distancia unitaria.
El investigador de OpenAI Noam Brown aportó una nota de cautela al afirmar: «Lamentablemente, todavía no hemos resuelto ninguno de los Problemas del Milenio».
Por qué estas demostraciones son importantes
Todos los grandes anuncios sobre capacidades de la inteligencia artificial realizados en los últimos tres años han compartido una misma debilidad: la empresa que hace la afirmación es también la única que puede verificarla. Los modelos se evalúan con pruebas potencialmente contaminadas, las demostraciones públicas se seleccionan cuidadosamente y el resto de la comunidad acaba debatiendo si los resultados realmente significan algo.
Con Astra, la situación es diferente. Sus demostraciones fueron formalizadas en Lean, un asistente de demostraciones matemáticas que verifica paso a paso cada argumento, y los archivos con los certificados se publicaron en GitHub bajo una licencia abierta.
Cualquier persona puede descargarlos y ejecutar el verificador. Si un solo paso de la demostración no se deduce correctamente del anterior, el software la rechaza automáticamente. No hay margen para la interpretación ni es necesario convencer a ningún comité de expertos.
Habitualmente, cuando se presenta una demostración de un problema matemático de gran relevancia, esta entra en un proceso de revisión por pares durante el cual expertos analizan durante meses la validez de cada paso lógico antes de que la comunidad científica determine si la prueba resiste el escrutinio. En este caso, el certificado de Lean reduce ese proceso al tiempo que tarda en descargarse el archivo. La verificación y la publicación se produjeron el mismo día.
Esa característica es excepcional y explica por qué este anuncio difiere de la simple publicación de una puntuación en un benchmark. Una demostración verificada no exige confiar en quien la ha producido, porque cualquiera puede comprobar su validez.
Lo que los escépticos tienen razón al señalar
Hay tres objeciones que conviene tomar en serio, y una lectura honesta de los hechos obliga a reconocer que todas tienen fundamento.
En primer lugar, OpenAI pudo haber seleccionado los problemas que decidió publicar. Además, la cifra de 2.000 dólares hace referencia únicamente a las ejecuciones que tuvieron éxito, no a todos los intentos realizados por el modelo. En ese sentido, representa más bien el coste de obtener un resultado publicable que el coste real del proceso de descubrimiento.
En segundo lugar, investigadores externos han señalado que empleados de OpenAI participaron en la preparación de los artículos y en la formalización de las demostraciones, aunque la compañía sostiene que el contenido matemático fue generado por Astra.
Por último, ningún investigador ajeno a OpenAI puede ejecutar el modelo que produjo estos resultados. Es decir, las demostraciones pueden verificarse de forma independiente, pero no reproducirse.
El investigador Gary Marcus, uno de los críticos más conocidos del sector de la inteligencia artificial, calificó el anuncio de «asombroso», aunque consideró que su alcance había sido muy exagerado. Algunos especialistas creen que, una vez pase el entusiasmo inicial, solo unas pocas de las diez demostraciones se considerarán realmente sorprendentes, mientras que las demás corresponderán a problemas cuya resolución estaba al alcance de la comunidad, aunque nadie se hubiera dedicado aún a abordarlos.
Incluso aceptando todas esas objeciones, el argumento de fondo permanece intacto. Tanto si los diez problemas fueron cuidadosamente seleccionados como si no, los certificados siguen verificando las demostraciones. Un resultado escogido de forma selectiva pero verificable automáticamente es, en esencia, algo muy distinto de un resultado igualmente seleccionado que no puede comprobarse de manera independiente.
Donde el resultado verificable ya funciona
La implantación de la inteligencia artificial suele frenarse por una razón que tiene poco que ver con la capacidad del modelo. Una empresa no puede utilizar resultados que no tiene forma de verificar, y la revisión humana deja de ser escalable mucho antes de que lo haga la producción de la IA. Un analista puede revisar cuidadosamente un texto, pero nadie puede comprobar diez mil. Y precisamente ahí es donde fracasan muchos proyectos de IA empresarial.
Hay, sin embargo, algunos sectores que nunca han tenido ese problema, porque integraron la verificación automática en sus procesos hace décadas.
El ejemplo más claro es el diseño de chips. Las herramientas de verificación formal demuestran matemáticamente que un circuito cumple exactamente con las especificaciones para las que fue diseñado. Esa infraestructura ya existía mucho antes de que alguien pensara en aplicar modelos de lenguaje a este ámbito.
El resultado puede verse en los productos que estas compañías ya están desarrollando. Durante la feria Computex, celebrada en mayo, Cadence anunció que había ampliado las capacidades de su agente de diseño hasta alcanzar un funcionamiento totalmente autónomo. El sistema ejecuta cientos de simulaciones utilizando el motor de verificación formal Jasper, reduciendo un proceso de validación que antes requería cinco semanas a menos de un día. Synopsys comercializa una herramienta equivalente, VC Formal, que utiliza análisis estático para demostrar matemáticamente que un diseño es correcto, en lugar de comprobarlo mediante pruebas individuales.
Esta rapidez tiene menos que ver con la confianza en la inteligencia artificial que con una cuestión puramente práctica. Si un diseñador de chips puede verificar la respuesta de la máquina de forma automática, rápida y barata, el coste de detectar un error resulta prácticamente insignificante.
La misma lógica se aplica a cualquier ámbito donde ya exista una obligación de demostrar formalmente la validez de un resultado. Es el caso de la criptografía, el software para sistemas críticos o la verificación de hardware.
Las empresas que controlan esas capas de verificación son precisamente las que más pueden beneficiarse del crecimiento de la IA, porque cuanto mayor es el volumen de resultados generados, más inviable resulta la revisión humana.
En otras palabras, el coste de obtener una respuesta compleja acaba de reducirse prácticamente a cero; el verdadero desafío pasa ahora a ser demostrar que esa respuesta es correcta.
Este artículo ha sido traducido de Forbes.com
