Une preuve cryptographique pour vérifier quel modèle d'IA a réellement répondu

Avec FlashProve, Anthropic explore une méthode pour certifier l'origine des réponses d'une IA sans révéler ses paramètres, grâce aux preuves cryptographiques.

Rien ne garantit aujourd'hui à un utilisateur que le modèle d'intelligence artificielle auquel il pense s'adresser est bien celui qui produit sa réponse. Un intermédiaire pourrait lui substituer un modèle moins coûteux, un serveur compromis pourrait modifier les résultats, et même un auditeur indépendant ne disposerait pas nécessairement des moyens de vérifier l'identité du système utilisé. Cette difficulté prend une autre dimension à mesure que les modèles interviennent dans des opérations sensibles, de la cybersécurité à l'évaluation de systèmes soumis à des obligations réglementaires.

Une équipe de recherche d'Anthropic, associée à des spécialistes de l'EPFL, du MIT et de Succinct, a développé FlashProve, un prototype capable de produire une preuve cryptographique reliant une réponse aux paramètres d'un modèle précis. Présenté dans une publication consacrée à l'inférence vérifiable, ce dispositif utilise des preuves à divulgation nulle de connaissance, appelées zkSNARKs, pour établir qu'un calcul a été effectué correctement sans exposer les informations confidentielles qui ont servi à le réaliser. Prouver l'origine d'une réponse sans accéder au modèle

Le fonctionnement de FlashProve repose sur deux étapes. Avant toute requête, le fournisseur publie un engagement cryptographique, une sorte d'empreinte associée à un ensemble précis de paramètres du modèle. Ces paramètres restent secrets, mais l'engagement sert de référence pour vérifier les réponses produites ultérieurement.

Lorsqu'une requête est soumise, le fournisseur peut générer un certificat démontrant que les tokens vérifiés correspondent au résultat du modèle associé à cette empreinte. L'utilisateur, ou un auditeur tiers, contrôle alors la validité de la preuve sans télécharger les paramètres ni exécuter lui-même le modèle. La vérification nécessite ainsi beaucoup moins de ressources que le calcul initial.

Cette méthode ne certifie pas qu'une réponse est vraie, pertinente ou exempte de biais. Elle établit une propriété différente : les éléments vérifiés proviennent bien d'un calcul défini, effectué avec les paramètres auxquels le fournisseur s'est engagé. La distinction est importante pour les services qui proposent plusieurs modèles derrière une même interface, mais aussi pour les entreprises souhaitant attester qu'une analyse a réellement été effectuée par un système donné. Un modèle de 400 milliards de paramètres vérifié sur une seule H100

Les chercheurs ont expérimenté leur système sur Llama 4 Maverick, un modèle à mélange d'experts de 400 milliards de paramètres, dont environ 17 milliards sont mobilisés pour chaque token. Les tests utilisent une version quantifiée sur quatre bits et un dispositif de preuve faisant intervenir une seule carte NVIDIA H100, accompagnée de 24 cœurs CPU.

Dans cette configuration, FlashProve traite environ 110 tokens de contexte par seconde lors de la génération des preuves, sur un lot de 24 requêtes. Chacune porte sur une fenêtre de 1 024 tokens et la preuve vérifie un token sélectionné par requête. Le chiffre de 110 tokens par seconde ne correspond donc pas à une génération de texte vérifié à cette cadence.

Chaque certificat représente environ 18,78 Mo. Sa vérification prend 17 secondes avec 24 threads CPU, ou 21 secondes sur un seul thread, sans nécessiter de carte graphique. La préparation initiale de l'engagement cryptographique demande environ 39 minutes, mais cette opération peut ensuite servir à quelque 16 millions de requêtes avant d'être renouvelée.

Le coût informatique reste néanmoins important. D'après les mesures détaillées par Anthropic, la production des preuves mobilise entre 70 et 95 fois davantage de temps GPU que l'exécution de référence avec vLLM, selon la charge testée. La comparaison porte sur des configurations matérielles et numériques différentes et ne constitue pas un multiplicateur universel applicable à tous les modèles. Des garanties mathématiques examinées avec Lean

Une difficulté supplémentaire apparaît lorsqu'il faut vérifier le système chargé de produire et de contrôler ces certificats. Une erreur dans son implémentation pourrait fragiliser les garanties de sécurité, même si le principe cryptographique est solide.

Pour limiter ce risque, les chercheurs ont utilisé Lean, un assistant de preuve formelle permettant de représenter des propriétés mathématiques et d'en vérifier la démonstration. Trois garanties principales sont étudiées : l'acceptation des preuves honnêtes, le rejet des preuves frauduleuses sauf probabilité négligeable, et l'absence de divulgation des paramètres secrets par le certificat.

Le projet comprend un vérificateur rapide écrit en C++ et une seconde implémentation en Lean, plus lente, mais reliée aux propriétés formellement démontrées. Cette séparation facilite l'examen des fondements mathématiques tout en conservant un outil utilisable pour les expérimentations.

Elle ne supprime cependant pas tous les risques. Les chercheurs reconnaissent que la correspondance entre les propriétés formalisées, la documentation et l'intégralité du code exécutable n'est pas elle-même entièrement garantie. Le dispositif protège les paramètres du modèle, mais pas son architecture, et certaines informations pourraient théoriquement être révélées par des canaux indirects, comme l'observation des temps de calcul. Une piste pour contrôler les fournisseurs et les modèles autorisés

L'inférence vérifiable pourrait répondre à plusieurs problèmes rencontrés par les organisations qui utilisent des modèles externes. Un client passant par un service de routage aurait la possibilité de contrôler qu'il reçoit bien les réponses du modèle prévu, tandis qu'un évaluateur indépendant pourrait vérifier que le système testé correspond à celui réellement proposé aux utilisateurs.

Les applications envisagées concernent aussi la surveillance des modèles les plus avancés. Une autorité pourrait exiger des preuves attestant que seules certaines versions autorisées sont utilisées, sans avoir accès à leurs