Anthropic lanza una biblioteca de verificación formal a gran escala de Claude

La empresa de inteligencia artificial Anthropic, a través de su equipo Frontier Red Team, publicó el 22 de octubre un estudio que afirma que los modelos de lenguaje grande ahora pueden redactar automáticamente pruebas formales a mayor escala. El equipo colaboró con Theorem para utilizar Claude en la capa de ensamblador RISC-V para probar las propiedades de seguridad de más de 100 bibliotecas de código abierto reales, marcando la primera vez que se realiza una verificación formal a gran escala de software de producción utilizando IA en la capa de ensamblador. Durante el proceso de redacción de pruebas, se descubrieron vulnerabilidades que no habían sido detectadas durante años. El experimento convirtió las pruebas de fuzzing compilables ya existentes en Google OSS-Fuzz en especificaciones, bajo supuestos de binarios estáticos de un solo hilo, presupuesto de memoria fijo, CPU RISC-V y Linux, donde para cualquier entrada menor de 64 MB, el programa debería salir normalmente sin activar errores de seguridad de memoria o fallos de aserción. Después de corregir los problemas, Claude demostró las propiedades mencionadas en 239 puntos de entrada de 123 bibliotecas de OSS-Fuzz, con pruebas dirigidas a instrucciones RISC-V compiladas, aproximadamente 180 millones de líneas de Rocq, verificadas por el núcleo de Rocq. La página indica que esto no significa que estas bibliotecas estén libres de vulnerabilidades, ya que los problemas restantes pueden estar en componentes de confianza o fuera del alcance de la prueba. El equipo también hizo que Claude formalizara el RFC 1950 y demostró en la capa binaria x86 que la implementación de zlib en el núcleo de Linux cumple con esa especificación; se desarrolló un intérprete en Rust que cubre un gran subconjunto de Python, con una proporción del 99.95% de programas generados aleatoriamente que se comportan de manera consistente con CPython. En 36 pequeñas tareas de verificación, Opus 5.5 demostró que se necesitaban aproximadamente un 40% menos de tokens para la mitad de ellas en comparación con Opus 5.