Puntos clave
- Anthropic y su socio Theorem usaron Claude para verificar matemáticamente código de software existente y generar demostraciones formales de su corrección.
- El modelo produjo aproximadamente 180 millones de líneas de código de demostración para 123 bibliotecas de código abierto en solo unas pocas semanas. En el camino, Claude detectó cientos de errores que las pruebas convencionales habían pasado por alto.
- Si la IA puede escribir código y demostrar que es correcto, la automatización del software podría dar un gran salto. Anthropic quiere que la verificación formal con IA se vuelva tan rutinaria como las pruebas estándar.
Anthropic usó Claude para demostrar matemáticamente que el código existente es correcto. El enfoque aborda un problema central del software generado por IA, pero conlleva estrictos límites prácticos.
Demostrar que un software funciona sin errores en todas las circunstancias siempre ha sido prohibitivamente caro. Un equipo de especialistas necesitó 20 años-persona solo para verificar formalmente el pequeño núcleo de sistema operativo seL4, por lo que el método estaba reservado para casos extremos como el software de aviónica de Airbus.
El Frontier Red Teamde Anthropic, trabajando con su socio Theorem, dejó que Claude se encargara del trabajo de demostración. El modelo produjo aproximadamente 180 millones de líneas de código de demostración matemática en solo unas pocas semanas, basándose en programas de prueba de 123 bibliotecas de código abierto del proyecto de seguridad OSS-Fuzz de Google.
En lugar de escribir código nuevo, Claude verificó software existente traduciendo pruebas de fallos a problemas matemáticos, analizando el código máquina compilado y produciendo demostraciones extensas. Un programa de verificación independiente llamado Rocq comprueba automáticamente esas demostraciones y, según Anthropic, el proceso casi no necesita revisores humanos. Los investigadores lo llaman generación de demostraciones "totalmente autónoma", aunque las herramientas y los fundamentos formales fueron construidos por humanos en Theorem.Ad
Claude detecta errores que años de pruebas pasaron por alto
Mientras generaba demostraciones, Claude se topó con cientos de errores y se le permitió corregirlos él mismo. Muchos habrían escapado a las pruebas convencionales porque solo aparecen en condiciones muy específicas, como archivos de entrada inusualmente grandes o una secuencia particular de accesos, según los investigadores.
Durante un esfuerzo por verificar un lector de PDF muy utilizado, por ejemplo, el equipo encontró tantos errores de seguridad en una semana como los que normalmente se reportan para ese software en un año entero. En otra aplicación, Claude detectó un error lógico que había pasado inadvertido durante más de una década. Incluso cuando una demostración completa finalmente falla, dice Anthropic, el intento sigue revelando errores reales.
Lo que la verificación formal puede y no puede hacer
Anthropic reconoce que "verificado formalmente" no significa "libre de errores". Las demostraciones solo son válidas bajo condiciones estrictas: una arquitectura de procesador específica, programas de un solo hilo y entradas de menos de 64 MB. En la práctica, estas bibliotecas se ejecutan en hardware diferente y en configuraciones distintas.
El coste de cómputo es elevado, con demostraciones individuales que consumen cientos de millones de tokens. Anthropic no informa del coste total del proyecto. Pero si la IA puede verificar su propio código, los desarrolladores pueden confiar más en el software generado por IA y dedicar menos tiempo a revisarlo. Eso ahorra costes no solo en la verificación, sino en todo el proceso de programación. Una prueba más pequeña también mostró que las demostraciones son reutilizables, y los modelos más nuevos son cada vez más eficientes: Opus 5.5 resuelve la mitad de las demostraciones con aproximadamente un 40 por ciento menos de tokens que Opus 5.Ad
El proyecto refuerza el argumento a favor de la automatización del software. Si la IA puede escribir código y garantizar su corrección bajo condiciones definidas, la pregunta cambia de "¿Puede programar la IA?" a "¿Puede la IA demostrar que el código que escribe es seguro?" Si la respuesta es sí, las consecuencias podrían ir mucho más allá de las herramientas de programación actuales.
Un ejemplo claro: Anthropic espera que la verificación formal con IA pronto se vuelva tan práctica como las pruebas estándar, y La hoja de ruta de Theorem ya apunta a infraestructura crítica como glibc, OpenSSL y cURL.
Fuente: Anthropic