Anthropic presenta FlashProve: le risposte AI diventano verificabili con prove crittografiche

🛡️ Executive Summary

• AI verificabile: Anthropic presenta FlashProve, un prototipo open source che dimostra crittograficamente quale modello ha generato una risposta senza rivelarne i pesi.
• 110 token al secondo: il sistema verifica l’inferenza di Llama 4 Maverick da 400 miliardi di parametri utilizzando una Nvidia H100 e prove da circa 19 MB.
• Costi ancora elevati: generare le prove richiede risorse GPU circa 70–95 volte superiori all’inferenza ordinaria. Il sistema rimane sperimentale.

Anthropic presenta FlashProve, un prototipo open source che consente di dimostrare crittograficamente quale modello di intelligenza artificiale ha generato una risposta, senza rivelarne i pesi. La ricerca, pubblicata il 2 novembre 2026, affronta un problema concreto dei servizi AI: chi utilizza un chatbot o un gateway di terze parti normalmente non può verificare che stia ricevendo davvero il modello acquistato, né escludere modifiche fraudolente alla risposta. Il sistema utilizza prove zero-knowledge di tipo zkSNARK e raggiunge circa 110 token al secondo su una singola GPU Nvidia H100, testando Llama 4 Maverick da 400 miliardi di parametri. Il risultato apre prospettive per auditing, cybersecurity e controllo dei fornitori, ma non equivale a una soluzione pronta per tutti: produrre le prove richiede ancora un costo computazionale circa 70–95 volte superiore all’inferenza ordinaria.

Come funziona FlashProve: un certificato per ogni risposta del modello

Nella ricerca ufficiale su FlashProve, Anthropic descrive due ruoli distinti: il fornitore del modello, che produce una prova, e il destinatario, che può verificarla. Prima dell’utilizzo il provider pubblica un impegno crittografico, o commitment, legato a una specifica configurazione dei pesi. Quando arriva una richiesta, il sistema genera una prova che collega input, output e modello dichiarato. Il verificatore può controllare il certificato usando una CPU ordinaria, senza accedere ai pesi proprietari né eseguire nuovamente l’intero modello. La proprietà zero-knowledge nasconde i pesi e i passaggi intermedi della computazione; non rende necessariamente segreti il prompt e la risposta, né nasconde l’architettura del modello. Il meccanismo può essere utile contro la sostituzione silenziosa di un modello costoso con uno più economico e contro la manipolazione delle risposte lungo un’infrastruttura compromessa. Non garantisce però che una risposta sia vera, imparziale o sicura: certifica l’origine computazionale rispetto al modello impegnato. È una proprietà differente dalla protezione dei pagamenti e dell’identità attraverso zkAPI, che utilizza tecniche zero-knowledge per un altro obiettivo.

Llama 4 Maverick da 400 miliardi di parametri: i risultati e il prezzo delle prove

Il benchmark riguarda Llama 4 Maverick, modello Mixture-of-Experts da 400 miliardi di parametri, quantizzato a quattro bit, che ne attiva circa 17 miliardi per token. Il sistema di generazione delle prove utilizza una H100 con memoria host aggiuntiva e raggiunge 110 token verificati al secondo elaborando richieste in batch. Ogni prova pesa mediamente 18,78 MB e riguarda un token verificato su un contesto massimo di 1.024 token. La verifica richiede circa 17 secondi su una CPU a 24 thread, oppure 21 secondi su un solo thread, senza GPU. Preparare l’impegno iniziale richiede circa 39 minuti. Questi numeri sono promettenti rispetto ai precedenti esperimenti, ma rendono evidente il divario economico: nei confronti pubblicati dai ricercatori il lavoro GPU necessario a dimostrare una risposta risulta all’incirca 70–95 volte più oneroso del normale servizio di inferenza con vLLM. Parlare di verificabilità istantanea o gratuita sarebbe dunque fuorviante.

Lean, codice aperto e limiti: la verifica formale non copre tutto il sistema

Anthropic pubblica documentazione e codice di FlashProve su GitHub, un verificatore rapido in C++ e uno in Lean, oltre alle dimostrazioni delle proprietà matematiche del protocollo. Il ricorso a Lean consente di formulare e controllare proprietà come completezza, solidità e zero-knowledge, ma la stessa società indica un limite essenziale: il codice ad alte prestazioni e la sua equivalenza integrale al protocollo formalizzato non sono ancora dimostrati. Il prototipo riguarda inoltre un modello con aritmetica intera e decodifica greedy, non tutti i modi con cui i chatbot commerciali generano testo; il contesto di 1.024 token è molto inferiore a quello di numerose conversazioni moderne. Anche possibili canali laterali, come i tempi di generazione delle prove, restano fuori dalla garanzia dichiarata. Il repository è distribuito con licenza Apache 2.0, ma viene presentato come artefatto di ricerca, non come prodotto mantenuto per ambienti di produzione.

Dalla sicurezza dei gateway AI alla verifica per aziende e regolatori

L’applicazione più immediata riguarda servizi che instradano richieste fra diversi modelli, dove il cliente deve oggi fidarsi delle dichiarazioni del fornitore. Un certificato verificabile potrebbe dimostrare l’utilizzo del modello promesso, documentare controlli effettuati da sistemi AI e sostenere verifiche indipendenti. Questo filone è complementare alle architetture di confidential computing e attestazione dell’ambiente di esecuzione, già affrontate nell’approfondimento sull’integrazione del team Opaque in Anthropic. Un’altra impostazione è quella della cifratura end-to-end e dell’attestazione hardware adottate da Brave Leo. Anthropic ipotizza anche strumenti per regolatori interessati a verificare l’impiego di modelli approvati, ma non presenta FlashProve come requisito normativo esistente. Per aziende e pubbliche amministrazioni italiane il valore è prospettico: poter distinguere una promessa commerciale da una prova tecnica ridurrebbe l’asimmetria informativa nei contratti AI. Il limite, per ora, resta l’industrializzazione: senza costi sostenibili, contesti più lunghi e verifica completa del software, la prova crittografica rimane un risultato di ricerca significativo, non un certificato universale di affidabilità dell’intelligenza artificiale.