FlashProve, de Anthropic, demuestra criptográficamente que una respuesta procede de unos pesos comprometidos

Anthropic presentó el 2 de noviembre FlashProve, un sistema de investigación de código abierto para lo que denomina inferencia demostrable: una forma de que cualquiera compruebe que la respuesta de un modelo de lenguaje la generó realmente un modelo determinado, y no un sustituto más barato o una versión manipulada. El trabajo reúne a investigadores de Anthropic con criptógrafos de la EPFL, el MIT y las empresas StarkWare y Succinct.

Cómo funciona

El proveedor publica primero un compromiso criptográfico breve, una especie de huella de los pesos de su modelo. Este paso previo tardó unos 39 minutos por modelo, y un solo compromiso sirve para unos 16 millones de solicitudes. Después, para cada solicitud, el sistema genera un argumento sucinto de conocimiento cero (zkSNARK) que demuestra que esos pesos, aplicados al prompt, producen los tokens devueltos. Quien verifica no sabe nada de los pesos, los valores intermedios ni los expertos activados; la arquitectura, en cambio, no queda oculta.

Anthropic probó el sistema con Llama 4 Maverick de Meta, un modelo de mezcla de expertos de 400.000 millones de parámetros, en una conversión pública de 4 bits, usando una única GPU H100 y 24 núcleos de CPU. Según la empresa, alcanza unos 110 tokens por segundo de prueba, con un coste de entre 66 y 95 veces el tiempo de GPU que requiere servir las mismas solicitudes con vLLM. Cada solicitud de 1.024 tokens da lugar a una prueba de unos 19 MB, que se verifica en unos 17 segundos con 24 hilos de CPU y sin GPU. Un trabajo anterior sobre el mismo modelo, VerInf, necesitó más de 14 horas para 1.000 tokens, según los autores.

Las propiedades de completitud, solidez y conocimiento cero del protocolo se enunciaron y demostraron formalmente con el asistente de pruebas Lean. El código, las pruebas y la documentación tienen licencia Apache 2.0.

Límites y posibles usos

Los propios autores enumeran las salvedades. El verificador rápido en C++ carece de garantía formal, aunque coincidió con el verificador en Lean, más lento, en todas las pruebas. Las demostraciones cubren una versión entera exacta del modelo con decodificación voraz, por lo que las salidas muestreadas quedan fuera; el contexto se limita a 1.024 tokens; las pruebas se generan por lotes a posteriori, y los canales laterales, como el tiempo de ejecución, no se contemplan. Los resultados aún no se han reproducido de forma independiente.

Anthropic plantea que estas pruebas ayudarían a los usuarios a confirmar que reciben el modelo por el que pagan y a auditores y reguladores a contrastar lo que afirman los proveedores. La empresa lo presenta como una herramienta más, junto al hardware de confianza.