Anthropic dévoile FlashProve : la preuve que la réponse vient bien de votre LLM

Vous avez payé pour un modèle haut de gamme, mais un service intermédiaire l'a remplacé en chemin par un modèle bon marché. Il est presque impossible de s'en apercevoir à la lecture de la réponse : la qualité peut rester tout à fait correcte. Anthropic a publié un prototype de recherche qui tente de combler cette faille grâce à la cryptographie.

Ce qui a été réalisé

Le système s'appelle FlashProve. Le principe : le fournisseur du modèle publie à l'avance une « empreinte » de ses poids (commitment). Les poids eux-mêmes restent secrets. Ensuite, il joint à chaque réponse une courte preuve de type zkSNARK attestant que ces poids précis, appliqués à ce prompt, ont bien produit ces tokens. L'utilisateur vérifie la preuve sur un simple CPU, sans les poids et sans matériel puissant.

Imaginez un sceau notarial apposé sur chaque réponse du modèle. Le sceau ne peut pas être falsifié, et le notaire ne voit pas le contenu du coffre où sont conservés les poids.

Les chiffres

Les tests ont porté sur Llama 4 Maverick : 400 milliards de paramètres, mixture of experts, quantification en 4 bits. Un seul H100 génère des preuves à un rythme d'environ 110 tokens par seconde. La taille de la preuve est d'environ 19 Mo par requête de 1024 tokens. Cela représente 70 à 95 fois plus de temps GPU que le modèle seul sous vLLM. Selon les auteurs, les systèmes ouverts précédents sont plus lents de plusieurs ordres de grandeur.

Une partie du travail a été réalisée par Claude lui-même, qui a optimisé le système. Mais de telles optimisations sont difficiles à vérifier dans un code complexe ; les garanties de sécurité clés ont donc été formulées sous forme d'énoncés en Lean, un langage de vérification formelle. Ils peuvent être audités séparément, grâce à un outil de visualisation. Cinq artefacts ont été publiés : un article, un rapport technique, une description du protocole, le code (prover, vérificateur rapide en C++ et vérificateur validé en Lean) et les preuves elles-mêmes. Licence Apache 2.0.

À quoi cela sert

Les auteurs citent quatre scénarios :

• Pacing de l'IA : un régulateur vérifie que le matériel exécute réellement l'inférence du modèle déclaré, et n'entraîne pas autre chose en parallèle.
• Protection contre la substitution : une entreprise s'assure que ses serveurs font tourner exactement les poids attendus, même si le serveur est compromis ou si le modèle se substitue lui-même.
• Provenance du texte : on peut prouver que le code a été relu par un modèle puissant. Par exemple, « Proof-of-Failure » : le modèle a dépensé au moins un million de tokens sans trouver de bug dans un patch.
• Approbation des modèles : un régulateur vérifie que seuls des modèles autorisés tournent en production.

Anthropic mentionne par ailleurs sa Frontier Safety Roadmap, dont l'objectif était de réaliser un prototype d'ici le 30 septembre 2026. Cet objectif a été atteint par un autre projet, voisin : le trafic est signé et l'inférence est recalculée sur un serveur de confiance. FlashProve poursuit le même but par une autre voie.

Limites

La solution n'est pas prête pour la production. Un surcoût de plusieurs dizaines de fois en temps GPU la rend inapplicable à chaque requête d'un chat ordinaire. L'architecture du modèle n'est pas dissimulée, seuls les poids le sont. La preuve ne démontre pas que le matériel n'entraîne pas de modèle en parallèle. Les auteurs eux-mêmes parlent d'un résultat intermédiaire, et non d'un programme abouti.

Il existe aussi une alternative : les environnements d'exécution de confiance matériels (TEE) reposent sur le fabricant de puces, alors qu'ici la sécurité repose sur la complexité de calcul de problèmes cryptographiques. Les auteurs considèrent ces approches comme complémentaires.

Que faire en pratique

Si vous développez un routeur, un agrégateur de modèles ou un proxy d'API, suivez ce domaine : d'ici quelques années, les clients pourraient exiger une authenticité prouvable du modèle. Si vous réalisez des audits ou des évaluations de sécurité de modèles, il vaut déjà la peine d'examiner comment les spécifications Lean aident à vérifier des affirmations. Pour les autres, la conclusion est plus simple : l'inférence vérifiable est passée de la théorie à un prototype fonctionnel en code ouvert, que l'on peut essayer et améliorer.