Anthropic acelera las pruebas criptográficas de IA

Anthropic presentó FlashProve, un prototipo que permite demostrar criptográficamente qué modelo produjo una respuesta de IA sin revelar sus pesos, es decir, los valores internos que definen cómo funciona el modelo.

La idea responde a un problema que hoy no tiene una solución sencilla: cuando usas un modelo a través de una API, no puedes comprobar por tu cuenta que la respuesta salió realmente del sistema que el proveedor anuncia. Un servicio de enrutamiento podría sustituirlo por uno más barato, un atacante podría alterar los resultados o un servidor comprometido podría estar ejecutando otro modelo.

Una prueba en lugar de una promesa

FlashProve utiliza un tipo de prueba criptográfica llamado zkSNARK. En términos simples, el proveedor entrega junto a la respuesta un certificado que demuestra que una versión concreta del modelo recibió ese mensaje y generó esos tokens.

El usuario no necesita descargar los pesos ni volver a ejecutar el modelo. Solo verifica la prueba. Además, el certificado no revela los pesos ni los valores intermedios usados durante la inferencia, aunque sí deja visible la arquitectura general del modelo.

La prueba se ata a una especie de huella digital de los pesos. Si el proveedor se comprometió con una versión concreta, una respuesta generada por otra versión no debería superar la verificación, salvo que alguien consiga romper los supuestos criptográficos del sistema.

El objetivo es que el usuario pueda verificar la respuesta sin tener los pesos del modelo ni la infraestructura necesaria para ejecutarlo.

Qué resultados obtuvo

Anthropic probó el sistema con Llama 4 Maverick, un modelo de tipo Mixture-of-Experts con 400.000 millones de parámetros. En este tipo de modelos, cada token activa solo una parte de los parámetros, alrededor de 17.000 millones en este caso.

Con una GPU H100 y pesos cuantizados a 4 bits, el sistema generó pruebas a unos 110 tokens por segundo. Cada solicitud de 1.024 tokens produjo un archivo de prueba de aproximadamente 19 MB.

La verificación se realizó en una CPU de 24 núcleos y tardó unos 17 segundos por prueba. No requiere una GPU ni acceso a los pesos del modelo. La huella inicial de los pesos ocupa alrededor de 6,5 MB.

El coste sigue siendo elevado. Generar las pruebas tomó entre 70 y 95 veces más tiempo de GPU que ejecutar la misma carga con vLLM, un motor de inferencia habitual. Por eso, el sistema no está listo para añadir una prueba completa a cada respuesta de un chat sin afectar de forma importante a la velocidad y al coste.

Para qué podría servir

La verificación tendría usos concretos para empresas, auditores y reguladores:

• Comprobar que se sirve el modelo contratado cuando una compañía usa un intermediario para acceder a una IA.
• Detectar sustituciones o manipulaciones en servidores comprometidos.
• Demostrar que una evaluación se hizo con el modelo correcto, algo importante al comparar sistemas antes y después de una actualización.
• Verificar compromisos regulatorios, como servir únicamente modelos aprobados o demostrar que cierta infraestructura se destinó a inferencia.
• Acreditar el origen de una respuesta, por ejemplo, cuando una empresa afirma que un modelo revisó código o analizó un plan de negocio.

Esto no demuestra que la respuesta sea correcta ni que el modelo sea seguro. Solo prueba que la respuesta coincide con la ejecución del modelo comprometido para esa entrada.

Una investigación abierta, no un producto terminado

Anthropic publicó el código, el protocolo, un verificador rápido en C++ y otro implementado en Lean, un lenguaje usado para expresar y comprobar matemáticamente propiedades de un sistema. También liberó pruebas formales de las garantías principales: que las pruebas honestas sean aceptadas, que las falsas no puedan fabricarse de forma viable y que no filtren los pesos.

Pero el propio equipo marca varias limitaciones. El prototipo prueba una versión entera del modelo con decodificación codiciosa, no cualquier ejecución de coma flotante ni respuestas generadas mediante muestreo. Además, solo trabaja con ventanas de hasta 1.024 tokens, muy por debajo de los contextos de cientos de miles o millones de tokens que ofrecen algunos modelos actuales.

Tampoco oculta la arquitectura del modelo y, por ahora, está especialmente diseñado para sistemas Mixture-of-Experts. Anthropic advierte además que el código rápido todavía no tiene las mismas garantías formales que el verificador lento escrito en Lean, y que ciertos ataques por canales laterales, como analizar cuánto tarda en generarse una prueba, quedan fuera del alcance de esta versión.

La importancia de FlashProve no está en que vaya a cambiar mañana la experiencia de un chatbot. Está en que reduce la distancia entre ejecutar un modelo y poder demostrar que se ejecutó el modelo correcto. El siguiente paso será bajar el coste, ampliar el contexto y cerrar la brecha entre las garantías matemáticas y el código que se usa en producción.