FlashProve demuestra el origen de las respuestas de los LLM

Qué demuestra exactamente FlashProve

Lo esencial resulta muy atractivo: FlashProve permite verificar que una respuesta fue calculada realmente por el modelo declarado, con un conjunto de pesos fijado de antemano. En la investigación de Anthropic sobre inferencia demostrable, el sistema se presenta como un prototipo abierto para grandes modelos de lenguaje con arquitectura mixture-of-experts.

El proveedor primero fija criptográficamente el modelo y sus pesos, y después genera una prueba para una entrada y una salida concretas. Un verificador independiente puede confirmar la corrección del cálculo sin recibir los pesos propietarios. El sistema se apoya en pruebas de conocimiento cero del tipo zkSNARK.

En el momento de su publicación, Anthropic informó de más de 100 tokens por segundo en una sola H100 para Llama 4 Maverick, un modelo de 400.000 millones de parámetros, con cuantización de 4 bits. La prueba de una solicitud de 1.024 tokens ocupaba unos 19 MB. Sin embargo, generar esa prueba requería entre 70 y 95 veces más tiempo de GPU que servir una solicitud comparable mediante vLLM.

Por tanto, ya no es una simple fantasía criptográfica, pero tampoco una marca gratuita junto a cada respuesta de una API. El rendimiento parece convincente, mientras que el tamaño de las pruebas y el cómputo adicional se vuelven problemáticos a gran escala.

También destaca la solidez de la ingeniería. La publicación incluye un prover abierto, un verificador rápido en C++, otro más lento en Lean y una formalización del protocolo en Lean 4. Se declaran pruebas formales de completitud, corrección y conocimiento cero.

Dónde termina esta garantía

FlashProve demuestra el origen del cálculo, no la calidad de la respuesta. La diferencia es fundamental: un modelo inseguro o equivocado puede generar texto inseguro o erróneo con una prueba criptográfica perfectamente válida.

Aun así, el valor práctico es considerable. Un auditor podrá comprobar que producción ejecuta el mismo modelo que fue evaluado; al operador le resultará más difícil sustituir los pesos sin avisar; y un sistema posterior podrá rechazar respuestas sin prueba de un modelo autorizado.

Yo vigilaría primero tres cuellos de botella: el coste del prover, el tamaño de la prueba y la latencia de la verificación independiente. La asimetría es especialmente interesante: crear la prueba exige muchos recursos de GPU, pero verificarla funciona en CPU convencionales. Eso hace más viable la auditoría externa, aunque generar pruebas de forma continua siga siendo caro.

FlashProve no resuelve el alignment, pero elimina una brecha incómoda entre la promesa y el despliegue real. La pregunta «¿respondió este modelo?» puede separarse de otra mucho más difícil: «¿merece confianza su respuesta?».

Anteriormente explicamos cómo las métricas IRT pueden medir la fiabilidad de la evaluación basada en LLM. Ese marco complementa el trabajo de Anthropic sobre inferencia demostrable al reforzar la evidencia para evaluar las salidas de IA.