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

La empresa de inteligencia artificial Anthropic, a través de su Frontier Red Team, publicó el 22 de octubre un estudio que afirma que los modelos de lenguaje grandes 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 propiedades de seguridad en 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 fuzz ya compilables 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, probando aproximadamente 180 millones de líneas de Rocq, que fueron verificadas por el núcleo de Rocq. La página aclara que esto no significa que estas bibliotecas no tengan vulnerabilidades, ya que los problemas restantes pueden estar fuera del alcance de los componentes de confianza o de la prueba. El equipo también hizo que Claude formalizara el RFC 1950 y probó en la capa de binario x86 que la implementación de zlib en el núcleo de Linux cumple con esa especificación; además, se desarrolló un intérprete escrito en Rust que cubre un gran subconjunto de Python, con un 99.95% de coincidencia en el comportamiento de más de 1.7 millones de programas generados aleatoriamente con CPython. En 36 pequeñas tareas de verificación, Opus 5.5 demostró que necesitaba aproximadamente un 40% menos de tokens que Opus 5 para la mitad de ellas.