Anthropic (États-Unis) publie FlashProve, un système de vérification de l'inférence des grands modèles

fr.wedoany.com Rapport : Le 2 novembre, l'entreprise américaine d'intelligence artificielle Anthropic a publié FlashProve, un résultat de recherche sur l'inférence vérifiable des grands modèles de langage, qui utilise la technologie zkSNARK (argument de connaissance succinct non interactif à divulgation nulle) pour générer des preuves cryptographiques du processus de calcul d'inférence d'un modèle donné. L'équipe de recherche a réalisé ses tests sur le modèle à experts mixtes Llama 4 Maverick, dont le nombre total de paramètres est d'environ 400 milliards, atteignant, dans des conditions de traitement par lots spécifiques, un débit de génération de preuves d'environ 110 tokens par seconde, avec une taille de fichier de preuve d'environ 18,78 mégaoctets, et a rendu publics le rapport technique, la spécification du protocole ainsi que le code associé.

La recherche utilise le modèle Llama 4 Maverick développé par Meta, dont environ 17 milliards de paramètres sont effectivement activés par token. Les tests ont recours aux poids du modèle quantifiés en 4 bits rendus publics, avec une fenêtre de contexte d'inférence unique fixée à 1024 tokens, et établissent une preuve pour le processus de calcul de l'un des tokens générés. Le système lie le résultat de vérification aux paramètres spécifiques du modèle au moyen d'un mécanisme d'engagement sur les poids du modèle.

Le serveur de génération de preuves de FlashProve est équipé d'un GPU NVIDIA H100 et de 24 cœurs CPU. Le processus d'engagement initial des poids du modèle prend environ 39 minutes ; le test en ligne utilise une tâche par lots composée de 24 requêtes, et la génération d'un lot de preuves nécessite environ 223 secondes. Dans ces conditions de test, le système atteint un débit de génération de preuves d'environ 110 tokens par seconde, cet indicateur ne représentant pas la vitesse réelle de génération de texte du modèle.

Chaque fichier de preuve cryptographique a une taille d'environ 18,78 mégaoctets, et les données d'engagement des poids du modèle d'environ 6,5 mégaoctets. L'équipe de recherche estime qu'un seul engagement des poids du modèle peut prendre en charge environ 16 millions de requêtes. Le processus de vérification ne nécessite pas de GPU : dans un environnement CPU à 24 threads, la vérification d'une preuve prend environ 17 secondes ; en mode mono-thread, environ 21 secondes.

L'équipe de recherche a utilisé le framework d'inférence vLLM pour réaliser des tests de performance de référence sur le même modèle. Les résultats montrent que le temps de calcul GPU unitaire nécessaire à la génération de preuves FlashProve est d'environ 70 à 95 fois celui de l'inférence ordinaire du modèle. Le système adopte un traitement par lots et génère les preuves après achèvement de l'inférence ; les données de performance associées proviennent de l'environnement expérimental défini par l'équipe de recherche.

En matière d'allocation des ressources de calcul, FlashProve adopte une approche de traitement segmenté des poids du modèle, stockant les poids du grand modèle dans la mémoire de l'hôte, puis les transférant par lots au GPU selon les tâches de calcul. Le système de test est équipé de 80 Go de mémoire vidéo et d'environ 290 Go de mémoire hôte, et réalise la génération de preuves pour les calculs associés au modèle de 400 milliards de paramètres avec un seul GPU H100.

L'équipe de recherche a utilisé le langage de vérification formelle Lean pour établir des preuves mathématiques vérifiables par ordinateur des propriétés de complétude, de solidité et de divulgation nulle du protocole. Les matériels logiciels publics comprennent le programme de génération de preuves, le vérificateur C++, le vérificateur Lean et les fichiers de preuve formelle associés ; le code est publié sous licence Apache 2.0.

FlashProve se trouve actuellement au stade de prototype de recherche ; le périmètre de vérification testé couvre principalement les contextes jusqu'à 1024 tokens, les calculs sur entiers et les conditions de décodage glouton. La preuve formelle Lean porte sur le modèle mathématique du protocole et n'équivaut pas à une vérification formelle de l'ensemble du code d'exécution haute performance. Le système vérifie la cohérence du processus de calcul et de la provenance de la sortie du modèle spécifié, sans porter sur la détermination de l'exactitude factuelle des réponses du modèle.