FlashProve di Anthropic: come verificare quale modello AI ti sta rispondendo

Quando usi un assistente AI tramite un servizio online, c’è una domanda che di solito resta senza risposta: il modello che ti sta rispondendo è davvero quello dichiarato dal fornitore? Anthropic ha pubblicato FlashProve, un prototipo di ricerca open source per la cosiddetta inferenza dimostrabile, cioè un sistema che permette di verificare in modo crittografico che una risposta sia stata prodotta da uno specifico modello, senza che i pesi vengano mai rivelati.

Il lavoro, descritto nella pagina di ricerca ufficiale di Anthropic, è stato sviluppato con ricercatori di EPFL e MIT ed è rilasciato con licenza Apache 2.0. Non è un prodotto pronto per la produzione, e gli stessi autori lo presentano come un progresso intermedio. Ma il problema che affronta è reale, e il modo in cui lo affronta merita di essere capito.

Che cos’è FlashProve e quale problema risolve

FlashProve è un sistema basato su una zkSNARK, ovvero una prova a conoscenza zero succinta. In pratica ci sono due attori: un prover, cioè il fornitore del modello, e un verifier, cioè tu o chiunque voglia controllare. Il fornitore dimostra che un certo testo è l’output di un certo modello, e il verificatore può controllarlo senza vedere i pesi.

Perché è importante? Oggi la fiducia verso un’API di inferenza è totale e cieca. Un fornitore potrebbe servire una versione più piccola o quantizzata del modello per risparmiare, un server potrebbe essere compromesso, un intermediario potrebbe sostituire il modello senza dirlo. Con una prova verificabile, questi scenari diventano rilevabili.

Cosa significa “provare” un modello

La prova non dice che la risposta sia corretta o utile. Dice una cosa più precisa: il modello impegnato in una commitment pubblica produce esattamente quei token di output a partire da quel prompt. È una garanzia sull’identità del modello, non sulla qualità del suo ragionamento.

Gli autori elencano quattro proprietà. La completezza garantisce che le prove oneste vengano accettate. La solidità rende praticamente impossibile falsificare una prova per un’affermazione falsa. Lo zero-knowledge assicura che il verificatore non impari nulla su pesi, valori intermedi o su quali esperti siano stati attivati. La succintezza mantiene le prove piccole e rapide da controllare.

Come funziona: commitment offline e prove online

Il processo si divide in due fasi. Nella fase offline il fornitore pubblica una breve commitment ai pesi del modello, una sorta di impronta digitale che li identifica senza esporli. Questa operazione si fa una sola volta per modello.

Nella fase online, per ogni richiesta, il prover genera un file di prova che attesta che il modello impegnato produce quei token. Chiunque disponga della commitment, del prompt e della risposta può verificarla, senza accedere ai pesi.

La costruzione tecnica si basa su un interactive oracle proof compilato in una prova crittografica tramite funzioni hash. Secondo Anthropic questo approccio offre sicurezza post-quantistica, un dettaglio non banale per un sistema pensato per durare.

Le scelte di ingegneria

Per rendere il tutto praticabile, il team ha preso alcune decisioni mirate. Il lavoro del prover scala con i circa 17 miliardi di parametri attivi per token, e non con tutti i 400 miliardi del modello, grazie all’architettura Mixture-of-Experts. Le richieste vengono dimostrate in batch dopo la generazione, e non durante. Il sistema entra su una sola GPU da 80 GB, con i pesi trasmessi da circa 290 GB di memoria host.

La scelta della prova a posteriori, su un sottoinsieme di token, è un compromesso dichiarato: secondo gli autori sacrifica la verifica in tempo reale a favore di velocità, sicurezza e minore complessità.

I numeri: quanto costa dimostrare un modello

I test sono stati condotti su Llama 4 Maverick, un modello Mixture-of-Experts da circa 400 miliardi di parametri con pesi a 4 bit, usando una GPU H100 e 24 core CPU per il prover. La fase offline richiede circa 39 minuti e produce una commitment che copre circa 16 milioni di richieste.

Per la fase online, un batch di 24 richieste richiede circa 223 secondi, pari a circa 110 token al secondo. Ogni richiesta copre una finestra di 1.024 token e produce una prova di circa 18,78 MB.

Il verificatore scarica una commitment da circa 6,5 MB e poi una prova per richiesta. Il controllo richiede circa 17 secondi su 24 thread, oppure 21 secondi su un solo thread, comprese le verifiche offline.

Il prezzo della garanzia

