Anthropic publica FlashProve para generar pruebas criptográficas de inferencia de IA

Anthropic publicó FlashProve el 2 de noviembre de 2026: un prototipo de investigación de código abierto que utiliza pruebas criptográficas para demostrar que una respuesta de un modelo de lenguaje procede de unos pesos comprometidos, sin revelarlos. La empresa informó que la generación de pruebas alcanzó 110 tokens por segundo con Llama 4 Maverick de Meta.

Este trabajo aborda una brecha de verificación en la IA alojada. Una respuesta de alta calidad no permite saber qué modelo la generó: un servicio de enrutamiento podría sustituirlo por otro sistema, un evaluador podría recibir un modelo distinto del previsto para la prueba o un atacante podría alterar el flujo de tokens. Para los usuarios, comprobarlo volviendo a ejecutar el modelo no es práctico cuando los pesos son privados y los requisitos de hardware son considerables.

Vincular las respuestas a pesos ocultos

FlashProve utiliza un argumento sucinto de conocimiento de conocimiento cero, o zkSNARK, en un diseño que solo requiere software y no depende de hardware de confianza. Durante una fase sin conexión, el proveedor publica un compromiso breve que identifica un conjunto exacto de pesos y los mantiene en secreto. Para cada par de solicitud y respuesta completado, el sistema genera una prueba de que los tokens de salida son el resultado del modelo comprometido. Cualquiera que disponga del compromiso, la solicitud y la respuesta puede verificar la prueba sin acceder a los pesos.

Las propiedades previstas son completitud, solidez, conocimiento cero y concisión. Una prueba honesta debería aceptarse, mientras que certificar una afirmación falsa debería requerir romper supuestos criptográficos ampliamente aceptados. Verificar una prueba no debería revelar ni los pesos ni los valores intermedios del cálculo. El diseño también oculta qué subredes de mezcla de expertos se ejecutaron para cada token, aunque la arquitectura del modelo sigue siendo visible.

La implementación aprovecha la estructura de mezcla de expertos de Maverick. El trabajo del probador se escala en función de los aproximadamente 17.000 millones de parámetros activos para un token, en lugar de los 400.000 millones totales, y a la vez oculta qué expertos se eligieron. Los pesos segmentados se transmiten desde la memoria del servidor, lo que permite ejecutar el probador en una sola GPU de 80 GB con unos 290 GB de memoria del servidor disponibles.

Anthropic describe posibles usos en comprobaciones de integridad para clientes, evaluaciones independientes, herramientas regulatorias y aplicación de requisitos sobre modelos aprobados. Los certificados de inferencia podrían acreditar que las solicitudes fueron atendidas por el modelo declarado, pero no demostrarían que el mismo hardware no se utilizó también para entrenar otro modelo. Esta distinción limita lo que esos certificados podrían demostrar respecto de los requisitos de cumplimiento basados en el uso de la capacidad de cómputo.

Rendimiento de las pruebas y sobrecarga de inferencia

La evaluación de Anthropic utilizó una conversión de 4 bits del modelo disponible públicamente. Un servidor con una H100 y 24 núcleos de CPU generó pruebas para un lote de 24 solicitudes en unos 223 segundos y produjo una prueba de 18,78 MB por solicitud. La fase de compromiso sin conexión tardó unos 39 minutos.

Para verificar, el cliente descarga un compromiso de aproximadamente 6,5 MB y comprueba las pruebas en una CPU, sin GPU. Anthropic midió un tiempo de verificación de 17 segundos con 24 subprocesos y de 21 segundos con uno, incluidas las comprobaciones de la fase sin conexión.

Estas mediciones distinguen un proceso de verificación que solo utiliza la CPU de una operación de generación de pruebas mucho más exigente. En la comparación de Anthropic con la inferencia FP8 en ocho H100 que ejecutaban vLLM, generar las pruebas requirió unas 72 veces más tiempo por GPU para el mismo lote y unas 94 veces más con la carga más alta de vLLM que se probó. Por tanto, este rendimiento conlleva un coste considerable frente a servir el modelo sin pruebas.

Verificación formal y límites prácticos

El repositorio de FlashProve incluye un probador, un verificador rápido en C++, un verificador más lento en Lean, pruebas Lean de enunciados matemáticos de alto nivel y un visualizador interactivo de teoremas, todo bajo la licencia Apache 2.0. La versión 0.16.0 se describe como un artefacto de investigación sin mantenimiento que no acepta contribuciones.

El trabajo en Lean aborda la completitud, la solidez y el conocimiento cero en el modelo del oráculo aleatorio. Aún es necesario revisar manualmente los enunciados formales para establecer que expresan las garantías previstas. El verificador Lean está conectado formalmente con el teorema de solidez, pero el verificador en C++ destinado al uso habitual no cuenta con garantías formales; en su lugar, se comprobó que sus resultados coincidieran con los del verificador Lean.

La documentación sobre las limitaciones conocidas del proyecto indica que sistemas de IA bajo dirección humana escribieron casi todo el software, las pruebas Lean y la documentación, y ejecutaron las pruebas cuyos resultados se comunicaron. No se ha realizado ninguna auditoría de seguridad independiente y las pruebas sobre el ocultamiento de los pesos y las pruebas adversariales siguen siendo limitadas.

Las pruebas cubren una versión entera exacta de los pesos con decodificación voraz. La inferencia en coma flotante o la decodificación por muestreo pueden diferir del cálculo que se demuestra, y las pruebas genéricas de errores no cubren solicitudes diseñadas de forma adversarial. Los contextos están limitados a 1.024 tokens, mientras que los ataques de temporización y otros ataques de canal lateral quedan fuera de la garantía. La generación de pruebas a posteriori también implica volver a realizar cálculos, garantías tardías y no determinismo, a diferencia de generar las pruebas durante la inferencia.

Para que la inferencia verificable se convierta en una comprobación rutinaria del tráfico atendido, el trabajo pendiente se concentra en las limitaciones que pone de manifiesto este lanzamiento: reducir el costo de generar pruebas, admitir decodificaciones menos restrictivas y contextos más largos, y vincular con mayor solidez la implementación rápida al protocolo formal.