FlashProve : ce que la preuve laisse au produit

Une réponse peut venir du modèle payé et rester fausse. Une preuve cryptographique peut rendre l'origine du calcul vérifiable sans décider de la vérité du texte. FlashProve, prototype de recherche d'Anthropic, vaut la lecture pour les frontières précises de sa documentation.

Cet examen des sources date du 5 novembre 2026. Je n'ai ni compilé le vérificateur, ni exécuté une preuve, ni loué de GPU. Le dépôt se présente comme un artefact de recherche non maintenu, sans contributions acceptées. Je ne le choisirais pas comme dépendance de production accompagnée.

Quel modèle l'engagement identifie-t-il ?

L'annonce de recherche décrit une preuve d'inférence sans révéler les poids. Le fournisseur publie un engagement envers un ensemble de poids ; un GPU produit la preuve et un CPU la vérifie contre la requête et l'engagement attendus.

L'identité de cet engagement doit provenir d'une source de confiance. Le guide des limites précise qu'un fournisseur peut choisir n'importe quel modèle, même petit ou dégénéré. Une preuve liée à un engagement arbitraire n'établit pas le nom commercial attendu par le client.

La couverture compte aussi : seuls les emplacements de sortie désignés sont vérifiés. Une réponse raccourcie peut être acceptée comme plus courte. Le consommateur doit vérifier la plage prévue et la fin de réponse. La preuve ne nomme pas intrinsèquement un client ou une heure ; le service doit assurer cette liaison.

Lire la politique d'acceptation

L'égalité exacte concerne les tokens du modèle entier défini. La politique plus souple clipped gap accepte des coûts de tokens dans certaines limites. Elle n'établit pas que chaque token est le choix exact du modèle.

Une acceptation exacte et WITHIN LIMITS peuvent toutes deux retourner zéro. Transformer chaque code zéro en badge "réponse correcte du modèle" supprimerait une partie essentielle du résultat. Le projet ne recommande pas de seuils prêts à l'emploi. Un seuil qui laisse passer les réponses ordinaires doit aussi être évalué sur des substitutions pertinentes.

Engagement attendu + requête + couverture + politique
                         |
                  Vérification de preuve
                         |
              Résultat selon cette politique

Exactitude factuelle, permission et tâche terminée
exigent leurs propres preuves.

Le théorème ne couvre pas tous les programmes

Le guide des propriétés prouvées décrit les preuves Lean concernant le vérificateur Lean et les définitions du protocole, avec leurs hypothèses. Le vérificateur C++ et le prouveur CUDA suivent le protocole et sont testés contre lui ; leur équivalence formelle aux définitions Lean n'est pas prouvée.

Le calcul concerne un modèle quantifié à arithmétique entière et virgule fixe. Sa relation avec un modèle flottant d'origine relève de mesures. Mon interprétation : spécification, programme et enveloppe de service demandent chacun des éléments adaptés à leur frontière.

Le dénominateur des 110 tokens par seconde

Le guide de performances explique le chiffre : préremplissage stable, contexte de 1 024 tokens, lots de 24 requêtes sur un H100. Dans ces mesures, chaque preuve porte sur le token suivant. Démarrage, création de l'engagement et vérification par l'enveloppe du service sont exclus du chiffre principal.

Ce n'est pas un débit de 110 tokens de réponse générés par seconde. Les réponses complètes stockées, sous la politique souple, appartiennent à une autre expérience. Attente du lot, vérification CPU et mémoire hôte comptent également. Ce sont des mesures du projet, sans journaux d'exécution dans le dépôt, que je n'ai pas reproduites.

Un dossier d'essai modeste

Ce JSON explicatif n'est ni le format de requête FlashProve ni un vérificateur fonctionnel :

{
  "expected_commitment": "reviewed-registry-entry",
  "request_fixture": "synthetic-question-07",
  "expected_output_positions": [0, 1, 2],
  "acceptance_policy": "exact-match",
  "proof_status": "not-run",
  "factual_answer_check": "separate-fixture-required",
  "external_action_permission": "none"
}

L'essai proposé change l'engagement ou la requête et exige un rejet. Une couverture réduite doit produire une différence explicite. Une politique inconnue reste non prise en charge ; un délai dépassé ne devient pas une acceptation. Ces vérifications n'ont pas été exécutées ici.

Il faut ensuite confronter la réponse à un exemple synthétique dont le total attendu est connu. Une preuve d'inférence ne remplace pas ce contrôle et ne donne pas la permission d'envoyer un message ou de modifier un compte.

La licence Apache 2.0 concerne le projet ; poids et composants ont leurs conditions. Le code ouvert n'efface pas les coûts GPU et d'ingénierie. Pour un produit, je retiens une exigence : afficher la politique et la couverture du résultat sans en faire une promesse générale de vérité ou de tâche accomplie.