Le 2 novembre 2026, Anthropic a présenté FlashProve, un prototype de recherche open source conçu pour vérifier si certains tokens d’une réponse correspondent aux poids engagés d’un modèle. La preuve porte sur l’origine de la sortie dans un calcul précis, pas sur la justesse de la réponse. Anthropic décrit le protocole et ses résultats.
Ce que FlashProve vérifie
Un fournisseur commence par créer un engagement cryptographique sur un ensemble précis de poids, autrement dit une valeur qui fixe le modèle utilisé sans révéler ces poids. Pour une requête, FlashProve produit ensuite une preuve qu’un vérificateur peut examiner à partir de l’engagement, du prompt et de la réponse. La méthode s’appuie sur des zkSNARK, des preuves cryptographiques succinctes et non interactives conçues pour vérifier un calcul sans divulguer certaines de ses données.
Selon Anthropic, la preuve masque les poids et certaines informations intermédiaires, mais pas l’architecture du modèle. Elle permet de vérifier que les tokens contrôlés proviennent du modèle engagé selon le calcul spécifié. Elle ne renseigne pas sur la qualité factuelle de la réponse.
Des résultats rapportés sur Llama 4 Maverick
Anthropic a évalué FlashProve avec Llama 4 Maverick, un modèle à mélange d’experts de 400 milliards de paramètres, dont environ 17 milliards sont actifs pour chaque token. L’essai utilisait une conversion publique en 4 bits réalisée par un tiers. Les poids du modèle ne sont pas inclus dans la publication.
Sur un H100 et avec 24 cœurs CPU, Anthropic rapporte qu’un lot de 24 requêtes a demandé environ 223 secondes pour produire les preuves, soit un débit annoncé de 110 tokens par seconde. Chaque preuve pesait 18,78 Mo et vérifiait un token. Le test portait sur une fenêtre de 1 024 tokens.
La vérification pouvait, selon les mesures d’Anthropic, s’effectuer sur CPU : 17 secondes avec 24 threads, ou 21 secondes avec un seul thread. Le client devait aussi télécharger un engagement de modèle d’environ 6,5 Mo. La préparation initiale de cet engagement prenait près de 39 minutes par modèle; Anthropic indique qu’il pouvait ensuite servir pour environ 16 millions de requêtes.
Le débit de 110 tokens par seconde concerne la production des preuves dans ces conditions, pas la vitesse ordinaire de génération d’un modèle. Pour comparer FlashProve à vLLM, Anthropic a utilisé la version FP8 du même modèle sur huit H100. L’entreprise rapporte environ 72 fois plus de temps GPU par GPU pour la preuve, avec une variation de 66 à 77 fois selon les essais, et environ 94 fois à la charge vLLM la plus élevée testée.
Le calcul prouvé a un périmètre précis
FlashProve vérifie une version entière du modèle avec un décodage glouton, qui sélectionne à chaque étape le token ayant le score le plus élevé. Le contexte est limité à 1 024 tokens dans la description actuelle. Les sorties obtenues avec des calculs en virgule flottante ou un décodage par échantillonnage peuvent différer du calcul vérifié. L’affirmation publiée ne constitue donc pas une attestation générale de paramètres de génération comme la température ou l’effort de recherche.
La preuve intervient après la génération : FlashProve traite des lots de texte et ne vérifie qu’un sous-ensemble de tokens, plutôt que de certifier chaque token au moment où il apparaît. Anthropic cite le recalcul nécessaire, le délai avant l’obtention d’une garantie et le non-déterminisme parmi les contreparties de cette approche.
La vérification formelle ajoute une autre réserve. Anthropic a publié des preuves écrites en Lean, un assistant de preuve utilisé pour formaliser des énoncés mathématiques. Mais l’entreprise précise que le protocole Lean, l’article et le code exécutable rapide ne sont pas formellement garantis équivalents. Le vérificateur C++ a donné les mêmes résultats que celui de Lean pour toutes les preuves testées par Anthropic.
Les éléments publiés par Anthropic
La publication comprend un prouveur, un vérificateur rapide en C++, un vérificateur en Lean, une spécification du protocole, des preuves formelles et un visualiseur interactif de théorèmes. Anthropic indique que le code, les preuves Lean et la documentation sont sous licence Apache 2.0. Le prototype reste une étape de recherche, et les poids de Llama 4 Maverick ne font pas partie des fichiers publiés.
