Anthropic lance FlashProve pour produire des preuves cryptographiques d’inférence par IA

Anthropic a lancé FlashProve le 2 novembre 2026 : un prototype de recherche open source qui recourt à des preuves cryptographiques pour montrer qu’une réponse générée par un modèle de langage provient de poids associés à un engagement, sans les révéler. L’entreprise a indiqué que, pour Meta’s Llama 4 Maverick, la génération des preuves atteignait 110 jetons par seconde.

Ce travail vise à combler une lacune dans la vérification des systèmes d’IA hébergés. Une réponse de grande qualité ne permet pas de savoir quel modèle l’a produite : un service de routage pourrait en substituer un autre, un évaluateur pourrait recevoir un modèle différent de celui prévu pour le test, ou un attaquant pourrait modifier le flux de jetons. Pour les utilisateurs, relancer le modèle afin de vérifier le résultat est peu réaliste lorsque les poids sont privés et que le matériel nécessaire est important.

Lier les réponses à des poids cachés

FlashProve utilise un argument succinct de connaissance à divulgation nulle, ou zkSNARK, dans une architecture entièrement logicielle qui ne dépend pas de matériel de confiance. Lors d’une phase hors ligne, le fournisseur publie un court engagement qui identifie un ensemble précis de poids tout en les gardant secrets. Pour chaque paire complète de requête et de réponse, le système produit une preuve que les jetons générés sont bien la sortie du modèle associé à l’engagement. Toute personne disposant de l’engagement, de la requête et de la réponse peut vérifier la preuve sans avoir accès aux poids.

Les propriétés visées sont la complétude, la solidité, la divulgation nulle de connaissance et la concision. Une preuve honnête devrait être acceptée, tandis que certifier une affirmation fausse devrait nécessiter de briser des hypothèses cryptographiques largement considérées comme fiables. La vérification d’une preuve ne devrait révéler ni les poids ni les valeurs intermédiaires du calcul. La conception dissimule également quels sous-réseaux du mélange d’experts ont été exécutés pour chaque jeton, bien que l’architecture du modèle elle-même reste visible.

L’implémentation tire parti de l’architecture à mélange d’experts de Maverick. La charge de travail du prouveur évolue en fonction des quelque 17 milliards de paramètres actifs pour un jeton, plutôt que des 400 milliards au total, tout en dissimulant les choix d’experts. Les poids segmentés sont transférés depuis la mémoire hôte, ce qui permet au prouveur de fonctionner sur un seul GPU de 80 Go, accompagné d’environ 290 Go de mémoire hôte.

Anthropic décrit des utilisations possibles pour les contrôles d’intégrité destinés aux clients, les évaluations indépendantes, les outils réglementaires et l’application des exigences relatives aux modèles approuvés. Les attestations d’inférence pourraient certifier que les requêtes ont été traitées par le modèle annoncé, mais elles ne prouveraient pas que le même matériel n’a pas également servi à entraîner un autre modèle. Cette distinction limite ce que ces attestations pourraient démontrer au sujet des exigences de conformité fondées sur l’utilisation de la capacité de calcul.

Performances des preuves et surcoût de l’inférence

L’évaluation d’Anthropic a utilisé une conversion publique du modèle en 4 bits. Un serveur équipé d’un H100 et de 24 cœurs de processeur a produit des preuves pour un lot de 24 requêtes en environ 223 secondes, avec une preuve de 18,78 Mo par requête. La phase d’engagement hors ligne a pris environ 39 minutes.

Du côté de la vérification, le client télécharge un engagement d’environ 6,5 Mo et vérifie les preuves sur un processeur, sans GPU. Anthropic a mesuré un temps de vérification de 17 secondes avec 24 threads et de 21 secondes avec un seul thread, y compris les vérifications de la phase hors ligne.

Ces mesures distinguent une vérification réalisée uniquement sur processeur d’une opération de génération de preuves beaucoup plus exigeante. Dans sa comparaison avec l’inférence FP8 sur huit H100 utilisant vLLM, Anthropic a constaté que la génération de preuves nécessitait environ 72 fois plus de temps GPU pour le même lot, et environ 94 fois plus au niveau de charge vLLM le plus élevé testé. Ce débit s’accompagne donc d’un coût substantiel par rapport au service du modèle sans preuves.

Vérification formelle et limites pratiques

Le dépôt FlashProve comprend un prouveur, un vérificateur rapide en C++, un vérificateur plus lent en Lean, des preuves Lean d’énoncés mathématiques de haut niveau ainsi qu’un visualiseur interactif de théorèmes, sous licence Apache 2.0. La version 0.16.0 y est présentée comme un artefact de recherche non maintenu qui n’accepte pas les contributions.

Les travaux en Lean portent sur la complétude, la solidité et la divulgation nulle de connaissance dans le modèle de l’oracle aléatoire. Les énoncés formels doivent encore faire l’objet d’un examen manuel pour établir qu’ils expriment bien les garanties visées. Le vérificateur Lean est formellement relié au théorème de solidité, mais le vérificateur C++ destiné à un usage courant ne bénéficie d’aucune garantie formelle ; sa concordance avec le vérificateur Lean a plutôt été testée.

La documentation du projet sur les limites connues indique que des systèmes d’IA placés sous la direction d’humains ont écrit la quasi-totalité du logiciel, des preuves Lean et de la documentation, et exécuté les tests présentés. Aucun audit de sécurité indépendant n’a été réalisé, et les tests portant sur la dissimulation des poids et les preuves adversariales restent limités.

Les preuves portent sur une version entière exacte des poids et supposent un décodage glouton. L’inférence en virgule flottante ou le décodage par échantillonnage peuvent s’écarter du calcul faisant l’objet de la preuve, et les tests génériques d’erreur ne couvrent pas les requêtes conçues de manière adversariale. Le contexte est limité à 1 024 jetons, tandis que les attaques temporelles et autres attaques par canal auxiliaire ne sont pas couvertes par la garantie. La génération de preuves a posteriori implique également un nouveau calcul, des garanties différées et du non-déterminisme, contrairement à une génération menée en parallèle de l’inférence.

Pour que l’inférence vérifiable devienne un contrôle systématique du trafic traité, les travaux restants portent principalement sur les lacunes mises en évidence par cette version : réduire le coût de génération des preuves, prendre en charge des méthodes de décodage moins restrictives et des contextes plus longs, et rattacher plus solidement l’implémentation rapide au protocole formel.