FlashProve es la prueba criptográfica con la que Anthropic quiere acabar con un acto de fe: hoy nadie puede comprobar qué modelo generó la respuesta que lee en pantalla. Un servicio de enrutamiento puede servir un modelo barato y cobrar el caro. Un atacante que altere el flujo de tokens puede colar texto falso con apariencia legítima. La calidad del párrafo no delata el cambiazo, y los pesos del modelo, los números internos que definen su conducta, son secretos que el proveedor jamás entrega.
El prototipo salió el 2 de noviembre desde el Frontier Red Team de Anthropic, con Roy Rinberg y Alex Allain al frente y coautores de la EPFL, el MIT, StarkWare y Succinct. La entrega trae cinco piezas: el anuncio, un informe técnico, la especificación del protocolo, el código ejecutable con dos verificadores y las demostraciones en Lean, todo bajo licencia Apache 2.0 y en código abierto. Anthropic lo presenta como progreso intermedio para que otros lo tomen y lo mejoren, palabra por palabra.
Una huella de 6,5 MB contra el modelo impostor
El mecanismo trabaja en dos tiempos. Primero, el proveedor publica un compromiso, una huella breve que fija un único juego de pesos sin mostrarlos; ese archivo de compromiso ronda los 6,5 MB. Después, por cada respuesta, genera una prueba que certifica una frase exacta: el modelo comprometido produce estos tokens con esta entrada. La herramienta es un zkSNARK, una prueba criptográfica de conocimiento cero: convence de que un cálculo se hizo bien sin revelar los datos del cálculo, y cabe en un archivo breve frente a la magnitud de lo probado.
Comprobar sale barato. El verificador corre en una unidad central de procesamiento común, sin tarjeta gráfica y sin acceso a los pesos: tarda 17 segundos con 24 hilos y 21 segundos con un único hilo. La prueba ocupa 18,78 MB por cada petición de 1.024 tokens. Del otro lado, el proveedor pagó la factura fuerte: una sola tarjeta NVIDIA H100 de 80 GB, apoyada en unos 290 GB de memoria del equipo anfitrión, generó las pruebas a unos 110 tokens por segundo, con lotes de 24 peticiones cerrados en cerca de 223 segundos.
El modelo de la demostración impresiona por tamaño: Llama 4 Maverick, de Meta, con 400.000 millones de parámetros en arquitectura de mezcla de expertos, unos 17.000 millones activos por token, en una versión entera de 4 bits que pesa cerca de 232 GB. La fase inicial de compromiso dura unos 39 minutos y sirve para unos 16 millones de peticiones antes de renovarse. El contraste con el trabajo previo es brutal: VerInf, el único sistema anterior sobre ese mismo modelo, avanzaba a 0,02 tokens por segundo y tardó 14,3 horas en probar 1.000 tokens, con una prueba de 93,6 GB que exigió casi un día de verificación.
Claude escribió código que después hay que auditar
Un detalle distingue esta entrega: Claude, el modelo de la propia Anthropic, produjo las mejoras del zkSNARK que aceleraron el sistema. Anthropic admite que Claude optimiza muy bien y a la vez toma decisiones difíciles de evaluar en sistemas grandes. Su antídoto fue escribir las garantías centrales en Lean, un asistente de demostraciones formales: integridad, solidez y conocimiento cero quedan como enunciados que una máquina puede revisar línea por línea. Es el mismo laboratorio que en octubre ocupó titulares criptográficos cuando Claude rastreó el origen de las semillas del NIST hasta un generador de 1997.
Las aplicaciones que Anthropic pone sobre la mesa apuntan a dinero y a regulación. Un evaluador independiente podría confirmar que el modelo examinado antes del lanzamiento es el mismo que atiende al público. Una empresa que contrata capacidad por medio de un intermediario recibiría un recibo matemático de cada respuesta. Un regulador podría exigir pruebas de que un proveedor sirve solo modelos aprobados, o de que su hardware trabaja en inferencia y no entrenando otra cosa a escondidas. Hasta una afirmación comercial gana respaldo: decir que un modelo de frontera revisó una biblioteca de código en busca de fallos dejaría de ser una frase de mercadeo.
Las limitaciones vienen escritas por los propios autores, sin letra pequeña escondida. Probar cuesta entre 70 y 95 veces el tiempo de tarjeta gráfica que consume servir el mismo lote con vLLM, el motor de inferencia abierto de referencia: 72 veces en la medición principal y 94 con la carga más alta. El contexto probado llega a 1.024 tokens, una ventana corta frente a conversaciones reales de cientos de miles. La prueba cubre una copia entera del modelo con decodificación voraz, la elección siempre del token más probable; una respuesta en coma flotante o con muestreo puede apartarse del cálculo certificado. La arquitectura queda visible, los canales laterales como el tiempo de respuesta quedan fuera del alcance, y el verificador rápido en C++ carece de garantía formal: la garantía vive en la versión lenta escrita en Lean.
TechCrunch recogió el punto que separa el laboratorio de la calle: no hay planes de desplegar FlashProve en Anthropic ni en ningún otro laboratorio, y el repositorio se declara sin mantenimiento. La prueba, además, certifica el origen de la respuesta, nunca que la respuesta sea correcta. Para que un lector común reciba ese recibo de 19 MB junto a su chat, un proveedor tendría que publicar su compromiso y correr el probador en cada contestación, un gasto de cómputo que hoy ninguna aplicación comercial asume.
Fuente: Anthropic
