Anthropic rilascia FlashProve per dimostrare crittograficamente l’inferenza dell’IA

Anthropic ha rilasciato FlashProve il 2 novembre 2026: un prototipo di ricerca open source che usa prove crittografiche per dimostrare che la risposta di un modello linguistico è stata generata a partire da pesi fissati, senza rivelarli. L’azienda ha riferito che la generazione delle prove raggiunge 110 token al secondo con Llama 4 Maverick di Meta.

Il progetto affronta una lacuna nella verifica dei sistemi di IA ospitati. Una risposta di alta qualità non dimostra quale modello l’abbia generata: un servizio di instradamento potrebbe sostituirlo con un altro sistema, un valutatore potrebbe ricevere un modello diverso da quello previsto per il test oppure un aggressore potrebbe alterare la sequenza di token. Per gli utenti, verificare rieseguendo il modello è impraticabile quando i pesi sono privati e i requisiti hardware sono considerevoli.

Vincolare le risposte a pesi nascosti

FlashProve usa un argomento succinto di conoscenza a conoscenza zero, o zkSNARK, in una soluzione basata esclusivamente sul software, senza dipendere da hardware fidato. Durante una fase offline, il fornitore pubblica un impegno conciso che identifica un insieme preciso di pesi, mantenendoli segreti. Per coppie di prompt e risposte già completate, il sistema genera una prova che attesta che i token di output sono stati prodotti dal modello identificato dall’impegno. Chiunque disponga dell’impegno, del prompt e della risposta può verificare la prova senza accedere ai pesi.

Le proprietà previste sono completezza, solidità, conoscenza zero e succintezza. Una prova onesta dovrebbe essere accettata, mentre certificare un’affermazione falsa dovrebbe richiedere di violare ipotesi crittografiche ampiamente ritenute valide. La verifica di una prova non dovrebbe rivelare né i pesi né i valori intermedi dei calcoli. La soluzione nasconde anche quali sottoreti dell’architettura a mistura di esperti siano state eseguite per ciascun token, pur lasciando visibile l’architettura del modello.

L’implementazione sfrutta la struttura a mistura di esperti di Maverick. Il lavoro del dimostratore cresce in proporzione ai circa 17 miliardi di parametri attivi per ciascun token, anziché a tutti i 400 miliardi, pur continuando a nascondere la selezione degli esperti. I pesi suddivisi in segmenti vengono trasferiti in streaming dalla memoria host, consentendo al dimostratore di funzionare su una GPU da 80 GB affiancata da circa 290 GB di memoria host.

Anthropic indica tra i possibili impieghi i controlli di integrità per i clienti, le valutazioni indipendenti, gli strumenti normativi e l’applicazione dei requisiti relativi ai modelli approvati. I certificati di inferenza potrebbero attestare che le richieste sono state elaborate dal modello dichiarato, ma non dimostrerebbero che lo stesso hardware non sia stato utilizzato anche per addestrare un altro modello. Questa distinzione limita ciò che tali certificati potrebbero dimostrare in merito ai requisiti di conformità basati sull’uso della capacità di calcolo.

Prestazioni delle prove e sovraccarico dell’inferenza

La valutazione di Anthropic ha utilizzato una conversione a 4 bit del modello disponibile al pubblico. Un server con una H100 e 24 core CPU ha generato le prove per un lotto di 24 richieste in circa 223 secondi, producendo una prova di 18,78 MB per ciascuna richiesta. La fase di impegno offline ha richiesto circa 39 minuti.

Dal lato della verifica, il client scarica un impegno di circa 6,5 MB e controlla le prove su una CPU, senza GPU. Anthropic ha misurato tempi di verifica di 17 secondi con 24 thread e 21 secondi con un thread, includendo i controlli della fase offline.

Queste misurazioni distinguono una procedura di verifica eseguita solo su CPU da un’operazione di generazione delle prove molto più onerosa. Nel confronto di Anthropic con l’inferenza FP8 su otto H100 con vLLM, per generare le prove è stato necessario circa 72 volte il tempo GPU per lo stesso lotto e circa 94 volte il tempo al carico massimo di vLLM sottoposto a test. Questa produttività comporta quindi un costo considerevole rispetto all’elaborazione delle richieste con il modello senza prove.

Verifica formale e limiti pratici

Il repository di FlashProve contiene un dimostratore, un verificatore veloce in C++, un verificatore Lean più lento, dimostrazioni Lean di enunciati matematici di alto livello e un visualizzatore interattivo di teoremi, il tutto sotto licenza Apache 2.0. La versione 0.16.0 è indicata come un artefatto di ricerca non più mantenuto e per il quale non si accettano contributi.

Il lavoro in Lean affronta completezza, solidità e conoscenza zero nel modello dell’oracolo casuale. Gli enunciati formali richiedono comunque una revisione manuale per accertare che esprimano le garanzie previste. Il verificatore Lean è collegato formalmente al teorema di solidità, mentre il verificatore in C++, destinato all’uso ordinario, non offre garanzie formali ed è stato invece sottoposto a test per verificarne la concordanza con quello Lean.

La documentazione sui limiti noti del progetto specifica che sistemi di IA diretti da esseri umani hanno scritto quasi tutto il software, le dimostrazioni Lean e la documentazione, oltre ad aver eseguito i test riportati. Non è stata svolta alcuna verifica di sicurezza indipendente e i test sull’occultamento dei pesi e sulle prove avversarie restano limitati.

Le prove riguardano una versione intera esatta dei pesi in condizioni di decodifica greedy. L’inferenza in virgola mobile o la decodifica con campionamento possono discostarsi dal calcolo oggetto della prova, e i test generici degli errori non coprono prompt progettati in modo avversario. I contesti sono limitati a 1.024 token, mentre gli attacchi basati sui tempi e gli altri attacchi tramite canali laterali non rientrano nella garanzia. La generazione di prove a posteriori comporta inoltre ricalcoli, garanzie ritardate e non determinismo rispetto alla generazione delle prove durante l’inferenza.

Affinché la verifica dell’inferenza diventi un controllo di routine sul traffico effettivamente servito, il lavoro ancora da fare si concentra sulle lacune messe in luce da questa versione: ridurre i costi della verifica, supportare modalità di decodifica meno restrittive e contesti più lunghi, e collegare più saldamente l’implementazione rapida al protocollo formale.