FlashProve : prouver qu'une réponse vient bien du modèle annoncé

Vous payez pour un modèle précis, par l'intermédiaire d'un fournisseur ou d'un service de routage. Comment savoir qu'un modèle moins coûteux ne lui a pas été substitué, ou que la réponse n'a pas été modifiée en chemin ? Aujourd'hui, on ne peut pas. C'est le problème de l'« inférence prouvable », auquel s'attaque un billet publié le 2 novembre 2026 par l'équipe Frontier Red Team d'Anthropic, avec des chercheurs de l'EPFL et du MIT.

Le principe

FlashProve fonctionne en deux temps.

• Une fois par modèle, l'opérateur publie un « engagement » : une empreinte cryptographique des poids du modèle, qui ne les révèle pas.
• Pour chaque requête, il produit une preuve que le modèle ainsi engagé a bien généré les tokens renvoyés.

Le client vérifie cette preuve sur un processeur ordinaire, sans carte graphique et sans connaître les poids. La méthode est purement logicielle : elle ne repose pas sur un matériel de confiance. Le billet indique qu'elle cache les poids et les calculs intermédiaires, mais pas l'architecture du modèle.

Les chiffres annoncés

Ils viennent des auteurs, mesurés sur Llama 4 Maverick, un modèle de 400 milliards de paramètres dont environ 17 milliards sont actifs pour chaque token.

• Préparation : environ 39 minutes, une fois par modèle.
• Production des preuves : un lot de 24 requêtes en 223 secondes environ, soit près de 110 tokens par seconde, sur une carte H100 et 24 cœurs de processeur.
• Taille d'une preuve : 18,78 Mo.
• Vérification : 17 secondes sur 24 fils d'exécution, 21 secondes sur un seul.

Le progrès se lit par rapport aux travaux antérieurs cités dans le billet, dont beaucoup restaient sous un token par seconde. Mais le coût demeure élevé : par carte graphique, prouver un lot prend environ 72 fois plus de temps que le générer avec le moteur vLLM, selon la comparaison des auteurs.

Ce que la preuve ne couvre pas

La liste des limites est longue, et le billet la détaille.

• Le contexte est plafonné à 1 024 tokens par requête, très loin d'une conversation réelle, et chaque preuve porte sur un seul token.
• La preuve vaut pour une version exacte en nombres entiers des poids et pour un décodage déterministe. Une réponse produite avec tirage aléatoire ou en virgule flottante peut diverger.
• Seuls les modèles à « mélange d'experts » sont pris en charge, pas les modèles denses.
• Les preuves sont produites après coup, par lots : la garantie arrive avec retard.
• Les démonstrations formelles, écrites en Lean, portent sur le protocole. Le vérificateur rapide en C++ et le programme qui produit les preuves n'ont pas de garantie formelle.
• La preuve montre qu'une machine sert bien le modèle annoncé, pas qu'elle ne fait rien d'autre.

Les auteurs parlent d'un prototype de recherche. Le code, le rapport technique et les preuves Lean sont publiés sous licence Apache 2.0. Les poids du modèle ne sont pas fournis, et faire tourner l'exemple complet demande une grosse machine à carte graphique.

Notre lecture

Rien ici n'est utilisable tel quel par une petite entreprise aujourd'hui. L'intérêt est ailleurs : le sujet devient un chantier de recherche sérieux, porté par un grand éditeur, avec du code ouvert.

Si vous passez par un intermédiaire pour accéder à des modèles, la question reste entière. En attendant mieux :

• demandez à votre fournisseur quel modèle exact et quelle version il sert, et s'il s'engage par contrat à ne pas le remplacer ;
• conservez un petit jeu de questions de référence et rejouez-le régulièrement pour repérer un changement de comportement ;
• pour les usages sensibles, préférez l'accès direct à l'éditeur ou un modèle que vous hébergez vous-même.

Ce ne sont pas des preuves, seulement des indices. C'est précisément l'écart que ce type de recherche cherche à combler.