FlashProve di Anthropic verifica il modello eseguito, non la verità della risposta
Il sistema sperimentale dimostra un calcolo di inferenza circoscritto senza rivelare i pesi. Il risultato di velocità comporta però un costo GPU molto superiore.
La ricerca FlashProve di Anthropic affronta una domanda alla quale una risposta AI ben scritta non può rispondere: è stata davvero prodotta dal modello promesso dal fornitore? Il prototipo pubblicato genera prove crittografiche legate a un impegno su specifici pesi del modello, permettendo di verificare il calcolo senza ottenere quei pesi. Non dimostra che la risposta sia vera, utile o sicura.
La separazione conta. Un sistema può eseguire fedelmente il modello dichiarato e produrre comunque un errore fattuale. All’opposto, una risposta particolarmente convincente non dimostra che un intermediario abbia usato il modello indicato nel servizio acquistato. FlashProve riguarda l’identità e l’integrità del calcolo, non la valutazione del testo risultante.
La prova deve riferirsi a un’identità conosciuta
Il fornitore si impegna prima su un insieme di pesi. Produce poi una prova dell’inferenza, che viene controllata rispetto all’identificatore atteso. Se quest’ultimo arriva soltanto dallo stesso server non fidato che fornisce la risposta, il controllo può dimostrare coerenza senza stabilire che si tratti del modello desiderato dall’utente.
La documentazione del progetto chiede quindi di ottenere l’identificatore dell’impegno da una fonte fidata. È un confine pratico: la crittografia può legare il calcolo a un identificatore, ma qualcuno deve ancora stabilire quale modello quell’identificatore rappresenti.
Il protocollo punta a nascondere i pesi, non l’architettura. Esclude inoltre dal proprio ambito canali laterali come eventuali informazioni ricavabili dai tempi di esecuzione. L’espressione “conoscenza zero” descrive ciò che rivela la prova definita dal protocollo, non una garanzia incondizionata su tutto il sistema che la circonda.
La velocità ha un costo computazionale rilevante
Anthropic riporta circa 110 token al secondo per la produzione delle prove sul prefill di Llama 4 Maverick, modello mixture-of-experts da 400 miliardi di parametri, usando una conversione pubblica a quattro bit e una NVIDIA H100. La prova occupa circa 19 MB per una richiesta da 1.024 token. Il controllo può richiedere pochi secondi su CPU, mentre produrre la prova rimane oneroso.
Gli autori stimano un tempo GPU circa 70–95 volte superiore all’inferenza ordinaria con vLLM nelle condizioni confrontate. Il valore in token al secondo non annuncia quindi una chat verificata allo stesso costo di un servizio normale. Descrive una particolare configurazione sperimentale e un particolare lavoro di prova.
Il limite di contesto di 1.024 token è altrettanto importante: è molto più corto di numerose conversazioni operative e richieste di analisi documentale. La prova riguarda inoltre una versione del modello con aritmetica intera e decodifica greedy; esecuzione in virgola mobile e campionamento possono divergere da quel calcolo esatto.
Dimostrare il protocollo non certifica automaticamente il codice veloce
Il rilascio comprende enunciati e prove formali in Lean, insieme a verificatori eseguibili. Anthropic identifica esplicitamente due passaggi ancora da controllare: che gli enunciati corrispondano alla proprietà di sicurezza desiderata e che il codice implementi davvero il protocollo dimostrato. Il verificatore C++ più rapido viene confrontato nei test con quello Lean, ma non eredita una garanzia formale soltanto perché è distribuito nello stesso progetto.
Il repository si presenta come artefatto di ricerca, non come software di produzione mantenuto. Il risultato resta concreto: offre un modo per studiare la sostituzione del modello senza cercare di riconoscerlo dallo stile delle risposte. Una risposta potrebbe portare con sé una prova del calcolo che l’ha prodotta; verificare ciò che afferma resterebbe un lavoro distinto e necessario.
