Claude de Anthropic ahora escribe código y demuestra su seguridad automáticamente
decoder ·
Anthropic se ha asociado con Theorem para demostrar que su modelo de IA, Claude, puede generar automáticamente pruebas matemáticas que verifican la corrección del código de software existente. En un proyecto reciente, Claude produjo aproximadamente 180 millones de líneas de código de prueba para 123 bibliotecas de código abierto del proyecto OSS-Fuzz de Google en apenas unas pocas semanas. Este proceso autónomo implicó traducir pruebas de fallos a problemas matemáticos y analizar el código máquina compilado, con una herramienta independiente llamada Rocq que verificaba los resultados. Durante esta fase de verificación, Claude identificó cientos de errores que los métodos de prueba convencionales habían pasado por alto durante años, incluidas vulnerabilidades de seguridad críticas en lectores de PDF ampliamente utilizados. Sin embargo, estas pruebas formales están sujetas a estrictas limitaciones, aplicándose solo a arquitecturas de procesadores específicas, programas de un solo hilo e entradas inferiores a 64 MB. Aunque el costo computacional sigue siendo elevado, Anthropic señala que los modelos más recientes son cada vez más eficientes, requiriendo menos tokens para resolver pruebas similares. La empresa tiene como objetivo convertir la verificación formal impulsada por IA en algo tan rutinario como las pruebas estándar de software, lo que podría transformar la forma en que los desarrolladores confían y revisan el código generado por IA.
decoder