FlashProve: Anthropic dimostra quale modello ha dato la risposta

Il 2 novembre il Frontier Red Team di Anthropic ha pubblicato FlashProve, un prototipo aperto di inferenza verificabile («provable inference»). Con questo strumento un fornitore di modelli può dimostrare crittograficamente che una certa risposta proviene da un certo insieme di pesi, dichiarato in anticipo, senza rivelare i pesi stessi. Il codice è su GitHub con licenza Apache 2.0.

Quale problema risolve FlashProve?

Quando interroghiamo un modello tramite API, non abbiamo modo di verificare che a rispondere sia stato davvero il modello per cui paghiamo. Gli autori citano l’esempio di un servizio intermediario che sostituisce di nascosto il modello «for cost reasons», e di un fornitore che potrebbe servire una versione più economica o degradata e falsificare i log.

FlashProve risponde con uno zkSNARK, cioè una prova breve a conoscenza zero. Funziona in due passaggi:

1. Una volta per modello, il fornitore pubblica un impegno (commitment) sui pesi: una breve «impronta digitale» che lo vincola a un solo insieme di pesi senza svelarli.
2. Per ogni richiesta, il server genera una prova che proprio il modello dichiarato ha prodotto quei token. Chiunque può verificarla su una normale CPU, senza accesso ai pesi.

La prova ha alcune proprietà: una prova onesta passa sempre, una prova falsa è praticamente impossibile da costruire, i pesi e i valori intermedi restano nascosti e la prova stessa è piccola ed economica da verificare.

Quanto è veloce FlashProve?

Qui la cosa si fa interessante. Il team l’ha dimostrato sul Llama 4 Maverick completo, un modello MoE (mixture-of-experts) da 400 miliardi di parametri, di cui circa 17 miliardi attivi per token, con pesi a 4 bit. Secondo il post:

1. Il prover richiede una H100 e 24 core CPU, e legge i pesi in streaming da circa 290 GB di memoria dell’host.
2. La fase preliminare dura circa 39 minuti e si esegue una sola volta per modello.
3. Un batch di 24 richieste richiede circa 223 secondi, cioè circa 110 token al secondo, e una singola prova pesa 18,78 MB.
4. La verifica di una prova richiede 17 secondi su 24 thread (21 secondi su uno), senza GPU.

Il sovraccarico resta alto: generare la prova richiede circa 72 volte più tempo di quanto vLLM impieghi per elaborare le stesse 24 richieste (da 66 a 77 volte a seconda dell’esecuzione). Per confronto, gli autori citano precedenti lavori aperti che raggiungevano frazioni di token al secondo o funzionavano su modelli della taglia di GPT-2.

E Claude che ruolo ha?

Nella ricerca stessa. Secondo gli autori, Claude ha sviluppato i miglioramenti degli zkSNARK per l’inferenza e ha scritto la specifica del protocollo. Il team sottolinea però che Claude «often makes decisions that are hard to evaluate», perciò le proprietà di sicurezza sono state formalizzate e dimostrate in Lean. Il repository contiene, tra l’altro, il prover, un verificatore veloce in C++ e un secondo verificatore, formalmente verificato, in Lean; secondo gli autori i due concordano su ogni prova testata. Di come Claude se la cava con le dimostrazioni formali ho scritto a proposito della verifica formale di 123 librerie open source.

Tra gli autori ci sono ricercatori di Anthropic, EPFL, MIT, StarkWare e Succinct.

A cosa fare attenzione?

Primo: è un prototipo di ricerca. Il post non dice nulla sull’uso di FlashProve per i modelli Claude o in produzione in Anthropic, e il repository è segnato come non manutenuto e non accetta modifiche.

Secondo: i limiti descritti dagli stessi autori. La prova copre una versione intera dei pesi e la decodifica greedy (greedy decoding), quindi le risposte con campionamento possono differire. Il contesto è limitato a 1024 token, l’architettura del modello non è nascosta e il progetto presuppone un modello MoE. Mancano inoltre garanzie formali per il codice eseguibile veloce.

Terzo: la latenza. FlashProve genera la prova dopo l’inferenza, a batch, quindi la prova non arriva insieme alla risposta.

A cosa può servire?

Gli autori citano, tra l’altro, il rilevamento di server compromessi o modelli sostituiti, la conferma di quale modello ha scritto un certo testo e il controllo che vengano serviti solo modelli approvati. Un’idea curiosa è la cosiddetta «Proof-of-Failure»: una prova che il fornitore ha consumato almeno un certo numero di token di un modello specifico senza ottenere un risultato, per esempio che il modello non ha trovato bug in una patch dopo almeno 1 milione di token.

È un approccio diverso dal watermark di Claude, che marca il testo in modo statistico e richiede una chiave segreta per il rilevamento. FlashProve offre una prova matematica che chiunque può verificare. Nei piani del team ci sono l’occultamento dei dettagli dell’architettura e l’estensione del limite di 1024 token all’intera finestra di contesto.

FAQ

Che cos’è FlashProve?

È un prototipo aperto di Anthropic per l’inferenza verificabile: un sistema di prove crittografiche (zkSNARK) che permette di verificare che una risposta sia stata generata da un modello specifico e dichiarato, senza rivelarne i pesi.

FlashProve funziona con Claude?

Il post di Anthropic non ne parla. Il team l’ha testato sul modello aperto Llama 4 Maverick, e il progetto stesso è un prototipo di ricerca.

Posso verificare da solo una prova FlashProve?

Sì. Secondo il README, la verifica di una prova di esempio si può eseguire su Linux con g++ 13, con meno di 2 GB di RAM e senza GPU. Per generare prove sul modello completo servono una H100 da 80 GB e diverse centinaia di GB di RAM.

Con quale licenza è distribuito FlashProve?

Con licenza Apache 2.0. I pesi del modello non sono inclusi: vanno scaricati da Hugging Face con la licenza Llama 4.