Anthropic lanza sistema para verificar respuestas de modelos de IA

Anthropic lanzó el 2 de noviembre FlashProve, un sistema de código abierto que permite verificar si una respuesta de un modelo de IA fue generada por ese modelo y no por otro. Según la empresa, los usuarios de chatbots carecen actualmente de mecanismos técnicos para confirmar si un intermediario alteró o sustituyó el modelo consultado.

El sistema utiliza zkSNARK, un tipo de prueba criptográfica corta y rápida que no revela datos secretos. El proveedor del modelo publica primero una huella de sus pesos, es decir, de los parámetros internos que definen cómo responde. Después, adjunta una prueba a cada respuesta. Cualquiera que tenga la huella, la pregunta y la respuesta puede verificar la prueba sin conocer los pesos ni disponer de una infraestructura costosa.

En pruebas descritas en su informe técnico, Anthropic ejecutó el sistema con Llama 4 Maverick, un modelo de Meta de 400.000 millones de parámetros, en una versión comprimida a cuatro bits publicada por un tercero. Según esas mediciones, con una sola tarjeta gráfica H100, el generador de pruebas procesa unos 110 tokens por segundo, las unidades de texto que cuenta y cobra un modelo.

Cada prueba pesa unos 19 MB por solicitud de 1.024 tokens. Verificarla lleva 17 segundos en un procesador de 24 hilos y 21 segundos en uno solo, sin tarjeta gráfica. La preparación inicial del modelo tarda unos 39 minutos y sirve para unos 16 millones de solicitudes, tras las cuales hay que repetirla.

El costo es alto. Según Anthropic, generar las pruebas requiere entre 70 y 95 veces el tiempo de tarjeta gráfica que usa vLLM, una biblioteca abierta de uso común, para procesar los mismos textos. La empresa afirma que sistemas anteriores eran órdenes de magnitud más lentos.

Entre ellos cita a VerInf, que, según el informe de Anthropic, tardó 14,3 horas en probar 1.000 tokens con el mismo modelo. También menciona a Attestable, una empresa que informa entre 53 y 77 tokens por segundo con un modelo distinto, aunque no ha publicado su código.

Anthropic señala cuatro usos posibles. Uno es que evaluadores independientes confirmen que el modelo que prueban es el que se ofrece al público. Otro es detectar un servidor comprometido. Los otros dos son demostrar con pruebas que un análisis de seguridad se hizo con un modelo concreto y apoyar a reguladores que exijan servir solo modelos aprobados.

El informe técnico de Anthropic enumera las restricciones. El sistema solo maneja contextos de hasta 1.024 tokens, mucho menos que las conversaciones reales, y exige que el modelo sea de tipo mixtura de expertos, en el que solo se activa una parte de la red por cada token.

La prueba es sobre una versión con aritmética de números enteros del modelo y con decodificación determinista. Una respuesta generada con aritmética de coma flotante o con muestreo aleatorio podría diferir de lo que la prueba cubre. La arquitectura del modelo tampoco queda oculta, solo los pesos.

Anthropic también advierte que medir el tiempo que tarda en generarse una prueba podría filtrar información sobre los pesos, un riesgo que dejó fuera de esta versión. Además, el código rápido en C++ no tiene garantía formal, aunque coincide con el verificador en Lean en todas las pruebas realizadas.

Lean es un lenguaje de verificación formal con el que la empresa escribió demostraciones matemáticas de las propiedades de seguridad. Anthropic dice que Claude, su modelo, contribuyó a optimizar el sistema, y por eso incluyó enunciados auditables por humanos. El código, las demostraciones y el informe técnico se publicaron bajo licencia Apache 2.0.