Anthropic, junto con su socio Theorem, llevó a cabo un proyecto para demostrar matemáticamente que el código de software existente funciona correctamente mediante el modelo de IA «Claude». El trabajo abarcó 123 bibliotecas de código abierto incluidas en el proyecto de seguridad de Google «OSS-Fuzz». En unas semanas se generaron alrededor de 180 millones de líneas de código de demostración y, según se informa, se descubrieron también cientos de errores que habían pasado inadvertidos en las pruebas convencionales.
La distancia entre «ha superado las pruebas» y «se ha demostrado que es correcto»
Cuando se habla de comprobar la calidad del software, a muchas personas les vienen a la cabeza las pruebas: se proporcionan entradas preparadas y se comprueba si se obtiene el resultado esperado. Sin embargo, las pruebas solo permiten verificar lo que se ha probado. No indican cómo se comportará el programa en situaciones que no se hayan probado.
Ahí es donde entra en juego la verificación formal. Consiste en tratar el comportamiento de un programa como un problema matemático y demostrar que funciona correctamente dentro de unas condiciones definidas. En teoría es un método muy potente, pero requería un esfuerzo descomunal. Se calcula que un equipo de especialistas dedicó el equivalente a 20 años-persona a verificar seL4, un pequeño núcleo de sistema operativo. No es de extrañar que su uso se haya limitado a casos extremos, como el software de control de aviones de pasajeros.
En esta ocasión, Frontier Red Team, de Anthropic, se asoció con Theorem y encargó a Claude este trabajo de demostración. No le pidieron que escribiera código nuevo. En su lugar, le encomendaron analizar software ya existente, convertir las pruebas que buscan fallos de ejecución en problemas matemáticos y examinar incluso el código máquina resultante de la compilación para construir un gran número de demostraciones.
Otro programa se encarga de «calificar» las demostraciones
Que una IA declare «aprobada» una demostración que ella misma ha escrito no resulta convincente. Lo interesante en este caso es el sistema de evaluación: un programa de verificación independiente llamado Rocq comprueba automáticamente las demostraciones generadas. Según Anthropic, el proceso apenas requiere revisores humanos.
El equipo de investigación lo denomina generación de demostraciones «totalmente autónoma». Sin embargo, las herramientas empleadas y las bases formales fueron creadas por personas de Theorem. Más que decir que la IA lo generó todo desde cero, probablemente sea más fiel a la realidad afirmar que escribió de golpe una cantidad ingente de demostraciones sobre un terreno preparado por seres humanos.
Cientos de errores descubiertos durante el proceso de demostración
Durante el proceso, Claude se topó con cientos de errores y también se le permitió corregirlos por sí mismo. Según los investigadores, muchos solo afloran en condiciones muy concretas, como archivos de entrada extremadamente grandes o determinados órdenes de acceso a la memoria. No es de extrañar que las pruebas habituales no los detectaran.
También se han citado ejemplos concretos. Al verificar un lector de PDF muy utilizado, en una semana se encontró el mismo número de errores de seguridad que suele notificarse en ese software a lo largo de un año. En otra aplicación, se descubrió un error lógico que había pasado inadvertido durante más de diez años.
Otro aspecto que no conviene pasar por alto es qué ocurre cuando una demostración no llega a completarse. Anthropic explica que, aunque la demostración falle, durante el intento pueden salir a la luz errores reales. Así, las demostraciones no sirven solo para obtener un «certificado de aprobado», sino que también actúan como una sonda para sacar a la luz errores. Parece más probable que complementen las pruebas convencionales, en lugar de sustituirlas.
No hay que malinterpretar el alcance de «verificado formalmente»
Aun así, es peligroso interpretar «verificado formalmente» como «sin errores». La propia Anthropic reconoce que las demostraciones solo son válidas dentro de unas condiciones estrictas. Se presupone una configuración concreta del procesador, programas que se ejecutan en un solo hilo y entradas de menos de 64 MB. En el mundo real, las bibliotecas funcionan con distintos tipos de hardware y configuraciones.
El coste tampoco es desdeñable. Se calcula que, en algunos casos, cada demostración consume cientos de millones de tokens. No se ha hecho público el coste total del proyecto. Por otra parte, pequeños experimentos adicionales han demostrado que las demostraciones se pueden reutilizar y apuntan a que los modelos más nuevos son cada vez más eficientes. Según se informa, Opus 5.5 necesita alrededor de un 40 % menos de tokens que Opus 5 para resolver la mitad de las demostraciones.
La pregunta deja de ser «¿puede escribir programas?»
Si la IA puede escribir código y garantizar su corrección bajo ciertas condiciones, cambia la forma de plantear la cuestión. Ya no se trata de «¿puede programar la IA?», sino de «¿puede demostrar la IA que el código que ha escrito es seguro?». Para los equipos de desarrollo que desconfían de la fiabilidad del código generado por IA, este cambio no es menor. Si la IA puede verificar su propio código, también podría reducir la carga de las revisiones humanas y recortar los costes no solo de la verificación, sino de todo el proceso de desarrollo.
Anthropic prevé que, en un futuro próximo, la verificación formal mediante IA se convierta en una práctica tan habitual como las pruebas convencionales. La hoja de ruta de Theorem incluye entre sus objetivos software de infraestructuras críticas como glibc, OpenSSL y cURL.
Lo importante aquí no es tanto leer el «contenido» de la demostración como sus «premisas». ¿En qué entorno se ha planteado y qué entradas presupone? En una era en la que también confiamos a la IA la tarea de verificar, la capacidad humana para comprobar esas premisas parece ser la última línea de defensa de la seguridad.
コメント