¿Hipótesis del tiempo exponencial refutada por un modelo de OpenAI?

El 26 de octubre, OpenAI publicó en el repositorio openai/math el artículo “The Exponential Time Hypothesis is False”. Según el texto, un modelo interno de OpenAI no revelado ha refutado la hipótesis del tiempo exponencial (ETH), uno de los supuestos básicos de la teoría de la complejidad computacional. Un grupo independiente de informáticos, entre ellos dos coautores de la propia hipótesis, está examinando el artículo junto con su formalización en Lean.

¿Qué es la hipótesis del tiempo exponencial?

La ETH (Exponential Time Hypothesis) supone que el problema 3-SAT, es decir, comprobar si se puede satisfacer una fórmula lógica con cláusulas de tres variables, no puede decidirse más rápido que en tiempo 2^Ω(n) para n variables. Dicho de forma sencilla: con cada variable adicional el tiempo crece exponencialmente y ningún algoritmo ingenioso lo cambiará.

La hipótesis la formularon Russell Impagliazzo y Ramamohan Paturi (con Francis Zane). En la ETH se apoyan cientos de trabajos que demuestran que algún problema de grafos, bases de datos o biología computacional “no puede” resolverse más rápido (como recuerda The Next Web).

¿Qué demostró exactamente el modelo de OpenAI?

El artículo presenta un algoritmo determinista que cuenta exactamente todas las asignaciones que satisfacen una fórmula k-CNF para cualquier k ≥ 2 fijo. Funciona con memoria polinómica y en tiempo (n + m)^O(1) · 2^(n/(log n)^(1/2+o(1))), es decir, subexponencial. El caso de 3-SAT basta para refutar la ETH.

Curiosamente, el algoritmo no solo responde “sí” o “no”, sino que cuenta las soluciones. De ello el artículo deriva otras consecuencias:

1. algoritmos subexponenciales para contar coloraciones de grafos, conjuntos independientes y emparejamientos perfectos,
2. aproximaciones arbitrariamente precisas para Max-k-SAT en tiempo subexponencial,
3. una nueva cota inferior del tamaño de los circuitos lógicos para la clase E^NP.

Según The Next Web, el modelo encontró la prueba el 16 de octubre y un día después ya estaba verificada en Lean (un lenguaje formal para que un ordenador compruebe demostraciones). En el historial de cambios del repositorio, OpenAI indica que el artículo se publicó con la formalización en Lean.

¿Quién está revisando la prueba?

El grupo que debe examinar y explicar la prueba lo dirigen Russell Impagliazzo, Ramamohan Paturi (UC San Diego) y Ryan Williams (MIT). Según el historial del repositorio, fue precisamente a petición de este grupo que los materiales se publicaron de inmediato, para que todo el mundo pudiera revisarlos. Williams escribió en X que un modelo interno de OpenAI había producido una “claimed refutation of ETH”, es decir, una refutación declarada de la ETH.

Los investigadores no han firmado ningún NDA ni cobran por ello (según The Next Web). Pidieron a OpenAI que hiciera públicos todos los datos en bruto y financiara una conferencia sobre las consecuencias del resultado, y la empresa aceptó. Aun así, en una carta abierta advierten que su participación no confirma el resultado (“should not be taken as certification of the claim”), y añaden que, si la prueba es correcta, “it will change an important part of theoretical computer science”.

¿Es algo nuevo en el mundo de la IA?

No es la primera publicación de este tipo de OpenAI. Como sabemos, el 6 de octubre la empresa subió al mismo repositorio más de 700 artículos matemáticos generados por el modelo. En el README del repositorio leemos que el modelo recibió unos 4000 problemas abiertos, y cada resultado supuso de media tres horas de “pensamiento” a nivel de ChatGPT Pro.

Lo nuevo es que el 26 de octubre OpenAI anunció tres resultados a la vez y eligió un camino distinto para cada uno (lo describe Unite.AI):

1. ETH: el artículo y la prueba en Lean son públicos, y los revisa un grupo abierto de Impagliazzo, Paturi y Williams.
2. La conjetura de Sogge sobre el “local smoothing” en todas las dimensiones, de la que según OpenAI se siguen la conjetura de Kakeya y la conjetura de restricción de Stein: también publicada con prueba en Lean.
3. La existencia de la teoría de Yang-Mills y la QCD en cuatro dimensiones (uno de los Problemas del Milenio del Instituto Clay): aquí de momento no hay materiales. Un grupo dirigido por el premio Nobel David Gross decidió redactar el resultado por su cuenta.

OpenAI declara además que no quiere el mérito científico de los descubrimientos de sus modelos. El reconocimiento debe ser para las personas que los entiendan y los describan. La empresa también donó 5 millones de USD a la Fundación Simons para talleres y conferencias sobre resultados generados por IA.

¿En qué debemos fijarnos?

Primero, en el estado de la verificación. Una formalización en Lean es una señal fuerte, pero siempre hay que comprobar si el teorema escrito en Lean dice realmente lo mismo que el texto del artículo. La propia OpenAI escribe en el README que algunos resultados sin formalizar pueden contener errores, y el 7 de octubre retiró tres artículos por un error de signo en una de las pruebas. Así que tomemos el resultado con cautela hasta que el grupo termine su trabajo.

Segundo, en lo que el resultado no significa. Los autores escriben claramente que de él no se deduce que todos los problemas NP tengan algoritmos subexponenciales. Por tanto, no resuelve el problema P vs NP, y el tiempo de ejecución sigue creciendo más rápido que cualquier polinomio.

Tercero, en el ritmo. Un resultado en el que los teóricos llevaban trabajando más de 20 años lo habría encontrado el modelo durante una evaluación interna. Si se confirma, será probablemente el ejemplo más sólido hasta ahora de una IA haciendo descubrimientos propios en informática teórica. De paso vuelve el tema de las demostraciones formales, del que escribí a propósito de la verificación formal con Claude.

FAQ

¿Qué es la hipótesis del tiempo exponencial?

Es el supuesto de la teoría de la complejidad según el cual 3-SAT no puede resolverse en menos de 2^Ω(n) para n variables. La formularon Impagliazzo y Paturi con Francis Zane.

¿Ha resuelto OpenAI el problema P vs NP?

No. El algoritmo es subexponencial, pero no polinómico, y los autores señalan que el resultado no se traslada a todos los problemas NP.

¿Está ya confirmada la refutación de la ETH?

Todavía no. Existe una formalización en Lean, pero el grupo independiente de Impagliazzo, Paturi y Williams apenas la está examinando y advierte que su participación no implica confirmación.

¿Qué modelo de OpenAI lo hizo?

Un modelo interno no revelado. En el README del repositorio OpenAI no da su nombre.