Una IA verificó matemáticamente parte del código de Signal en medio día y por 500 dólares, frente a cinco meses de trabajo humano

Chuyue Sun, investigadora de Stanford, y sus colegas han creado una herramienta de IA que completó un proyecto de ingeniería en menos de medio día y por menos de $500: verificó parte del código que cifra las conversaciones en el mensajero Signal. Tres especialistas altamente cualificados habían tardado cinco meses en hacer el mismo trabajo a mano. La verificación no fue convencional, sino formal: en lugar de ejecutar el programa en miles de pruebas, se demuestra matemáticamente que se comporta como se diseñó. La idea no es nueva, pero hasta ahora resultaba demasiado cara y lenta. Hoy apuestan por ella startups con cientos de millones de dólares y grandes laboratorios de IA.

Por qué matemáticas en lugar de pruebas

Las pruebas convencionales muestran que el programa no falló en los casos que se le plantearon. La verificación formal demuestra que no fallará en ningún caso de la clase descrita. Los ingenieros redactan enunciados precisos sobre el objetivo del programa y después traducen el código a fórmulas que comprueban sistemas especializados, como Lean, Rocq e Isabelle.

Pero el trabajo es pesado. Las especificaciones hay que formularlas con mucho cuidado. Un ejemplo sencillo: una función que ordena una tabla debe devolver los mismos elementos que recibió, solo que en otro orden. Para una persona es obvio; para un sistema matemático hay que escribirlo con todo rigor.

Por eso el método se aplica donde el coste de un error es alto. Según las propias compañías, hay código verificado formalmente en aviones de Boeing, en servidores de Amazon y en más de 2,5 mil millones de dispositivos activos de Apple. Suele ser código relacionado con la seguridad. Byron Cook, de Amazon Web Services, afirma que la verificación resolvía las dudas de los clientes sobre la protección de la nube y aceleraba a los equipos internos: los errores graves se detectaban pronto.

Quién apuesta por la IA y cómo

Las startups quieren automatizar la parte más tediosa: redactar la descripción de cómo debe comportarse el programa. Los pasos restantes, posiblemente sin IA, traducen el código al formato que entienden los sistemas matemáticos.

• &Truth. Ha captado $70 millones. Sun se incorporó en agosto y el lanzamiento público tuvo lugar el jueves.

Su objetivo es verificar con el tiempo código en cualquier lenguaje de programación. El director científico, Ilya Sergey, compara el enfoque con la construcción: los puentes y los edificios no se derrumban porque se calculan antes de levantarlos, así que por qué no hacer lo mismo con el código. • **Harmonic.

** Cofundada por Vlad Tenev, director de Robinhood, ha captado $295 millones. Esta semana anunció que su agente de IA matemática Aristotle sabe verificar programas en C y descripciones de microchips en Verilog. La tecnología la evalúan clientes potenciales, entre ellos los fabricantes de chips Tensordyne y Nvidia; el brazo de capital riesgo de Nvidia es uno de los inversores.

• Anthropic y Theorem. Hace una semana informaron de que, con ayuda de IA, encontraron errores en software de código abierto que no habían detectado billones de pruebas. También lanzaron un complemento para Claude que ayuda a los desarrolladores con la verificación.

No revelaron el coste del primer proyecto. • Truidic. Fundada por Madan Musuvathi, que dejó Microsoft Research tras más de 20 años.

En su opinión, la IA en manos de los atacantes es muy potente, y la verificación puede hacer que la IA sea segura. • Proofcraft. Lleva tiempo dedicada a la verificación clásica.

Sus responsables, June Andronick y Gerwin Klein, afirman que el flujo de solicitudes supera la capacidad tanto de ellos como de sus competidores.

Los proyectos abiertos también prueban el método. La organización sin ánimo de lucro Beneficial AI Foundation verificó este año, con una subvención de Anthropic, el mismo código de cifrado que Sun. Michael Rosenberg, uno de los mantenedores de la biblioteca curve25519-dalek, espera que estos trabajos tengan financiación permanente, pero no sabe de dónde saldrá y no quiere depender de la buena voluntad de las empresas de IA.

Dónde choca el método con su techo

Por ahora la tecnología está en fase de prototipos. No está claro cuánto están dispuestos a pagar los clientes ni en qué forma querrán recibir el producto: directamente o a través de intermediarios como Anthropic. Varias empresas tecnológicas medianas contaron a Wired que habían verificado como máximo una función clave de su producto, o ninguna. Los motivos: falta de ingenieros de verificación, un coste superior al riesgo potencial y el temor a que semanas de espera por la verificación frenen el lanzamiento de actualizaciones. Incluso Apple se ve obligada a añadir con cautela código nuevo a su biblioteca de cifrado corecrypto para poder verificarlo a tiempo.

También hay objeciones de principio. La demostración se apoya en supuestos sobre cómo interactúan con el programa los ordenadores y las personas. Puede que no detecte errores de usuario ni fallos de hardware.

Will Wilson, director de la startup Antithesis (búsqueda de bugs con IA), llama a la verificación formal una «trampa» para aficionados a las matemáticas como él. Su empresa gastó millones en verificar parte de su protección y calificó el proceso de «un dolor en el trasero». Aun así, su propia herramienta encontró errores adicionales en ese código, además de bugs en software de clientes que ya lo habían verificado formalmente.

La conclusión de Wilson: la verificación aporta cierta confianza, pero solo las pruebas exhaustivas pueden confirmarla. Vitalik Buterin también escribió en su blog que la verificación formal no es una panacea, aunque la considera una defensa importante frente a los ciberataques con IA.

Andronick y Klein ven un riesgo adicional: si la descripción del problema la escribió una IA, surge una «confianza injustificada» en el resultado. La demostración es correcta solo en la medida en que lo sea la descripción de qué se considera correcto.

La conclusión práctica para los ingenieros: la IA reduce drásticamente el coste de la etapa más cara, pero habrá que revisar tanto las propias especificaciones como el trabajo con pruebas. Dos empresas en las que el código no se verifica formalmente estarían dispuestas a pagar a los laboratorios de IA por código «verificado» generado por IA. Si funciona, la verificación formal saldrá del ámbito de la NASA y Apple.