Il 2 novembre 2026 Anthropic ha presentato FlashProve, un prototipo di ricerca open source pensato per verificare se alcuni token di una risposta corrispondono all’output di un modello identificato in anticipo dai suoi pesi. La prova crittografica può collegare un output al modello impegnato, ma non ne stabilisce la correttezza. Anthropic
Che cosa verifica FlashProve
FlashProve usa gli zkSNARK, prove crittografiche compatte che consentono di controllare un calcolo senza rivelarne i dati riservati. In questo caso, il fornitore fissa crittograficamente una specifica versione dei pesi del modello. Chi verifica riceve l’impegno sui pesi, il prompt e la risposta e controlla se i token dichiarati corrispondono all’output di quel modello secondo il calcolo previsto.
Anthropic afferma che la prova nasconde i pesi e alcuni valori intermedi del calcolo, compresi gli esperti attivati nel modello. L’architettura, invece, resta visibile. La verifica riguarda la provenienza dell’output: non valuta se la risposta sia vera o sicura.
Come funzionano impegno e prova
La procedura ha una fase iniziale, svolta una volta per modello, che crea l’impegno crittografico sui pesi. In seguito, il sistema produce le prove per gli output scelti. FlashProve le genera a posteriori, in batch, anziché accompagnare ogni token mentre viene prodotto.
Questa scelta comporta ricalcoli e un’attesa prima che la garanzia sia disponibile. Inoltre, la prova descritta da Anthropic controlla un token per volta e riguarda un sottoinsieme dei token, non necessariamente ogni token di una risposta.
I risultati dichiarati da Anthropic
La valutazione ha usato Llama 4 Maverick, un modello mixture-of-experts da 400 miliardi di parametri, con circa 17 miliardi attivi per token e pesi pubblici convertiti a 4 bit da terzi. Con una GPU H100 e 24 core CPU, Anthropic riferisce che la prova di un batch di 24 richieste ha richiesto circa 223 secondi, con una velocità di circa 110 token al secondo. Ogni prova occupava 18,78 MB.
La verifica non richiedeva una GPU: Anthropic riferisce 17 secondi con 24 thread CPU e 21 secondi con un thread. Il client scaricava un impegno di circa 6,5 MB. La preparazione iniziale dell’impegno richiedeva circa 39 minuti per modello; secondo Anthropic, poteva essere riutilizzato per circa 16 milioni di richieste prima del rinnovo.
Il confronto con vLLM riguardava batch da 24 richieste e la versione FP8 dello stesso modello su otto H100. Anthropic riferisce circa 72 volte più tempo GPU per GPU per generare le prove, con valori da 66 a 77 volte nelle diverse esecuzioni e circa 94 volte al carico massimo di vLLM testato. Sono risultati legati a quelle condizioni, non una velocità generale valida per altri modelli o configurazioni.
I confini della prova
La prova riguarda una versione del modello calcolata con numeri interi e la decodifica greedy, cioè la scelta deterministica del token con il punteggio più alto. Anthropic indica un limite attuale del contesto di 1.024 token. Output generati con calcoli in virgola mobile o campionamento possono divergere da quello verificato; la descrizione del sistema non equivale a un’attestazione generale di impostazioni come la temperatura o i livelli di ricerca.
Anthropic ha formalizzato in Lean alcune proprietà di sicurezza, tra cui completezza, solidità e conoscenza zero. Tuttavia, non garantisce formalmente che il protocollo Lean, il documento tecnico e il codice eseguibile veloce coincidano. L’azienda riferisce che, nei test svolti, il verificatore C++ ha concordato con quello Lean su tutte le prove controllate. Segnala inoltre che i tempi di generazione potrebbero esporre informazioni attraverso effetti collaterali.
Che cosa ha pubblicato Anthropic
Il rilascio comprende un generatore di prove, un verificatore veloce in C++, uno in Lean, le specifiche del protocollo, le prove formali e un visualizzatore interattivo dei teoremi. Anthropic indica la licenza Apache 2.0 per codice, prove Lean e documentazione. I pesi di Llama 4 Maverick usati nella valutazione non fanno parte del rilascio.
