Anthropic publica FlashProve: una forma de comprobar con matemáticas qué modelo de IA te ha respondido

El 2 de noviembre de 2026, el equipo Frontier Red Team de Anthropic, con coautores académicos y de la industria, publicó FlashProve, un sistema de código abierto para lo que llaman «inferencia demostrable». «Inferencia» es el momento en que un modelo de IA genera una respuesta a tu pregunta. La idea es que quien la recibe pueda comprobar, con una prueba matemática, que esa respuesta salió realmente del modelo que se anunció y no de otro. Para ello usa zkSNARK, siglas en inglés de un tipo de prueba criptográfica de conocimiento cero: permite demostrar que un cálculo se hizo correctamente sin revelar los datos internos, en este caso los pesos del modelo, que son los números que forman el modelo y que las empresas guardan en secreto.

El problema que intenta resolver es cotidiano aunque casi invisible. Cuando usas un servicio de IA por internet, no tienes forma de saber si detrás está el modelo que te prometen o una versión más barata o recortada, ni si alguien ha manipulado el texto que recibes por el camino. Según Anthropic, una prueba así serviría a los usuarios para verificar el modelo servido, a los evaluadores independientes para confirmar que prueban el modelo real, y a reguladores y auditores para comprobar qué modelos se ejecutan sin acceder a información propietaria. Los proveedores, a su vez, podrían demostrar que cumplen compromisos o obligaciones legales sin enseñar sus pesos.

La publicación incluye un probador, un verificador rápido en C++, un verificador comprobado formalmente en Lean (un lenguaje para demostraciones matemáticas), las pruebas en Lean de las garantías de seguridad principales, un informe técnico y la especificación del protocolo, todo con licencia Apache 2.0. Las cifras se midieron con Llama 4 Maverick, un modelo de 400.000 millones de parámetros con arquitectura de mezcla de expertos y pesos de 4 bits. Generar la prueba va a unos 110 tokens por segundo en una sola GPU H100. Cada petición de 1.024 tokens produce una prueba de unos 19 MB, y verificarla lleva unos 17 segundos en una CPU de 24 hilos, además de descargar un compromiso de unos 6,5 MB.

Hay una fase previa: un paso de compromiso fuera de línea de unos 39 minutos que sirve para unos 16 millones de peticiones. El precio es alto: el coste equivale a entre 70 y 95 veces el tiempo de GPU de ejecutar el mismo modelo con vLLM, un motor habitual de servicio de modelos. Aun así, Anthropic afirma que los sistemas de código abierto anteriores son varios órdenes de magnitud más lentos; por ejemplo, VerInf alcanzaba unos 0,02 tokens por segundo con el mismo modelo. Otro sistema, Attestable, informa de entre 53 y 77 tokens por segundo con un modelo denso de 31.000 millones de parámetros, pero no ha publicado su biblioteca.

Los propios autores enumeran los límites. Las pruebas cubren una versión del modelo con números enteros y decodificación voraz, es decir, que elige siempre la palabra más probable, y no la generación con aleatoriedad que suelen usar los chats. El contexto está limitado a 1.024 tokens, muy por debajo de los de un chat actual. El sistema supone una arquitectura de mezcla de expertos, no oculta la arquitectura del modelo y deja fuera ataques de canal lateral, como analizar tiempos de respuesta. El código rápido y el artículo no están garantizados formalmente para coincidir con el protocolo en Lean, y como no se entrega el probador en Lean, la propiedad de conocimiento cero depende de las auditorías de seguridad del propio proveedor. Anthropic lo describe como un prototipo de investigación y un avance intermedio, no una agenda cerrada.

Lo que aún no se sabe es si algún servicio comercial lo adoptará, ni cuándo. Anthropic no anuncia en la página que vaya a ofrecer esta verificación en Claude, y con un sobrecoste de dos órdenes de magnitud no es viable para el uso diario. Su valor inmediato está en la comunidad investigadora, que ahora tiene código abierto para mejorar la velocidad y ampliar los límites.