Una IA ‘desmiente’ un enigma matemático de 90 años: el verificador falló primero

A finales de julio, una IA anunció: el problema de Collatz, que ha tenido en jaque a los matemáticos durante casi 90 años, ha sido refutado por mí, y aquí está el contraejemplo. La evidencia era una “prueba automática” verificable línea por línea por ordenador, impecable a primera vista. Sin embargo, antes de que el mundo pudiera celebrar, llegó la realidad: ese “contraejemplo” era una alucinación producto de un fallo de corrección (soundness bug) en la propia herramienta de verificación. Irónico, dado que la razón de ser de dicha herramienta es precisamente eliminar las alucinaciones de la IA.

Esta historia merece ser contada con detalle desde el principio. Afecta a una pregunta por la que todos estamos apostando: ¿cuánta confianza debemos depositar en lo que dice una IA?

Entender el problema de hace 90 años

Las reglas de la conjetura de Collatz son tan sencillas que cualquier niño de primaria las entiende: piensa un número entero positivo cualquiera. Si es par, divídelo entre 2; si es impar, multiplícalo por 3 y súmale 1. A continuación, repite la misma operación con el resultado.

Por ejemplo, empecemos con el 6. Como 6 es par, al dividir entre 2 obtenemos 3. 3 es impar, por lo que multiplicamos por 3 y sumamos 1, obteniendo 10. 10 es par, dividido entre 2 da 5. 5 es impar, resulta en 16. Y de ahí pasamos por 16 -> 8 -> 4 -> 2 -> 1. ¿Qué ocurre al llegar al 1? Como el 1 es impar, 1 * 3 + 1 nos devuelve al 4, entrando en un bucle infinito 4-2-1. La pregunta es simple: ¿independientemente del número del que se parta, se acaba siempre en el bucle 4-2-1?

Propuesto por el matemático alemán Lothar Collatz en 1937, nadie ha podido demostrarlo ni encontrar un solo contraejemplo. Los ordenadores han probado todos los números hasta (2^{68}) (más de 295 trillones), y absolutamente todos regresaron al 1. Pero los matemáticos no se dejan impresionar: comprobar billones de números no es una demostración, del mismo modo que observar millones de cisnes blancos no prueba que todos los cisnes sean blancos. El gran matemático húngaro Paul Erdős dejó una frase célebre: “Puede que la matemática aún no esté preparada para este tipo de problemas.” La dificultad estriba en su engañosa simplicidad: reglas sencillas, pero resbaladizas como una anguila.

Imagen: Árbol numérico de la conjetura de Collatz: todos los números que llegan al 1 en menos de 20 pasos cuelgan de este árbol. Fuente: Wikipedia (All Collatz sequences of a length inferior to 20)

Cómo se gestó el “avance” de la IA

El 25 de julio, el informático Raman Kumar publicó un repositorio de código que contenía una supuesta “refutación”: un número gigante concreto del cual se afirmaba que nunca regresaba al 1, echando por tierra la conjetura. El gran atractivo era que esta refutación constituía una prueba verificable por máquina generada con asistencia de IA.

Para entender esto, hay que explicar un concepto técnico fundamental. En los últimos años se ha puesto de moda en la matemática escribir las demostraciones como código en un lenguaje de programación especializado y enviarlas a un “compilador de pruebas” llamado Lean. Lean actúa como el examinador más inflexible: descompone cada paso de la prueba y lo verifica línea por línea. Si se salta algún paso lógico, muestra inmediatamente una bandera roja y lo rechaza. Una prueba aprobada por Lean es teóricamente imposible que contenga errores; este es precisamente su objetivo de diseño: sustituir las descuidos y sesgos del arbitraje humano por el rigor imparcial de la máquina.

La trascendencia de esta herramienta es enorme: kernels de seguridad de sistemas operativos, protocolos de criptomonedas y miles de teoremas matemáticos se apoyan en esta “verificación por máquina”. En la industria se ha llegado a promocionar como la solución definitiva para “acabar con las alucinaciones de la IA”: no importa que la IA delire, siempre que la máquina actúe de filtro final.

Por eso, cuando Kumar presentó un “contraejemplo verificado por Lean”, la reacción inicial de los expertos fue de asombro: si la prueba había pasado la revisión de la máquina, el enigma de 90 años se había derrumbado. La noticia se propagó a gran velocidad por las redes sociales bajo titulares llamativos: “Una IA derriba un problema matemático de 90 años”.

La verdad: el examinador cometió un error

El giro dramático no tardó en llegar. El 28 de julio, otro investigador redujo el contraejemplo a una contradicción lógica mínima y abrió una incidencia en el rastreador oficial de Lean, con el número #14576. El título de la incidencia era frío y categórico: “kernel accepts ill-typed projection, allowing proof of false without premises.” (el núcleo acepta proyecciones con tipos erróneos, lo que permite demostrar proposiciones falsas sin premisas).

