FlashProve : Anthropic veut prouver mathématiquement quel modèle d’IA a produit une réponse

Quand on interroge un assistant d’IA, on fait confiance au fournisseur pour utiliser le modèle annoncé. Mais rien ne le garantit : un service intermédiaire pourrait substituer un modèle moins cher pour réduire ses coûts, ou un pirate modifier les réponses en chemin. Le 2 novembre 2026, Anthropic a publié FlashProve, un prototype de recherche qui permet de prouver, grâce à la cryptographie, qu’une réponse a bien été produite par un modèle donné, sans révéler ses secrets. Une avancée technique qui pourrait servir autant aux utilisateurs qu’aux régulateurs.

Le problème : rien ne prouve quel modèle a répondu

Anthropic part d’une comparaison simple. Quand on parle à un ami en personne, on dispose de nombreux moyens de savoir que c’est bien lui. Face à un modèle d’IA, on n’en a presque aucun. Juger à la seule qualité de la réponse ne suffit pas.

L’entreprise cite plusieurs situations où une garantie serait utile :

• les évaluateurs indépendants qui testent un modèle avant et après sa sortie doivent être sûrs que le modèle testé est bien celui qui est servi aux utilisateurs ;
• les clients qui passent par un service intermédiaire, un routeur qui distribue les requêtes vers plusieurs fournisseurs, veulent l’assurance d’obtenir le modèle qu’ils paient ;
• en cas d'attaque, un pirate qui modifie le flux de réponses en se faisant passer pour un modèle ne peut pas être détecté à partir du seul texte.

La difficulté est double. Les poids des modèles de pointe, c’est-à-dire les paramètres qui les définissent, sont secrets. Et même en les connaissant, vérifier une réponse supposerait de refaire tourner le modèle, ce qui demande des moyens hors de portée d’un utilisateur ordinaire.

La solution : une preuve à divulgation nulle

FlashProve s’appuie sur une famille d’outils cryptographiques appelés zkSNARK. Le principe : le fournisseur joint à chaque réponse une courte preuve, de quelques mégaoctets, que l’utilisateur peut vérifier rapidement. Si la réponse ne provient pas du modèle annoncé, la vérification échoue. La preuve est dite à divulgation nulle de connaissance : elle ne révèle rien des poids du modèle.

Concrètement, le fournisseur s’engage d’abord publiquement sur un modèle précis, puis démontre pour chaque réponse qu’elle a été produite par ce modèle. Selon Anthropic, Claude a contribué de manière importante à la conception du système, en trouvant de nouvelles façons d’appliquer des outils cryptographiques récents.

Des performances encore coûteuses

Anthropic a testé FlashProve sur Llama 4 Maverick, un modèle ouvert de Meta de 400 milliards de paramètres. Les résultats annoncés :

Ce surcoût reste élevé, mais Anthropic affirme que les systèmes libres existants étaient plus lents de plusieurs ordres de grandeur. Produire des preuves pour chaque réponse d’un service grand public n’est donc pas encore envisageable à grande échelle, mais l’écart se réduit.

Des garanties vérifiées formellement

Pour éviter qu’une erreur ne se glisse dans un système aussi complexe, Anthropic a accompagné le prototype de preuves formelles écrites dans Lean, un langage qui permet de vérifier mathématiquement l’exactitude d’un raisonnement. L’entreprise reconnaît que Claude est très bon pour optimiser, mais prend parfois des décisions difficiles à évaluer : ces preuves formelles permettent d’auditer les garanties de sécurité revendiquées.

Anthropic publie cinq éléments : un billet de présentation, un rapport technique, une spécification du protocole rédigée par Claude, le code exécutable avec un générateur de preuves et deux vérificateurs, ainsi que les preuves formelles. Le tout est diffusé sous la licence libre Apache 2.0. Le projet associe des chercheurs d’Anthropic et de plusieurs institutions, dont l’École polytechnique fédérale de Lausanne et le MIT.

À quoi cela pourrait servir

Anthropic décrit plusieurs usages possibles :

• Contrôler le rythme du développement de l’IA : un régulateur pourrait vérifier qu’un fournisseur utilise bien son matériel pour servir un modèle déclaré, et non pour entraîner en secret un modèle plus puissant, même si cela ne prouve pas l’absence d’entraînement en parallèle.
• Détecter une falsification : un client pourrait repérer qu’une réponse a été modifiée par un attaquant.
• Prouver la provenance d’un texte : une entreprise pourrait démontrer qu’une analyse a bien été réalisée par un modèle spécialisé, par exemple un audit de sécurité.
• Garantir l’usage de modèles autorisés : si une réglementation impose de ne servir que des modèles jugés sûrs, une preuve pourrait l’attester pour chaque réponse.

Ces applications rejoignent les préoccupations des régulateurs, qui cherchent des moyens de vérifier les engagements des fournisseurs, à l’heure où le règlement européen sur l’IA impose des obligations aux fournisseurs de grands modèles.

Logiciel ou matériel : deux approches complémentaires

FlashProve n’est pas la seule piste pour vérifier l’origine d’une réponse. De nombreux travaux s’appuient sur des environnements d’exécution de confiance, des zones protégées intégrées aux processeurs, qui attestent qu’un calcul s’est déroulé comme prévu. Leur sécurité repose sur la capacité du fabricant à produire un matériel inviolable.

L’approche d’Anthropic est purement logicielle : sa sécurité repose sur la difficulté de certains problèmes mathématiques. Même si le matériel, le système d’exploitation ou l’infrastructure d’un fournisseur étaient compromis, un attaquant ne pourrait pas produire une preuve valide pour une fausse réponse sans résoudre un problème jugé impossible à calculer. Anthropic estime que les deux approches, matérielle et cryptographique, offrent des garanties différentes et auront chacune leur rôle.

Ce que cela pourrait changer pour les utilisateurs

À terme, ce type de preuve pourrait apparaître dans les services qui donnent accès à plusieurs modèles, où l’utilisateur choisit un modèle sans pouvoir vérifier qu’il est réellement servi. Un indicateur de vérification, comparable au cadenas des sites sécurisés, pourrait signaler qu’une réponse est accompagnée d’une preuve valide. Les entreprises qui paient pour un modèle haut de gamme auraient ainsi la garantie de ne pas recevoir les réponses d’un modèle moins coûteux.

Les limites du prototype

Anthropic présente FlashProve comme un travail intermédiaire, partagé pour que d’autres l’améliorent. Plusieurs limites sont reconnues : rien ne garantit que le code rapide, le rapport et les preuves formelles correspondent parfaitement ; la preuve porte sur une version en nombres entiers du modèle et sur un mode de génération déterministe, alors que les services réels utilisent souvent des calculs en virgule flottante et une part de hasard dans le choix des mots ; et le système suppose une architecture précise, dite à mélange d’experts. Masquer l’architecture du modèle ne fait pas partie des objectifs.

Pour les utilisateurs, la promesse reste lointaine. Mais la démarche ouvre une voie intéressante pour la transparence de l’IA : passer d’une confiance déclarée à une confiance vérifiable. Elle illustre aussi comment les modèles d’IA contribuent désormais eux-mêmes à la recherche, un sujet sur lequel Anthropic vient de publier un avertissement dans son prospectus boursier.