L’ANALISI
FlashProve: test CPU e limiti della prova sul modello
FlashProve accetta una prova sintetica su CPU e respinge 10 alterazioni: il test copre token 61–63 e y, non una chat o un servizio reale.
In breve: FlashProve è un prototipo di provable inference: collega un calcolo a un commitment dei pesi. Nel test CPU del 4 novembre il fixture originale passa e dieci copie alterate vengono respinte. È una dimostrazione su pesi sintetici, non un certificato per qualsiasi chat. Anthropic: Progress on provable inference.
Metodo: il Radar ha riletto e verificato hash e righe finali dei log prodotti dal laboratorio automatico del 4 novembre, sulla revisione 9e2bdd8ff5bf9c62f18263d7dac189b0400b260c. Non è una prova eseguita personalmente da Francesco e non è stata ripetuta in questo ciclo. Annuncio originale: 2 novembre 2026; verifica editoriale dei log: 4 novembre.
Che cosa può verificare FlashProve?
Il provider fissa un commitment dei pesi e produce una prova del calcolo; il client controlla la prova senza ricevere quei pesi. Per un servizio reale il commitment deve provenire da una fonte indipendente fidata: accettare soltanto quello fornito insieme alla prova non risolve l’identità del modello. Il programma verifica un’affermazione delimitata da input e parametri, non il nome commerciale mostrato nell’interfaccia. FlashProve: README della revisione verificata.
Che cosa ha restituito il test CPU?
La compilazione termina con exit 0. Il controllo del fixture termina con exit 0 e YES; lo script delle copie alterate termina con exit 0 e la conferma che tutti i dieci casi sono stati respinti. Per ciascuna copia alterata il verificatore restituisce exit 1 e un motivo NO. Sono controlli dello stesso esempio, non esperimenti indipendenti su dieci modelli. I log sono stati confrontati con gli hash della ricevuta originale. FlashProve: copie alterate e limiti della dimostrazione.
Quali token sono realmente coperti?
Il log dichiara tokens=61..63, y=yes e policy exact-match. Non autorizza a scrivere che tutti i 64 token del fixture siano stati verificati, né che lo sia una conversazione completa. La copertura va letta insieme all’esito: YES senza posizioni, input e commitment sarebbe un’informazione incompleta. Nel nostro caso il risultato riguarda un modello sintetico e i file dell’esempio distribuito. FlashProve: parametri e perimetro della verifica.
Il verificatore C++ è formalmente verificato?
La documentazione separa i teoremi del protocollo e della libreria dagli eseguibili cp_commit, cp_prove e cp_verify. Non abbiamo eseguito Lean, generato nuove prove o verificato inferenza Maverick. Il controllo di alterazioni documentate è utile come dimostrazione riproducibile, ma un attaccante non è limitato a cambiare un bit di una prova onesta. Anche l’esito crittografico non rende vera una risposta fattualmente sbagliata. FlashProve: limiti e perimetro dei teoremi.
Condizioni e limitazioni
Il fixture copre token 61–63 e valore y. Nessun modello reale, prover GPU o verificatore Lean eseguito; i teoremi documentati non riguardano il binario cp_verify. Il repository si dichiara non mantenuto. Dieci alterazioni respinte non dimostrano la sicurezza generale del sistema.
Checklist pratica
- Fissare la revisione del repository e controllare che il progetto non sia presentato come servizio mantenuto.
- Seguire il percorso CPU del README come utente ordinario; non installare o avviare il prover GPU per questo esempio.
- Compilare con verifier/build.sh e conservare exit code, ultima riga e avvertenze.
- Verificare il fixture accepted-proof con il commitment dichiarato; conservare anche covered e result-v1.
- Eseguire try_altered_copies.py in una nuova directory privata e controllare ogni rifiuto, non soltanto l’exit dello script.
- Per una prova reale procurarsi il commitment da una fonte fidata e costruire autonomamente la richiesta attesa.
- Non presentare il risultato come attestazione di ChatGPT, Claude, di tutti i token o della correttezza fattuale.