L'ESSENTIEL EN 30 SECONDES

  • FlashProve produit une preuve à divulgation nulle de connaissance attestant que des poids engagés, appliqués à un prompt, ont généré les jetons renvoyés, sans révéler ces poids.
  • Sur Llama 4 Maverick (4 bits) et un seul H100, le système prouve environ 110 jetons par seconde ; chaque requête de 1 024 jetons donne une preuve d'environ 19 Mo, vérifiée en 17 secondes environ sur CPU.
  • Le code, les preuves Lean et la documentation sont sous licence Apache 2.0 ; les auteurs le présentent comme un prototype de recherche aux limites assumées.

Anthropic a publié le 2 novembre FlashProve, un système de recherche open source consacré à ce que l'entreprise appelle l'inférence prouvable : un moyen, pour n'importe qui, de vérifier que la réponse d'un modèle de langage provient bien d'un modèle précis, et non d'un substitut moins coûteux ou d'une version altérée. Les travaux associent des chercheurs d'Anthropic à des cryptographes de l'EPFL, du MIT ainsi que des sociétés StarkWare et Succinct.

Le principe

Le fournisseur commence par publier un engagement cryptographique court, sorte d'empreinte de ses poids. Cette étape hors ligne a pris environ 39 minutes par modèle, et un même engagement couvre quelque 16 millions de requêtes. Pour chaque requête, le prouveur génère ensuite un argument succinct à divulgation nulle de connaissance (zkSNARK) montrant que ces poids, appliqués au prompt, donnent bien les jetons renvoyés. Le vérificateur n'apprend rien des poids ni des valeurs intermédiaires, pas même quels experts du modèle à mélange d'experts ont servi ; l'architecture, elle, reste visible.

Anthropic a testé l'outil sur Llama 4 Maverick de Meta, un modèle à mélange d'experts de 400 milliards de paramètres, dans une version publique quantifiée sur 4 bits, avec un seul GPU H100 et 24 cœurs CPU. L'entreprise annonce un débit de preuve d'environ 110 jetons par seconde, pour un coût de 66 à 95 fois le temps GPU nécessaire pour servir les mêmes requêtes avec vLLM. Une requête de 1 024 jetons produit une preuve d'environ 19 Mo, vérifiable en 17 secondes environ sur 24 threads CPU, sans GPU. Selon les auteurs, un travail antérieur sur le même modèle, VerInf, demandait plus de 14 heures pour 1 000 jetons.

La complétude, la robustesse et la propriété de divulgation nulle du protocole ont été énoncées et démontrées formellement avec l'assistant de preuve Lean. Code, preuves et documentation sont publiés sous licence Apache 2.0.

Limites et usages envisagés

Les auteurs détaillent eux-mêmes les réserves. Le vérificateur rapide en C++ n'a pas de garantie formelle, même s'il a concordé avec le vérificateur Lean, plus lent, lors de tous les tests. Les preuves portent sur une version entière exacte du modèle en décodage glouton : les sorties échantillonnées ne sont pas couvertes. Le contexte est limité à 1 024 jetons, la preuve se fait par lots a posteriori et les canaux auxiliaires, comme le temps d'exécution, sont exclus. Les résultats n'ont pas encore été reproduits de manière indépendante.

Selon Anthropic, ces preuves aideraient les utilisateurs à s'assurer qu'ils reçoivent bien le modèle payé, et les auditeurs comme les régulateurs à contrôler les déclarations des fournisseurs. L'entreprise y voit un outil parmi d'autres, aux côtés du matériel de confiance.