Una herramienta de IA de Stanford verifica parte del código de Signal en medio día y por menos de 500 dólares, frente a cinco meses

La verificación formal, es decir, la demostración matemática de que un programa hace exactamente lo que se le exige, ha sido durante décadas terreno de entusiastas y de los sistemas más críticos. Ahora la IA generativa intenta convertirla en una herramienta corriente. La investigadora de Stanford Chuyue Sun y sus colegas mostraron en un artículo reciente que su herramienta de IA completó un proyecto de ingeniería en menos de medio día y por menos de 500 dólares. Tres expertos altamente cualificados habían dedicado cinco meses al mismo trabajo. El proyecto abarcaba una parte del código que cifra las conversaciones en el mensajero Signal.

Por qué las matemáticas se han abaratado de golpe

La verificación clásica es difícil por dos razones. Los ingenieros deben escribir con precisión qué esperan del programa y luego traducir el código a fórmulas que puedan comprobarse. Las empresas ya ejecutan pruebas complejas, pero rara vez gastan en verificación formal, aunque detecta fallos más extraños.

Las nuevas startups apuestan por automatizar el primer paso. La IA debe redactar las especificaciones: por ejemplo, para ordenar una tabla exigen que el conjunto de elementos sea el mismo antes y después, y que solo cambie el orden. La traducción posterior del código al formato de los sistemas de demostración Lean, Rocq e Isabelle puede hacerse sin IA.

Sun se incorporó en agosto a &Truth, que se lanzó públicamente el jueves. La startup captó 70 millones de dólares y quiere verificar con el tiempo código en cualquier lenguaje. El director científico de &Truth, Ilya Sergey, lo compara con la construcción: los puentes y los edificios no se derrumban porque se calculan de antemano; la tecnología para razonar así sobre el código existía, pero escalaba mal.

Quién más compite en este mercado

La competidora Harmonic, cofundada por el jefe de Robinhood, Vlad Tenev, ha recibido 295 millones de dólares. Esta semana anunció que su agente de IA para matemáticas, Aristotle, puede verificar software en C y descripciones de hardware en Verilog. Evalúan la tecnología clientes potenciales, entre ellos el fabricante de chips Tensordyne y Nvidia, cuyo fondo de capital riesgo figura entre los inversores de Harmonic.

Una semana antes, Anthropic y la startup Theorem informaron de que habían usado IA para encontrar en software de código abierto errores que se les habían escapado a 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. Madan Musuvathi, que dejó Microsoft Research tras más de 20 años, fundó Truidic: según él, la IA es muy potente en manos de los atacantes, y la verificación puede hacer seguros los sistemas de IA.

La Beneficial AI Foundation verificó este año, con una subvención de Anthropic, el mismo código criptográfico que Sun. Michael Rosenberg, mantenedor de la biblioteca curve25519-dalek, espera una financiación sostenible, pero no sabe de dónde saldrá y considera un error depender de la buena voluntad de las empresas de IA.

Dónde están el escepticismo y los límites

La verificación ya está en los aviones de Boeing, los servidores de Amazon y más de 2.500 millones de dispositivos activos de Apple, pero suele aplicarse a código relacionado con la seguridad. Byron Cook, de AWS, dice que el método disipó parte de las dudas de los clientes de la nube y aceleró a los equipos internos.

En cambio, varias empresas medianas contaron a WIRED que habían verificado como máximo una función clave. Los motivos: falta de especialistas, un coste superior a los riesgos posibles y el temor a que semanas de espera frenen el lanzamiento del producto. Dos directivos de ciberseguridad de grandes empresas que no han verificado código formalmente no están seguros de que la automatización cambie el cálculo, pero están dispuestos a pagar a los grandes laboratorios de IA por código generado «verificado».

La tecnología sigue en fase de prototipo. No está claro cuánto están dispuestos a pagar los clientes ni cómo quieren adoptarla: directamente o mediante intermediarios como Anthropic. El método se apoya en supuestos sobre cómo interactúan los ordenadores y las personas con el software, por lo que parte de los expertos duda de que detecte errores de usuario y fallos de hardware.

Will Wilson, jefe de la startup Antithesis, que busca errores con IA, llama a la verificación formal una «trampa» para matemáticos como él. La empresa gastó millones de dólares en verificar parte de sus defensas, calificó el proceso de doloroso y aun así encontró errores adicionales con su propia herramienta. Antithesis también ha detectado errores en software de clientes que ya lo habían verificado. Según él, la verificación formal da cierta confianza, pero solo las pruebas exhaustivas pueden confirmarla. Vitalik Buterin también escribió en su blog que no es una panacea.

Otra salvedad afecta a las propias especificaciones. Los fundadores de Proofcraft, June Andronick y Gerwin Klein, dicen que el interés supera su capacidad y la de sus competidores, pero temen una «confianza injustificada» en los resultados con especificaciones hechas por IA. La conclusión práctica para los equipos: la IA abarata la verificación lo bastante como para probarla en módulos críticos como la criptografía, pero no promete sustituir a las pruebas.