Tech Teardown 041 | FlashProve : l'inférence IA sous preuves ZK

Contexte et phénomènes : vous ne savez pas si la réponse provient bien du modèle que vous avez choisi

Le 4 novembre 2026, Anthropic a publié un blog de recherche intitulé « Progress on provable inference for large language models », dans lequel il a dévoilé un système appelé FlashProve, et a également open-sourced cinq fichiers : le blog lui-même, les rapports techniques, les spécifications des protocoles, le code exécutable (un probateur et deux verificateurs), la preuve Lean et une plateforme de visualisation interactive des théorèmes. Le code, les preuves et les documents sont tous sous la licence Apache 2.0. Le dépôt associé anthropics/FlashProve a été créé le 30 octobre 2026, et au 5 novembre, il avait reçu 781★. Le fichier de version indiquait 0.16.0 ; l’entrée HN du blog était de 155▲ et il y avait 77 commentaires.

La question posée par le blog est directe : lorsque les utilisateurs demandent à un modèle une réponse, il n’y a aucun moyen de vérifier que la réponse provient bien du modèle choisi. Le service de routage pourrait, pour économiser, remplacer le modèle utilisé par un modèle moins cher, et les attaquants pourraient modifier le flux des tokens ; d’après la qualité de la réponse, on peut déduire son fiabilité, mais même les meilleures réponses ne prouvent pas l’origine des utilisateurs. Les agences d’évaluation indépendantes doivent savoir que l’on évalue le modèle en cours d’utilisation en ligne, et les utilisateurs qui utilisent un service de routage tiers doivent vérifier que le token provient bien du modèle acheté par eux-mêmes.

Le deuxième point de dissection concerne la composition de l’auteur et le rôle de Claude dans cette affaire. Le blog est signé par une combinaison d’académiques et d’entrepreneurs en sécurité informatique : deux personnes d’Anthropic, trois personnes de l’EPFL, ainsi que des chercheurs issus de MIT, StarkWare, Succinct et RESI. Plus frappant encore, le blog explique lui-même : « Claude a amélioré le zkSNARK utilisé pour la reasoning », permettant de créer un système beaucoup plus rapide que les systèmes open-sources existants ; le document des spécifications des protocoles dans les cinq fichiers indique clairement que ce sont Claude qui l’ont écrit. Anthropic souligne également les risques et les stratégies associées à cette approche : Claude est doué pour l’optimisation, mais les décisions dans de grands systèmes complexes sont souvent difficiles à évaluer. La stratégie consiste à écrire les garanties de sécurité en termes de preuve Lean, qui peuvent être auditées.

La première ligne du README décrit l’identité de l’auteur : « Fichiers de recherche : sans maintenance, sans contributions ». Le blog précise également que c’est un progrès intermédiaire, pas une fin de la recherche, et que l’objectif est de permettre aux autres d’apporter des améliorations.

Architecture et principes technologiques : trois étapes – commit, prove, verify

Le noyau de FlashProve est la reasoning probante basée sur zkSNARK, avec un mécanisme en trois étapes (selon le README). La première étape, commit : le service proposateur publie un ID de promesse, lié à un ensemble de poids secrets. Les valeurs publiques de tous les poids dépendants sont masquées, sauf pour la liste déclarée dans docs/what-is-not-hidden.md ; l’objectif du design est clairement défini : cacher les poids, mais pas l’architecture. La deuxième étape, prove : chaque réponse est probée par la GPU du service proposateur. La troisième étape, verify : toute personne peut utiliser le verificateur C++ cp_verify pour vérifier en quelques secondes sur une CPU ordinaire que « cette réponse provient bien du modèle promis », sans besoin de poids.

