Cuando pagas por un modelo de IA concreto a través de una app o un revendedor, no tienes forma de comprobar que tu respuesta vino de verdad de ese modelo y no de uno más barato cambiado en silencio para ahorrar dinero. FlashProve, de Anthropic, publicado como prototipo de código abierto, es un primer intento de cerrar esa brecha con criptografía, y es la primera versión de la idea que parece cercana a lo práctico.
La herramienta usa un zkSNARK, un tipo de prueba criptográfica que permite a un servidor convencerte de que un cálculo se hizo bien sin revelar nada más, en este caso sin exponer los pesos del modelo. El proveedor publica primero un compromiso, una huella corta que fija un conjunto exacto de pesos. Luego, para cada respuesta, genera una prueba de que esos pesos comprometidos, ejecutados sobre tu prompt, produjeron exactamente esos tokens. Cualquiera con el compromiso, el prompt y la respuesta puede verificarlo rápido en hardware corriente, sin los pesos y sin reejecutar el modelo. Eso importa para la confianza del consumidor, para que una empresa demuestre que un modelo de frontera revisó de verdad su código, y para que los reguladores comprueben que solo se sirven modelos aprobados.
La velocidad es el titular. En Llama 4 Maverick, un modelo de mezcla de expertos de 400 mil millones de parámetros que reseñamos, una sola GPU H100 produce pruebas a unos 110 tokens por segundo, con una prueba de unos 19 MB por petición de 1.024 tokens, usando pesos cuantizados a 4 bits. El único intento anterior de código abierto iba cerca de 0,02 tokens por segundo, así que es un salto de varios miles de veces. Anthropic entrega el probador, un verificador rápido en C++ y un verificador aparte probado correcto en Lean, todo bajo Apache 2.0, y lo presenta como progreso intermedio y no como un sistema terminado.
El coste es la pega evidente. Generar la prueba lleva unas 70 a 95 veces el tiempo de GPU de solo servir el modelo en vLLM, así que ejecutar FlashProve en cada petición multiplicaría muchas veces el coste de inferencia. Eso por sí solo lo deja fuera de la producción rutinaria por ahora.
Los otros límites merecen decirse con claridad. La prueba se restringe a decodificación voraz y a un contexto de 1.024 tokens, lo que descarta los contextos largos y las salidas muestreadas en los que se apoyan la mayoría de los productos. Y el verificador rápido en C++ no lleva las garantías formales del verificado en Lean, así que el camino cómodo todavía no es el camino probado. Anthropic ha publicado esto para que se construya sobre ello, y así conviene leerlo: una prueba de concepto creíble para la inferencia verificable, no algo que puedas exigir hoy a tu proveedor de modelos.