Anthropic ha pubblicato il 2 novembre 2026 FlashProve, un prototipo di ricerca open source progettato per produrre prove crittografiche dell’esecuzione di modelli linguistici, consentendo di verificare che una risposta sia stata generata utilizzando uno specifico insieme di pesi neurali senza rivelarne il contenuto. Il sistema affronta il problema dell’identificazione verificabile dei modelli utilizzati dai servizi di inferenza remota: normalmente, un utente può osservare il risultato prodotto da un servizio AI, ma non dispone di uno strumento indipendente per dimostrare che tale risultato provenga effettivamente dal modello dichiarato dal fornitore. Una piattaforma potrebbe instradare una richiesta verso un sistema differente, un servizio di valutazione potrebbe utilizzare un modello diverso da quello sottoposto a verifica oppure un soggetto ostile potrebbe modificare la sequenza di token restituita. FlashProve propone di associare alle risposte un certificato matematico verificabile senza richiedere l’accesso ai pesi proprietari né la riesecuzione completa del modello sui dispositivi dell’utente.
Il funzionamento si basa su prove a conoscenza zero della famiglia zkSNARK, utilizzate in un’architettura interamente software e non dipendente da ambienti hardware considerati affidabili. In una fase preliminare, il fornitore genera e pubblica un impegno crittografico compatto, o commitment, che identifica una configurazione esatta dei pesi senza divulgarli. Successivamente, per una coppia composta da prompt e risposta, il sistema produce una prova della corrispondenza fra i token restituiti e il modello identificato dal commitment. Un verificatore può controllare la prova utilizzando soltanto l’impegno pubblicato, il prompt e la risposta, senza conoscere i valori dei parametri. Il sistema è progettato intorno alle proprietà di completezza, correttezza crittografica, conoscenza zero e sinteticità della prova. Una computazione legittima deve superare la verifica, mentre produrre una certificazione falsa deve risultare impraticabile in base alle ipotesi crittografiche adottate. La verifica non deve inoltre rivelare i pesi, i valori intermedi dell’elaborazione o quali esperti di un’architettura mixture-of-experts siano stati attivati durante la generazione, pur non nascondendo la struttura generale del modello.
L’implementazione sperimentale è stata sviluppata utilizzando Meta Llama 4 Maverick, modello mixture-of-experts con circa 400 miliardi di parametri complessivi e circa 17 miliardi attivi per token. FlashProve sfrutta questa proprietà per proporzionare parte del lavoro crittografico ai parametri effettivamente coinvolti nella computazione, preservando contemporaneamente la riservatezza della selezione degli esperti. I segmenti dei pesi vengono trasferiti progressivamente dalla memoria del sistema ospitante, consentendo l’esecuzione del prover su una sola GPU con 80 GB di memoria, affiancata da circa 290 GB di RAM del sistema. Anthropic ha utilizzato una conversione pubblica del modello quantizzata a 4 bit per misurare le prestazioni. Un server con una GPU NVIDIA H100 e 24 core CPU ha elaborato un lotto di 24 richieste in circa 223 secondi, raggiungendo una velocità dichiarata di generazione delle prove pari a 110 token al secondo e producendo un certificato di 18,78 MB per richiesta. La fase iniziale di generazione del commitment ha richiesto circa 39 minuti.
Dal lato del verificatore, il controllo può essere eseguito esclusivamente su CPU, senza acceleratori GPU. Il client deve scaricare un commitment di circa 6,5 MB, mentre la verifica completa ha richiesto 17 secondi utilizzando 24 thread e 21 secondi con un singolo thread, comprendendo anche i controlli associati alla fase preliminare. La generazione delle prove rimane tuttavia considerevolmente più costosa rispetto alla normale inferenza. Nel confronto con l’esecuzione FP8 di Maverick su otto GPU H100 mediante vLLM, Anthropic ha registrato un impiego di tempo GPU per la certificazione circa 72 volte superiore per lo stesso lotto di richieste, che aumenta fino a circa 94 volte nel confronto con il massimo carico vLLM esaminato. Questi risultati distinguono la relativa leggerezza della verifica dalla complessità computazionale necessaria per produrre i certificati.
Il repository FlashProve, distribuito con licenza Apache 2.0, contiene il sistema di generazione delle prove, un verificatore rapido sviluppato in C++, un verificatore più lento implementato in Lean, dimostrazioni formali di proprietà matematiche di alto livello e uno strumento interattivo per visualizzare i teoremi. Le formalizzazioni in Lean affrontano completezza, correttezza e conoscenza zero nel modello dell’oracolo casuale, ma richiedono ancora una revisione manuale per accertare che gli enunciati rappresentino esattamente le garanzie desiderate. Il verificatore Lean è formalmente collegato al teorema di correttezza, mentre quello C++ destinato all’utilizzo ordinario non dispone di una garanzia formale equivalente ed è stato controllato attraverso test di concordanza. La versione 0.16.0 è classificata come risultato di ricerca non mantenuto e non aperto a nuovi contributi. Anthropic specifica inoltre che quasi tutto il software, le dimostrazioni Lean, la documentazione e i test sono stati prodotti con sistemi AI sotto supervisione umana. Non è stato effettuato un audit di sicurezza indipendente e le prove relative alla protezione dei pesi e alla resistenza ad attacchi avversari rimangono limitate. FlashProve costituisce quindi una dimostrazione sperimentale della possibilità di certificare l’identità computazionale di un modello durante l’inferenza, senza attestare automaticamente altri aspetti dell’infrastruttura, come l’eventuale impiego della stessa capacità hardware per attività di addestramento.
Questo articolo è stato redatto con il supporto di strumenti di intelligenza artificiale (AI)