FlashProve d'Anthropic : prouver l'origine des réponses d'un LLM sans dévoiler ses poids

Le 2 novembre 2026, Anthropic a publié FlashProve, un prototype de recherche open‑source qui utilise des preuves cryptographiques pour attester qu’une réponse d’un modèle de langue provient bien d’un jeu de poids engagé, tout en gardant ces poids secrets. L’objectif est de combler un vide de vérification dans les services d’IAIntelligence artificielleEnsemble de techniques permettant à des machines d'accomplir des tâches nécessitant habituellement certaines capacités humaines, comme la reconnaissance, la prédiction ou la prise de décision. hébergés : on ne sait pas toujours quel modèle a réellement généré la réponse affichée. Un service de routage peut remplacer le modèle, un évaluateur peut recevoir un autre système que celui prévu, ou un attaquant peut altérer le flux de tokensTokenUnité de contenu traitée par un modèle de langage, pouvant représenter un mot, une partie de mot ou un caractère.. Re‑exécuter le modèle n’est pas une solution viable lorsqu’il s’agit de poids privés et de besoins matériels importants.

Comment fonctionne FlashProve

FlashProve s’appuie sur un zkSNARK (zero‑knowledge succinct argument of knowledge) entièrement logiciel, sans dépendre de matériel de confiance. La procédure comporte deux phases :

1. Engagement hors‑ligne – le fournisseur publie un petit engagement qui identifie de façon unique un jeu de poids, tout en les gardant secrets.
2. Preuve à la volée – pour chaque paire invite‑réponse, le système génère une preuve que les tokens produits correspondent exactement aux sorties du modèle engagé.

Quiconque possède l’engagement, le texte d’entrée et la réponse peut vérifier la preuve sans jamais accéder aux poids. Les propriétés attendues sont la complétude (une preuve honnête est acceptée), la sondabilité (une fausse affirmation nécessite de briser des hypothèses cryptographiques largement admises), le zéro‑knowledge (aucune donnée sensible n’est révélée) et la succinctité (la preuve est petite et rapide à vérifier).

Le prototype exploite la structure mixture‑of‑experts du modèle Llama 4 Maverick d’Anthropic. Au lieu de charger les 400 milliards de paramètres du modèleParamètres du modèleValeurs numériques internes apprises pendant l'entraînement et utilisées par le modèle pour produire ses résultats. complet, le travail du prouveur ne dépend que des ~17 milliards de paramètres actifs pour chaque token, ce qui permet de tenir le processus sur un GPUGPUProcesseur conçu pour effectuer de nombreux calculs en parallèle, notamment utilisé pour entraîner et exécuter des modèles d'IA. de 80 Go avec environ 290 Go de mémoire hôte.

Enjeux pratiques et limites

Anthropic imagine plusieurs usages : contrôles d’intégrité client, évaluations indépendantes, outils de conformité réglementaire et certification d’inférenceInférencePhase durant laquelle un modèle entraîné utilise ses paramètres pour produire une prédiction ou une réponse à partir de nouvelles données.. Une inference certificate pourrait ainsi attester qu’une requête a bien été traitée par le modèle annoncé. Cependant, la preuve ne garantit pas que le même matériel n’a pas simultanément entraîné un autre modèle, ce qui limite son pouvoir en matière de conformité liée à l’usage des ressources de calcul.

Performances

Sur une conversion publique en 4 bits du modèle, un serveur équipé d’un H100 et de 24 cœurs CPU a prouvé un lot de 24 requêtes en 223 s, générant une preuve de 18,78 Mo par requête. L’étape d’engagement hors‑ligne a duré ~39 minutes. La vérification côté client, réalisée sur CPU uniquement, a nécessité 17 s avec 24 threads (ou 21 s en mono‑thread) pour télécharger un engagement de 6,5 Mo et vérifier la preuve. Comparé à une inférence FP8 sur huit H100, le processus de preuve consomme environ 72 à 94 fois plus de temps GPU pour le même lot, ce qui montre un coût significatif.

Vérification formelle et état du projet

Le dépôt FlashProve (version 0.16.0) comprend un prouveur, un vérificateur C++ rapide, un vérificateur Lean plus lent, les preuves Lean des affirmations mathématiques et un visualiseur sous licence Apache 2.0. Le travail Lean formalise complétude, sondabilité et zéro‑knowledge dans le modèle de l’oracle aléatoire, mais requiert encore une relecture manuelle pour s’assurer que les énoncés correspondent aux garanties voulues. Le vérificateur C++ utilisé en pratique n’a aucune garantie formelle ; il a simplement été testé pour être en accord avec le vérificateur Lean.

Le projet indique clairement que la quasi‑totalité du code, des preuves Lean et de la documentation a été générée par des systèmes d’IA sous supervision humaineHuman in the LoopApproche intégrant une intervention humaine dans le fonctionnement, la validation ou les décisions d'un système automatisé., et qu’aucun audit de sécurité indépendant n’a été réalisé. Les tests de dissimulation des poids et de résistance aux preuves adverses restent limités. De plus, les preuves couvrent uniquement une version entière des poids sous décodage greedy. Le décodage en virgule flottante ou à base d’échantillonnage peut diverger du calcul prouvé, et les contextes supérieurs à 1 024 tokens ne sont pas couverts. Les attaques par canaux auxiliaires (timing, side‑channel) sont également hors du champ de garantie.

Perspectives

Pour que la preuve vérifiable d’inférence devienne un contrôle routinier du trafic servi, il faudra :

• réduire le coût de génération de preuve,
• étendre la prise en charge aux décodages plus souples et aux contextes plus longs,
• renforcer le lien entre l’implémentation rapide (C++) et le protocole formel.

En l’état, FlashProve montre qu’il est possible d’attester l’appartenance d’une sortie à un modèle précis sans dévoiler le modèle, mais le prix en temps et la portée des garanties restent des obstacles majeurs avant une adoption massive.

Au‑delà du prototype

Si les acteurs du secteur – fournisseurs de cloud, plateformes d’IA et régulateurs – cherchent à instaurer davantage de transparence, des solutions comme FlashProve pourraient devenir des composantes clés d’un écosystème plus fiable. Le défi sera de concilier la rigueur cryptographique avec les exigences de performance des services d’inférence en temps réel.