🇬🇧 This article is also available in English.

FlashProve : ce qu'une preuve cryptographique d'inférence IA apporte réellement

FlashProve : ce qu'une preuve cryptographique d'inférence IA apporte réellement
🇬🇧 This article is also available in English.
📑 Table of Contents

En bref

FlashProve d’Anthropic est un prototype de recherche open source destiné à prouver qu’un modèle engagé a produit une sortie sans divulguer ses poids. Ses performances rapportées sont prometteuses pour la recherche, mais la vérification reste coûteuse, contrainte et non équivalente à la preuve qu’une réponse est correcte.

Introduction

Un agent peut utiliser un modèle via une API, une passerelle et un routeur sans jamais voir les poids du modèle. Il est donc difficile pour un client ou un évaluateur de vérifier indépendamment si le modèle annoncé a réellement été exécuté. Une réponse plausible ne constitue pas une preuve de provenance : un modèle moins coûteux, un flux de sortie modifié ou une configuration différente peuvent sembler convaincants.

La publication de recherche d’Anthropic du 2 novembre aborde ce problème comme une question cryptographique. FlashProve utilise un système de preuve à divulgation nulle de connaissance pour lier un résultat d’inférence à un engagement préalable sur les poids du modèle. L’entreprise a publié du code et des énoncés formels, et non une garantie de production pour chaque réponse de Claude. (Source : Anthropic — Progress on provable inference for large language models)

D’une promesse de modèle à un énoncé vérifiable

Le fournisseur s’engage d’abord sur un modèle. Ensuite, il fournit une preuve que le calcul associé à une invite et à une sortie est cohérent avec cet engagement. Un vérificateur peut contrôler la preuve sans recevoir les poids privés. L’architecture n’est pas cachée dans la conception actuelle, de sorte que la garantie de confidentialité est plus étroite que la dissimulation de chaque détail d’un modèle.

Cela comble une lacune réelle dans l’infrastructure des agents : un acheteur de benchmarks, un client entreprise ou un auditeur peut se soucier de savoir si un modèle engagé spécifique a été utilisé, et pas seulement si la sortie semble compétente. Mais l’engagement doit encore être relié à une identité de confiance. Si un attaquant peut substituer à la fois le modèle et l’engagement, les mathématiques seules ne peuvent pas indiquer au client quel engagement il devrait croire. La distribution des clés, la gestion des versions et l’identité contractuelle restent des problèmes opérationnels.

Le code, les preuves Lean et la documentation du prototype sont sous licence Apache 2.0. La démonstration d’Anthropic utilise un modèle Llama 4 Maverick quantifié obtenu séparément ; ses poids ne font pas partie de la publication et restent soumis aux conditions de Meta. (Source : Anthropic — Release and licensing)

Le chiffre de débit a besoin de son dénominateur

Anthropic rapporte environ 110 tokens traités par seconde sur un seul H100 pour un modèle mixture-of-experts de 400 milliards de paramètres utilisant des poids en quatre bits, avec une preuve d’environ 19 Mo par requête de 1 024 tokens. L’entreprise estime également un temps GPU d’environ 70 à 95 fois celui d’une inférence vLLM ordinaire dans sa configuration mesurée. Il s’agit de mesures de recherche du fournisseur, et non d’un benchmark de production indépendant. (Source : Anthropic — Executive summary)

Le dénominateur compte. La configuration du rapport technique inclut une preuve d’un token dans une fenêtre de 1 024 tokens ; traiter ces tokens de contexte n’est pas la même chose que prouver chaque token généré à ce rythme. Le rapport évoque séparément un débit de tokens vérifiés plus faible lorsque chaque token de la réponse est vérifié. Comparer un chiffre phare à une API en streaming sans tenir compte des opérations réellement prouvées surestimerait les performances pratiques. (Source : Anthropic — FlashProve technical report)

La fenêtre elle-même constitue une autre contrainte. Un contexte de recherche de 1 024 tokens est petit comparé aux historiques longs et évolutifs de nombreux agents. L’augmenter modifie l’économie de la génération de preuves, de la mémoire et de la vérification. La livraison de la preuve peut également être a posteriori : détecter une réponse substituée après qu’elle a été exploitée est différent de l’empêcher.

Une preuve n’est ni exactitude, ni sécurité, ni confidentialité de l’invite

Une preuve valide est un élément de preuve concernant un calcul spécifié selon les hypothèses du schéma. Elle n’établit pas que la réponse est vraie, qu’un appel d’outil est sûr, ni que le modèle n’a pas été manipulé par un contenu récupéré hostile. Elle ne certifie pas non plus automatiquement la récupération en amont, l’exécution des outils, l’approbation humaine ou l’identité derrière un engagement de modèle publié.

Pour un agent, une chaîne de preuves complète devrait couvrir davantage que l’inférence : les entrées et sorties des outils, les permissions d’exécution, les journaux d’audit et la relation entre une preuve et l’action qu’elle a autorisée. Même alors, la cryptographie peut préserver l’intégrité d’une mauvaise décision. La revue et l’évaluation ne disparaissent pas.

La vérification formelle a également une portée limitée. Anthropic a publié des énoncés Lean et un vérificateur Lean aux côtés du code exécutable ; c’est précieux pour un examen indépendant, mais un énoncé formel portant sur une partie d’un protocole ne doit pas être confondu avec un audit complet de chaque implémentation et dépendance opérationnelle. Le rapport technique note des limites et qualifie la publication de recherche intermédiaire. (Source : Anthropic — Technical report)

Ce que les développeurs doivent surveiller

L’opportunité à court terme est probablement une vérification sélective plutôt que des preuves sur chaque token de chaque conversation. Des évaluations à forte valeur ou des sorties contestées peuvent justifier un calcul supplémentaire et un délai de vérification avant que les charges de travail interactives ordinaires ne le fassent. Les développeurs devraient exiger l’engagement de modèle précis, le format numérique, le contexte pris en charge, les tokens réellement couverts, la taille de la preuve et le temps de vérification, plutôt que d’accepter un seul chiffre de débit.

Une reproduction indépendante est tout aussi importante. Une implémentation ouverte la rend possible ; elle n’établit pas en soi que les performances, les hypothèses cryptographiques ou l’intégration sont prêtes pour la production. FlashProve se comprend mieux comme une infrastructure pour un avenir auditable, et non comme un label d’authenticité clé en main aujourd’hui.

FAQ

FlashProve révèle-t-il les poids ?

La conception vise à masquer les poids engagés ; Anthropic indique que l’architecture n’est pas masquée.

Une preuve valide signifie-t-elle que la réponse est correcte ?

Non. Elle concerne le calcul de modèle spécifié, et non l’exactitude factuelle ou la sécurité d’une action en aval.

Le prototype est-il prêt pour toutes les charges de travail des agents ?

Cela n’est pas établi. La démonstration publiée a un contexte court et un surcoût de preuve rapporté substantiel.

Le code est-il open source ?

Le code, les preuves Lean et la documentation publiés sont sous Apache 2.0 ; les poids du modèle utilisés dans l’exemple ont des conditions distinctes.

Pour aller plus loin

— The Agent Report