En lenguaje llano: el examinador supuestamente infalible había omitido un paso en su rutina de comprobación principal. Al examinar tipos de datos anidados, no verificó en un punto si los nombres de los tipos coincidían. Como resultado, una pieza defectuosa escondida en la “demostración” generada por la IA logró colarse por esa grieta. En el momento en que la máquina declaró “verificación superada”, en realidad estaba sellando una alucinación.

Imagen: Órbitas de números pequeños según las reglas de Collatz, confluyendo en el 1. Fuente: Wikipedia (Collatz graph, skipping 27)

A continuación se produjo la escena más dramática. La comunidad de Lean ha contado desde hace tiempo con un diseño de “doble seguro”: además del verificador del núcleo oficial, existe un verificador independiente desarrollado por terceros (escrito en otro lenguaje y por otro equipo) encargado de revisar de forma cruzada los resultados del núcleo oficial. Esta hipótesis de independencia es el fusible en la cadena de confianza de la “verificación por máquina”.

Esta vez el fusible falló. El análisis posterior confirmó que se tuvieron que dar dos errores independientes de forma simultánea: el núcleo oficial omitió la comprobación de tipos anidados, mientras que el verificador independiente pasó por alto un detalle en la comprobación de proyecciones. Dos errores ocultos en rincones de dos códigos distintos se activaron con la misma “prueba”. Casualmente, el fallo del verificador independiente había sido corregido apenas una semana antes, pero la versión empleada por la IA era anterior a dicha corrección. El creador de Lean, Leo de Moura, señaló con franqueza en su análisis que, si bien el autor consideraba que la sincronía era casual, no se podía descartar que la IA hubiera visto el reporte de error en sus datos de entrenamiento.

¿Cómo evaluar esto desde la ingeniería? Que dos implementaciones independientes sean atravesadas por la misma bala tiene una probabilidad astronómicamente baja. Esto implica o bien una mala suerte extrema, o bien que la “refutación” fue elaborada específicamente para explotar esa vulnerabilidad. El propio De Moura ofreció su dictamen: “Este tipo de sucesos seguirá ocurriendo. Las IA son extremadamente hábiles explotando fallos de corrección en los núcleos.” La corrección del error se publicó apenas una hora después de notificarse, lo que demuestra que la arquitectura del núcleo es sólida; pero su hallazgo fue propiciado por un supuesto “gran avance de la IA”.

¿Quién verifica al verificador?

Las repercusiones de este incidente son aún más profundas que el hecho en sí. Tras descubrirse el fallo, OpenAI envió a un investigador de IA especializado en ciberseguridad para auditar el núcleo de Lean, encontrando y corrigiendo varios errores de programación adicionales. En otras palabras: la herramienta concebida para protegernos de la IA ahora depende de la IA para encontrar sus propios fallos.

Mientras tanto, el proyecto “Lean en Lean” (que busca escribir y verificar el propio verificador dentro de Lean) aún no cubre la sección de código afectada, y la porción de código adaptada albergaba el mismo error. La verificación funciona por capas: los resultados de la IA los supervisa el verificador, al verificador lo supervisa una segunda implementación independiente, pero ¿quién supervisa a la segunda implementación? Cada capa añade una fase y un coste extra, pero nunca existe una “última capa”. Esto coincide con la realidad técnica: “verificado por máquina” es siempre una propiedad probabilística; a mayor profundidad e independencia en las comprobaciones, menor es la probabilidad de error, pero nunca será cero.

Para el público general, el gran valor de este caso es calibrar las expectativas. La próxima vez que lea titulares como “Una IA resuelve un enigma de un siglo” o “Una IA demuestra un teorema”, hágase una pregunta más: ¿quién lo ha verificado, un humano o una máquina? Y si fue una máquina, ¿ha sido verificada la propia máquina? Por otra parte, no hay razón para caer en un escepticismo nihilista. La matemática misma ha salido indemne; la conjetura de Collatz sigue intacta. El fallo fue expuesto, corregido y documentado en un análisis ejemplar. El sistema tuvo un error, pero la forma en que lo procesó y rectificó es precisamente la razón por la que merece nuestra confianza.

La confianza es una cadena en la que cualquier eslabón puede romperse en cualquier momento. La gente inteligente no finge que la cadena es irrompible; simplemente se acuerda de revisar cada eslabón con frecuencia. Esta vez, la IA nos enseñó una grieta en uno de esos eslabones… bajo la forma de un falso avance.

Enlaces de referencia:

• Postórtem de Leo de Moura: Análisis completo del error de corrección del núcleo #14576
• Discusión en Lobsters (ojcl8j): Debate de la comunidad sobre el error del núcleo (48 puntos)
• Wikipedia: Conjetura de Collatz (Reglas, historia y avances de verificación)