Il confronto con l’inferenza normale è il dato che ridimensiona gli entusiasmi. Rispetto a vLLM con pesi FP8 su otto H100, la dimostrazione ha richiesto circa 72 volte il tempo GPU per singola GPU, con un intervallo tra 66 e 77 nelle varie prove, e circa 94 volte al carico massimo testato. Anthropic sintetizza il tutto in un sovraccosto di circa 70-95 volte.

Per questo la prova non può accompagnare ogni risposta di un servizio reale. Ha senso come controllo a campione, come audit o come strumento per chi deve certificare che un certo hardware stia eseguendo un certo modello.

Limiti dichiarati dagli autori

Una parte apprezzabile della pubblicazione è l’elenco onesto dei limiti. Il codice veloce non ha garanzie formali, e il protocollo in Lean, il paper e il codice non sono garantiti allineati tra loro. La prova riguarda una versione intera esatta dei pesi con decodifica greedy, quindi output in virgola mobile o campionati potrebbero divergere, e i prompt costruiti in modo avversariale non sono coperti.

Il sistema presuppone un’architettura Mixture-of-Experts, e l’architettura stessa non viene nascosta: nasconderla è lasciato a lavori futuri. Gli attacchi side-channel, come le misure di temporizzazione, sono fuori ambito. Infine il contesto è limitato a 1.024 token, pochissimo rispetto alle finestre dei modelli di frontiera.

In breve, siamo davanti a una dimostrazione di fattibilità, non a una soluzione pronta.

Casi d’uso: regolazione, audit e provenienza del testo

Anthropic indica diversi scenari. Il primo riguarda il controllo e la regolazione: verificare che un hardware stia eseguendo inferenza, anche se questo non esclude che nel frattempo venga usato per addestrare. Il secondo è il rilevamento di manomissioni, cioè confermare quali pesi girano su un server e individuare server compromessi o modelli sostituiti.

Poi c’è la provenienza del testo, ossia dimostrare che un certo modello è stato usato su certi input, e l’approvazione dei modelli, per garantire che vengano serviti solo quelli autorizzati. Infine, la garanzia per valutatori indipendenti e per i clienti di servizi di routing di terze parti, che oggi devono fidarsi di chi sta in mezzo.

Si inserisce nel quadro di un’attenzione crescente di Anthropic verso trasparenza e controllo dell’ecosistema. Ne abbiamo parlato, da angolazioni diverse, a proposito della Usage and Cost Analytics API per tenere sotto controllo l’uso di Claude, e delle regole di opt-out dall’addestramento in robots.txt, dove il tema della fiducia tra fornitori e utenti era già centrale.

Perché ti riguarda da vicino

Se lavori con le API dei modelli, per sviluppo o per marketing e contenuti, FlashProve non cambia il tuo flusso di lavoro oggi. Cambia però la prospettiva: l’idea che un fornitore possa dimostrare, e non solo dichiarare, quale modello sta usando potrebbe diventare un requisito in settori regolati, dalla finanza alla sanità.

È anche un segnale per chi sviluppa agenti e applicazioni su catene di servizi: più intermediari ci sono, più serve poter verificare. Tra le novità recenti sul fronte sviluppatori c’è ad esempio l’API per le conversazioni lunghe e gli agenti di Anthropic, un ambito in cui la tracciabilità diventerà sempre più rilevante.

Cosa è incluso nel rilascio

Anthropic rende disponibili un rapporto tecnico, una specifica del protocollo e un post introduttivo. Sul versante del software ci sono un prover, un verificatore veloce in C++ e uno più lento scritto in Lean, insieme alle dimostrazioni Lean delle affermazioni principali e a un visualizzatore interattivo per facilitare l’audit.

I pesi non sono inclusi: vanno scaricati da Hugging Face secondo la licenza Llama 4 di Meta.

Conclusioni: una direzione da seguire

FlashProve non rende i modelli più intelligenti né le risposte più affidabili nel contenuto. Rende però possibile, almeno in laboratorio, una cosa che finora mancava: verificare l’identità di un modello senza chiedere a nessuno di rivelare i propri segreti industriali. Con un sovraccosto di 70-95 volte e un contesto di 1.024 token siamo lontani dall’uso quotidiano, ma la direzione è chiara.

Se ti occupi di AI per lavoro, tieni d’occhio questa linea di ricerca e leggi il materiale originale. E se vuoi approfondire l’ecosistema dei modelli di Anthropic, parti dalla nostra sezione dedicata a Claude AI: ti aiuterà a collocare queste novità nel quadro più ampio.