La partie Lean constitue l’autre axe central du repository. Les fichiers clonés localement comptent 30,902 pièces, dont 29,563 fichiers .lean et seulement 185 fichiers .py, avec une taille totale de 723MB. Les dossiers contiennent prover, verifier, lean, paper (rapports techniques en PDF), docs (19 articles), guide (8 articles), tests, toy, scales, etc. Le fichier lean/THEOREM.md liste six théorèmes, tous visant le même set de committer, prover et verifier, et étant valables pour chaque configuration publique : sound (la probabilité pour l’entraîneur de tromper le verificateur sous q fois de recherche de hachage ne dépasse pas environ q/2^124 + 2^-101 ; l’auteur note en note explicative « ceci est une limite, pas un niveau de sécurité ») ; soundAndBinding (personne ne peut transformer la promesse en un autre ensemble de poids, sauf avec une probabilité d’environ q/2^124 + 2^-100) ; completeOnCanServe (la probabilité pour une demande de service d’être rejetée par erreur par une preuve honnête ne dépasse pas 2^-40) ; zeroKnowledgeOnCanServe (la divulgation de la limite avec 2^64 fois de recherche de hachage et 688,127 réponses ne dépasse pas 2^-154, le simulateur ne peut pas obtenir les poids) ; refusedHandsOutNoProof (une demande rejetée ne peut donner qu’une preuve vide, mais « être correctement rejetée » n’est pas inclus dans la preuve) ; repliesFit (le compte de cohérence entre 688,127 réponses et le nombre de tableaux).

Deux limites méritent d’être mentionnées, toutes deux déclarées par le repository. Premièrement, les six théorèmes exigent une « correspondance exacte », mais le verificateur ne vérifie pas ce point : si le serviceur change la stratégie de fichiers publiés après avoir reçu la demande, le théorème ne s’applique pas. Deuxièmement, l’ensemble des tests utilise des poids synthétiques, comme indiqué dans le fichier SUITE.md : les tests réussis ne montrent que que le programme donne les réponses attendues aux entrées synthétiques, sans fournir plus d’informations sur la fiabilité et l’anonymat.

Données clés : 110 tok/s, coût de 93 fois et six limites de probabilité

Les chiffres de performance proviennent tous du fichier guide/performance.md et README du repository, selon les déclarations officielles. Aucune reproduction indépendante n’a été réalisée pour l’instant.

Objet de test : Llama 4 Maverick en taille complète (400B paramètres MoE), utilisant la conversion 4-bit publiée par un tiers (téléchargement de 232GB), fenêtre de contexte de 1,024-token, et une seule machine H100 de 80GB. Vitesse : une commande pré-fill en 24 heures donne 111.23±0.92 tokens/s, le README indique environ 110 ; une commande unique donne seulement 17.41 ; une commande de 64 donne 123.31, mais le repository note que 80GB ne permet pas de faire 64 commandes de manière fiable, avec une mémoire vidéo atteignant 80,629/81,559 MiB, et toutes les tentatives de CUDA avec 8 poids ont échoué.

Le coût est également une déclaration du repository : par GPU, c’est 93 fois plus lent que le pré-fill natif de vLLM (pour les charges maximales), et 71.4 fois plus lent que la commande de 24 de vLLM. De plus, ceci est « calculé, dans le meilleur cas », sans compter le temps de démarrage et de promesse, et l’ordinateur de base utilise toujours 8×H100 pour exécuter FP8.

Prouve et volume de stockage : Une preuve unique mesure en moyenne 18,78 MB ; le client télécharge une fois par engagement 6,24 MB ; le fournisseur doit conserver 2,15 GB. L’engagement dure environ 39 minutes, et un engagement peut être utilisé plusieurs fois ; le serveur du fournisseur doit disposer de 330 GB de mémoire et de 245 GB de disque. Le coût de la vérification est le chiffre le plus asymétrique dans tout le système : cp_verify en un thread dure environ 21 secondes, nécessite jusqu’à 3,53 GB de mémoire, sans GPU ; la version Lean du « verificateur de validité » dure environ 24 minutes pour une preuve complète, nécessite jusqu’à 14,13 GB de mémoire.

Le dépôt explique assez honnêtement ses points faibles : le démarrage prend de 68 à 79 secondes ; après avoir réparti les coûts d’engagement sur les 1 000 premières requêtes, la vitesse de stabilité est de 88,81 tok/s, ne répondant pas à l’objectif fixé de 100 tok/s, et performance.md admet directement que cela ne suffit pas.

Impact et signification : transformer « quel modèle dit » en une propriété vérifiable

Premièrement, dans les scénarios de conformité et d’audit. Le blog indique clairement que zkSNARK peut servir comme outil pour vérifier la conformité des exigences AI : les autorités exigent que les fournisseurs fournissent des certificats couvrant une certaine période de requêtes de raisonnement, et le fournisseur ne peut pas fabriquer de faux certificats à moins que son hardware ne fonctionne réellement avec le modèle annoncé, tout en ne pouvant pas obtenir les informations sur les droits exclusifs. Un commentaire très approuvé sur HN exprime la même idée : dans les audits de conformité, les chaînes d’agencement, et les scénarios réglementaires, « quel modèle dit » est en soi une propriété clé.

