Anthropic usa Claude para demostrar propiedades de seguridad en 123 bibliotecas de software
El trabajo con Theorem convierte pruebas existentes en reglas matemáticas y publica parte de las demostraciones; sus garantías se limitan a entradas, plataformas y condiciones concretas.
Por qué confiar en Pulso Diario
Ilustración editorial original
Las bibliotecas de software son paquetes de funciones reutilizables por otros programas. Probar un programa con muchos ejemplos puede encontrar errores, pero no demostrar que ningún otro ejemplo vaya a fallar. La verificación formal aborda esa diferencia mediante razonamiento matemático. Anthropic y Theorem presentaron el 22 de octubre un experimento para automatizar parte de ese trabajo con Claude.
Qué demostraron y cómo
El equipo partió de pruebas de OSS-Fuzz, un proyecto que busca fallos introduciendo muchas entradas distintas en programas abiertos. Transformó esas pruebas en afirmaciones sobre el comportamiento del código ya compilado para procesadores RISC-V, un diseño que define las instrucciones básicas que ejecuta el chip. Claude escribió demostraciones y el comprobador matemático Rocq verificó si satisfacían las reglas. Según el informe, se probaron propiedades de ausencia de fallos en 239 puntos de entrada, las vías usadas para introducir datos de prueba, de 123 bibliotecas, en ocasiones después de corregir problemas encontrados durante el proceso.
La garantía tiene un perímetro
La propiedad examinada cubre entradas inferiores a 64 megabytes y evita los fallos detectados por las comprobaciones incluidas, entre ellos ciertos errores de acceso a la memoria, dentro del modelo utilizado. Se supone un programa y sus dependencias unidos en un mismo ejecutable, un único flujo de operaciones, un presupuesto de memoria fijo y un entorno definido del sistema operativo Linux. No demuestra que toda función haga lo que espera el usuario, que todo el sistema operativo sea seguro o que el mismo resultado se aplique automáticamente a otro procesador. Los propios autores advierten que las bibliotecas pueden conservar errores fuera de lo demostrado.
Fuentes: [1] Anthropic · informe técnico completo y límites
Ilustración editorial original
Por qué el comprobador también importa
La confianza final depende de que las reglas elegidas expresen el problema correcto, de que el modelo matemático del procesador y de Linux sea fiel y de que Rocq compruebe bien las demostraciones. Anthropic publica una parte de ellas y componentes necesarios para que otros puedan verificarlas y reutilizarlas. El informe también explora otras técnicas y arquitecturas, pero esas experiencias no deben mezclarse con la cifra principal de 123 bibliotecas. El trabajo no elimina la necesidad de revisar qué se está garantizando.
La prueba matemática debe explicar primero qué comportamiento garantiza
El avance útil sería abaratar garantías precisas que otros puedan comprobar. Su valor se pierde si la palabra demostrado se convierte en una etiqueta general de seguridad. Una herramienta así debería acompañar cada prueba con una explicación legible de su alcance: qué entradas cubre, qué entorno supone y qué comportamiento no ha intentado demostrar. Esa información permite decidir dónde aporta protección y dónde siguen haciendo falta otras comprobaciones.
Opinión de Pulso Diario · elaborada a partir de los hechos y fuentes citadosFuentes y límites de verificación
Se leyó el informe técnico íntegro, incluidas sus secciones de limitaciones y componentes de confianza. No se ejecutaron las demostraciones ni se hizo una auditoría del código. Theorem es colaborador del proyecto y no se presenta como contraste independiente.
Comentarios · ¿qué duda te queda?
¿Qué dato te ayudaría a entender mejor esta noticia? Comparte tu pregunta o señala un posible error con su fuente. Usaremos las dudas para orientar nuevas explicaciones, sin prometer una respuesta individual.
Los comentarios se revisan antes de publicarse. Respeta a los demás, aporta argumentos y evita publicidad o datos personales. Puedes eliminar tus propios comentarios.
Google se cargará al pulsar. Privacidad.
Has accedido con Google.
Más en Inteligencia artificial
Claude amplía su marca de agua textual a tres modelos: qué permite detectar y qué no
Claude abre hilos temporales para agilizar conversaciones largas sin reducir los tokens facturados
La historia viral de Claude Code y 17.342 fotos: qué revisar en tu iPhone
OpenAI presenta LifeVal para evaluar la ayuda de la IA en tareas cotidianas
IA cuántica: la carrera por calcular lo que hoy se nos resiste
Gemini tiene diez consejos para la próxima década: el primero empieza por tu cuerpo
Karpathy se hartó de YouTube: así creó HackerTube con IA en unas dos horas
Los nuevos proyectos de pago de Gemini API guardan solicitudes por defecto: cómo controlar el registro
Sheets añade las fuentes web de las respuestas generadas con Gemini a cada celda
«Brain fry»: cuando supervisar la IA se convierte en otra carga de trabajo
AlphaFold y las curas con IA: qué está demostrado y qué falta
