Setecientos problemas y una pregunta (I): lo que se publicó

El 6 de octubre OpenAI subió a GitHub 722 manuscritos de matemática escritos por un modelo interno que el público no puede usar. Los titulares hablaron de “700 problemas resueltos”. La cifra suena a hazaña, pero la letra chica es más interesante que el titular.

Empecemos por los números. Los manuscritos se agrupan en 372 familias de resultados, y una familia puede incluir el teorema principal, pruebas alternativas y consecuencias lógicas. Se intentaron unos 4000 problemas, así que lo publicado cubre menos del diez por ciento, y es la selección de los aciertos que OpenAI consideró significativos. Cualquiera que haya rendido un parcial sabe que mostrar solo los ejercicios que salieron bien es una manera de contar la historia. La mayoría de los resultados costó, en promedio, el equivalente a unas tres horas de ChatGPT Pro. El de Navier-Stokes, en cambio, requirió un enjambre de 10.000 agentes trabajando 88 horas, probablemente por millones de dólares, según estima Science. El precio de la matemática con IA baja rápido, y eso explica que se pueda publicar tanto de una vez.

Después viene la verificación, que es el punto central. Cada manuscrito incluye su demostración escrita, pero solo una parte tiene su resultado principal formalizado en Lean, el lenguaje que permite chequear una demostración con una máquina.

OpenAI habla de 300 de 719, cerca del 42%, aunque otros recuentos dan cifras menores, y apenas diez manuscritos traen un resumen del razonamiento del modelo. Tampoco formalizar es una garantía absoluta: lo que se traduce a Lean puede ser algo más débil que el teorema que anuncia el papel. La propia documentación admite que los resultados sin formalizar podrían tener problemas, y los hubo.

Al día siguiente de la publicación, un error de signo invalidó una construcción de la que dependían otros dos artículos, y los tres fueron retirados. Hoy el catálogo tiene 719 manuscritos. Pero hay otro dato que dice mucho: en el primer registro de cambios, OpenAI corrigió además otros 14, entre reparaciones de pruebas, enunciados ajustados e hipótesis aclaradas. Es decir, entre retiros y correcciones, diecisiete manuscritos necesitaron arreglos casi de inmediato. La empresa dice que encontró los errores en una auditoría propia, y aclaró que retiró las pruebas, no los enunciados, lo cual es cierto, pero limitado: que algo no esté refutado no significa que esté demostrado.

Alex Townsend, profesor asociado de matemática en la Universidad de Cornell, no se sorprendió de que un solo error se propagara a tres manuscritos. Es lo que pasa cuando una demostración se apoya en otra: si falla la base, cae todo lo que está encima. Townsend sospecha que van a aparecer más errores, y opina que OpenAI eligió mal el orden: debió haber anunciado primero los manuscritos verificados con Lean.

La lectura de Andrew Sutherland, investigador principal del departamento de Matemática del MIT, fue de doble filo. Por un lado, celebró la rapidez con que OpenAI retiró los papers y dijo que actuó de manera responsable.

Por otro, advirtió que hará falta mucho más que eso para recuperar la confianza que la empresa perdió, sobre todo por cómo se anunció Navier-Stokes en septiembre. El malestar no depende de si cada prueba resulta correcta. Tiene que ver con el método: un modelo cerrado que nadie puede replicar, cientos de resultados soltados de golpe y una comunidad de matemáticos a la que se le deja el trabajo de revisar, sin que nadie lo haya pedido.

El grupo independiente que asesora a OpenAI sobre cómo publicar estos resultados le pidió que deje de probar problemas abiertos con modelos no liberados, a los que nadie más puede acceder. Hasta ahora la empresa dijo que no, aunque coincide en el espíritu con otras recomendaciones, como depositar los resultados en repositorios independientes y divulgar las instrucciones que dieron origen a cada uno.

Conviene también poner cada titular en su lugar.

Los problemas del milenio son siete desafíos que el Instituto Clay propuso en el año 2000, con un millón de dólares para quien resuelva cada uno. Ese año, el matemático Alain Connes aseguró que eran “totalmente inaccesibles para las computadoras”. En un cuarto de siglo cayó uno solo, la conjetura de Poincaré, por obra del matemático ruso Grigori Perelman.

OpenAI dice haber tocado tres. La hipótesis de Riemann trata de cómo se distribuyen los números primos, cuyo orden esconde una función llamada zeta, y afirma que todos los ceros de esa función, los puntos donde vale cero, están alineados sobre una misma línea. Se comprobó por computadora en más de diez billones de casos, y aun así nadie pudo demostrarla.

Varios medios dijeron que OpenAI la resolvió, y no es así: el modelo demostró una versión más débil, que no hay ceros en una franja junto a uno de los bordes de la región donde se los busca. Pero tampoco es poca cosa. James Maynard, de la Universidad de Oxford y medalla Fields, lo calificó de revolucionario y dijo que es, dentro de su especialidad, el resultado más resonante de los últimos cien años.

Alex Kontorovich, de la Universidad de Rutgers, contó que no creyó que viviría para verlo. Todavía hay que confirmarlo, y hay un detalle que importa: de los cientos de papers, ese fue el único que humanos editaron antes de publicarse. Entre los manuscritos vinculados con Hodge, un problema de geometría abstracta, estaban los tres que se retiraron. Y la solución de Navier-Stokes, las ecuaciones que describen cómo se mueven los fluidos, que OpenAI anunció en septiembre, sigue esperando validación independiente: un preprint reciente señaló que su versión en Lean no coincide con la prueba escrita, algo que no prueba que esté mal, pero que muestra lo difícil que es comprobarla.

Quedan entonces dos cosas: un lote de resultados que todavía nadie puede comprobar y una comunidad de matemáticos que tiene que decidir qué hacer con él. Lo que eso ya les está haciendo, y quién va a leer las pruebas, es el tema de la segunda parte.