Deuxièmement, problème de confiance dans le routage agrégé. Un commentaire souligne que des agrégateurs comme OpenRouter route les requêtes vers d’autres modèles, et ce mécanisme peut être utilisé ; un autre commentaire fournit des scénarios de fraude plus spécifiques, où certains revendeurs de Claude promettent l’accès à des modèles réellement substitués, ce que la protection contre le raisonnement peut prouver. D’autres mentionnent des rumeurs selon lesquelles certains modèles du même nom sur certains serveurs fonctionnent nettement moins bien, et qu’ils utilisent une version quantitative non publiée (le commentateur considère cela comme une rumeur), demandant si ce mécanisme peut détecter cela.

Troisièmement, les modèles de poids open-source peuvent également s’en servir pour se justifier. Un commentaire très approuvé ayant lu les documents du dépôt indique : en utilisant des poids publics pour faire des engagements et en publiant des graines, n’importe qui peut récalculer les engagements à partir des fichiers de Hugging Face, pour vérifier si le fournisseur exécute bien le point de contrôle et la largeur de bits quantitatifs annoncés. Cela signifie que ce mécanisme ne sert pas seulement les fabricants fermés, mais offre également à la communauté un outil de self-audit.

Quatrièmement, la méthodologie de Claude pour écrire du code cryptographique et Lean pour se protéger peut être aussi importante que le système lui-même. Transformer « les décisions AI difficiles à évaluer » en une proposition de niveau supérieur vérifiable dans un langage formel, permettant aux machines de prouver que le code écrit par les humains est révisé, c’est un paradigme de conception reproductible lorsque l’IA participe au développement d’infrastructures clés (c’est mon jugement).

Controverses et risques : Une action de PR ou une remise à neuf dans le vide ?

Le commentaire le plus virulent dans la section HN est ironique. Le commentaire le plus approuvé considère que c’est une action de PR, avec des internautes rapportant des articles précédents, affirmant qu’une même entreprise a déjà fait la une pour avoir routé silencieusement des requêtes ML vers des modèles moins performants (le commentateur l’affirme, sans vérification indépendante). Mais un autre commentaire très approuvé réfute : le subterfuge des modèles est justement la plainte la plus courante des utilisateurs, et il n’y avait aucun mécanisme de vérification auparavant. Si ce système peut être mis en œuvre, son importance est grande.

La controverse sur la valeur s’approfondit. Certains estiment que cette fonctionnalité prouve une « exigence de base » : cependant, elle ne fournit pas beaucoup d’informations utiles, à part le fait que le résultat n’a pas été remplacé par un modèle moins cher ou qu’il n’y a pas de tiers intermédiaires. D’autres pensaient initialement qu’il fallait prouver « la justesse du résultat », mais ils se rendent compte que cela ne prouve que « le modèle utilisé ». Ils affirment que si l’on ne fait pas confiance aux prestataires de services, le jeu est déjà perdu. La réponse de l’opposition : les clients s’intéressent à la justesse du résultat, tandis que les fabricants se préoccupent du fait que le résultat provienne de leur propre modèle ; ce système résout le problème des derniers. D’autres commentaires prédisent qu’il sera finalement utilisé pour générer du FUD contre les services bon marché (c’est une hypothèse motivée par l’auteur). Mon point de vue : en réalité, les deux parties ne sont pas en conflit. « La justesse du résultat » et « le résultat provenant du modèle annoncé » sont deux questions de vérification indépendantes. La première n’est pas encore résolue, tandis que pour la seconde, il n’y a actuellement qu’une seule voie possible : la cryptographie (c’est mon jugement).

