FlashProve prouve l'origine des réponses des LLM

Ce que FlashProve prouve réellement

Le point essentiel est particulièrement intéressant : FlashProve permet de vérifier qu'une réponse a bien été calculée par le modèle annoncé, avec un jeu de poids fixé à l'avance. Dans les travaux d'Anthropic sur l'inférence prouvable, le système est présenté comme un prototype ouvert pour de grands modèles de langage à architecture mixture-of-experts.

Le fournisseur fixe d'abord le modèle et ses poids par un engagement cryptographique, puis produit une preuve pour une entrée et une sortie données. Un vérificateur indépendant peut confirmer que le calcul est correct sans recevoir les poids propriétaires. L'approche repose sur des preuves à divulgation nulle de connaissance de type zkSNARK.

Lors de la publication, Anthropic annonçait plus de 100 tokens par seconde sur une seule H100 pour Llama 4 Maverick, un modèle de 400 milliards de paramètres quantifié en 4 bits. La preuve d'une requête de 1 024 tokens représentait environ 19 Mo. En revanche, sa génération demandait approximativement 70 à 95 fois plus de temps GPU que le traitement d'une requête comparable avec vLLM.

Ce n'est donc plus une simple idée cryptographique, mais ce n'est pas non plus une coche gratuite à côté de chaque réponse d'API. Le débit paraît convaincant, tandis que la taille des preuves et le calcul supplémentaire deviennent vite problématiques à grande échelle.

La complétude de l'ingénierie est également remarquable. La publication comprend un prover ouvert, un vérificateur C++ rapide, un autre plus lent en Lean, ainsi qu'une formalisation du protocole dans Lean 4. Des preuves formelles sont annoncées pour la complétude, la correction et le zéro-knowledge.

Où s'arrête cette garantie

FlashProve prouve l'origine du calcul, non la qualité de la réponse. Cette distinction est fondamentale : un modèle dangereux ou erroné peut produire un texte dangereux ou faux avec une preuve cryptographique parfaitement valide.

La valeur pratique reste néanmoins importante. Un auditeur pourra vérifier que la production exécute bien le modèle évalué ; il sera plus difficile pour un opérateur de remplacer discrètement les poids ; et un système en aval pourra rejeter les réponses sans preuve provenant d'un modèle autorisé.

Les trois principaux goulets d'étranglement sont le coût du prover, la taille de la preuve et la latence de la vérification indépendante. L'asymétrie est particulièrement intéressante : produire une preuve exige d'importantes ressources GPU, alors que sa vérification fonctionne sur des CPU ordinaires. L'audit externe devient ainsi plus réaliste, même si la génération continue de preuves reste coûteuse.

FlashProve ne résout pas l'alignement, mais réduit un écart gênant entre une promesse et son déploiement réel. La question « est-ce bien ce modèle qui a répondu ? » peut désormais être séparée de la question beaucoup plus difficile : « peut-on faire confiance à sa réponse ? ».

Nous avons déjà expliqué comment les métriques IRT peuvent mesurer la fiabilité d'une évaluation fondée sur les LLM. Ce cadre complète les travaux d'Anthropic sur l'inférence prouvable en renforçant les preuves d'évaluation des sorties d'IA.