Il y a trois limites claires pour les risques technologiques. Premièrement, le problème de l’exactitude du matchage : six théorèmes exigent que les documents publiés soient exactement conformes aux promesses, mais les vérificateurs ne vérifient pas, et lorsque les prestataires de services changent de stratégie après avoir reçu la demande, cela sort de leur responsabilité. C’est un défaut connu du repository. Deuxièmement, le seuil de déploiement : la stack GPU exige Linux 4.14+ x86-64, une CPU avec extension SHA, une H100 de 80GB, CUDA 13.2 Update 2 (les outils ne prennent pas en charge les mises à jour), et pour la version modèle réelle, il faut 330GB de mémoire et 245GB de disque, ce qui est difficilement accessible pour les individus ou les petites équipes. Troisièmement, toutes les données de performance sont rapportées par l’équipe officielle, sans reprise par des tiers. Une réduction de 93 fois signifie que, à court terme, il ressemble davantage à un outil de vérification qu’à une fonctionnalité productive constante.

Conclusion et perspectives : le repository est lui-même un deuxième expérience

Le point principal est : FlashProve utilise zkSNARK pour transformer « la réponse provenant du poids annoncé » en une question que n’importe qui peut résoudre en quelques dizaines de secondes sur une CPU ordinaire, mais au prix d’un déploiement avec 70-95 fois plus de temps GPU et un niveau de mémoire de 330GB. En même temps, il utilise 29 563 fichiers Lean pour traduire la question « La cryptographie écrite par Claude est-elle fiable ? » en six théorèmes vérifiables.

Un phénomène digne d’attention : le README contient une section « Construit pour être exécuté par un agent », où l’auteur prévoit que les lecteurs orienteront leur agent de codage vers ce repository, avec un texte d’instruction directement imprimable. La voie de vérification est divisée en quatre parties selon la puissance : Voie 1 nécessite Linux et g++13, 2GB de mémoire, et peut être construit en 1-2 minutes avec une vérification en 2 secondes des preuves existantes ; Voie 2 nécessite environ 1 minute pour exécuter la vérification sur CPU ; la petite modèle synthétique de huit couches nécessite toute la stack H100, et le déploiement prend environ 29 minutes ; Voie 4 est la version réelle de Llama 4 Maverick, qui prend des heures. La posture de sécurité est également adaptée : l’accès root/sudo est interdit, et Landlock est utilisé dans le sandbox. Ces designs constituent eux-mêmes une expérience pour « assurer la sécurité du agent dans un repository inconnu ». Le premier lecteur des documents du repository pourrait être en train de passer de l’être humain à l’agent.

Deux choses méritent notre attention à l’avenir. Premièrement, la déclaration README indique qu’il n’est pas maintenu ni accepte de contributions ; le blog appelle les gens à améliorer le système. Il est probable que les cinq composants de l’licence Apache 2.0 soient poursuivis par le monde académique et le milieu des startups en cryptographie. La question de savoir si une implémentation indépendante peut être créée est une vérification plus difficile qu’une simple mise en avant. Deuxièmement, il convient de voir si les limites sont correctement corrigées, car cela détermine si ce mécanisme peut passer des scénarios d’audit à des processus de production réguliers.

Ma conclusion en une phrase : FlashProve mérite d’être analysé, non pas parce qu’il a déjà résolu le problème de la confiance dans l’inférence (il ne l’a pas, et les développeurs eux-mêmes l’admettent comme étant seulement un progrès intermédiaire), mais parce qu’il a transformé deux aspects qui auparavant ne pouvaient être assurés que par des promesses verbales en propositions prouvables : l’identité des modèles et la validité du code cryptographique écrit par l’IA. Le premier concerne le fondement de la confiance dans le marché de l’inférence, le second concerne les méthodes de garantie de qualité à l’ère de la programmation IA.

Sources de référence

• Blog de recherche d’Anthropic « Progress on provable inference for large language models » : anthropic.com/research/provable-inference (publié le 2026-11-04 ; les affirmations relatives à Claude sont toutes basées sur les descriptions du blog).
• Article sur HN : story 50368626 (155 ▲ / 77 commentaires, snapshot du 2026-11-05).
• Repo : github.com/anthropics/FlashProve (781★ / Apache 2.0 / créé le 2026-10-30 / VERSION 0.16.0, snapshot du 2026-11-05).
• Vérification de clone local (testé le 2026-11-05, aucun code du repo n’a été exécuté) : README.md, guide/performance.md, lean/THEOREM.md, SUITE.md, docs/, AGENTS.md ; 30,902 fichiers / 723MB selon les statistiques locales.
• Banque de commentaires sur HN : hn-provable.json (47 articles de preuve, le texte intégral a été cité sans citation directe).

Signé : Yongliang