Anthropic lanserar FlashProve för kryptografiska bevis av AI-inferens

Anthropic lanserade FlashProve den 2 november 2026: en forskningsprototyp med öppen källkod som använder kryptografiska bevis för att visa att ett svar från en språkmodell kommer från en uppsättning vikter som har låsts fast, utan att avslöja vikterna. Företaget uppgav att bevisgenereringen nådde 110 token per sekund för Meta’s Llama 4 Maverick.

Arbetet tar sig an en lucka i verifieringen av AI-tjänster som körs i värdmiljöer. Ett svar av hög kvalitet visar inte vilken modell som har genererat det: en routningstjänst skulle kunna byta ut modellen mot ett annat system, en utvärderare skulle kunna få en annan modell än den som var avsedd att testas, eller en angripare skulle kunna ändra tokenströmmen. För användare är det opraktiskt att kontrollera detta genom att köra modellen igen när vikterna är privata och maskinvarukraven är höga.

Koppla svar till dolda vikter

FlashProve använder ett kortfattat kunskapsargument med nollkunskap, eller zkSNARK, i en lösning som enbart bygger på programvara i stället för att förlita sig på betrodd maskinvara. I en offlinefas publicerar leverantören ett kort åtagande som identifierar en exakt uppsättning vikter, samtidigt som vikterna hålls hemliga. För färdiga prompt- och svarpar skapar systemet ett bevis för att utdatatokenen är resultatet från den modell som åtagandet avser. Alla som har åtagandet, prompten och svaret kan kontrollera beviset utan tillgång till vikterna.

De avsedda egenskaperna är fullständighet, sundhet, nollkunskap och kortfattadhet. Ett ärligt bevis bör godtas, medan det ska krävas att allmänt accepterade kryptografiska antaganden bryts för att intyga ett falskt påstående. Att kontrollera ett bevis bör varken avslöja vikterna eller mellanliggande beräkningsvärden. Lösningen döljer också vilka delnätverk i blandningen av experter som kördes för varje token, även om modellens arkitektur i sig förblir synlig.

Implementeringen utnyttjar Mavericks struktur med en blandning av experter. Bevisarens arbetsmängd skalar med de ungefär 17 miljarder parametrar som är aktiva för en token, i stället för med samtliga 400 miljarder, samtidigt som expertvalen fortfarande döljs. Segmenterade vikter strömmas från värdminnet, vilket gör att bevisaren ryms på en GPU med 80 GB minne och cirka 290 GB värdminne vid sidan av.

Anthropic beskriver möjliga användningsområden inom integritetskontroller för kunder, oberoende utvärderingar, regleringsverktyg och upprätthållande av krav på godkända modeller. Inferensintyg skulle kunna intyga att förfrågningar har hanterats av en viss angiven modell, men de skulle inte visa att samma maskinvara inte också användes för att träna en annan modell. Den skillnaden begränsar vad sådana intyg skulle kunna visa när det gäller efterlevnadskrav som bygger på hur beräkningskapaciteten används.

Bevisprestanda och inferensens merkostnad

Anthropics utvärdering använde en offentligt tillgänglig 4-bitarsversion av modellen. En server med en H100 och 24 CPU-kärnor skapade bevis för en batch med 24 förfrågningar på cirka 223 sekunder, med ett bevis på 18,78 MB för varje förfrågan. Offlinefasen för att skapa åtagandet tog cirka 39 minuter.

På verifieringssidan hämtar klienten ett åtagande på cirka 6,5 MB och kontrollerar bevisen på en CPU utan GPU. Anthropic uppmätte en verifieringstid på 17 sekunder med 24 trådar och 21 sekunder med en tråd, inklusive kontrollerna i offlinefasen.

Mätningarna skiljer en kontrollprocess som enbart använder CPU från en betydligt mer krävande bevisgenerering. I Anthropics jämförelse med FP8-inferens på åtta H100-kort med vLLM krävde bevisgenereringen cirka 72 gånger så mycket tid per GPU för samma batch och cirka 94 gånger så mycket vid den högsta belastning på vLLM som testades. Genomströmningen innebär alltså en betydande kostnad jämfört med att köra modellen utan bevis.

Formell verifiering och praktiska begränsningar

FlashProve-arkivet innehåller en bevisare, en snabb C++-verifierare, en långsammare Lean-verifierare, Lean-bevis för övergripande matematiska påståenden och en interaktiv satsvisualiserare, allt under licensen Apache 2.0. Version 0.16.0 betecknas som en forskningsartefakt som inte underhålls och som inte tar emot bidrag.

Lean-arbetet behandlar fullständighet, sundhet och nollkunskap i modellen med slumporakel. De formella påståendena behöver fortfarande granskas manuellt för att fastställa att de uttrycker de avsedda garantierna. Lean-verifieraren är formellt kopplad till sundhetssatsen, men C++-verifieraren, som är avsedd för rutinmässig användning, saknar formella garantier och har i stället testats för att se om den överensstämmer med Lean-verifieraren.

Projektets dokumentation om kända begränsningar anger att AI-system under mänsklig ledning skrev nästan all programvara, Lean-bevis och dokumentation samt körde de redovisade testerna. Ingen oberoende säkerhetsgranskning har genomförts, och testningen av hur väl vikterna hålls hemliga och av adversariella bevis är fortfarande begränsad.

Bevisen omfattar en exakt heltalsversion av vikterna vid girig avkodning. Inferens med flyttal eller avkodning genom sampling kan avvika från den beräkning som bevisas, och de generiska feltesterna omfattar inte promptar som utformats adversariellt. Kontextlängden är begränsad till 1 024 token, medan tidsattacker och andra sidokanalsattacker inte omfattas av garantin. Bevisgenerering i efterhand medför också omberäkningar, fördröjda försäkringar och icke-determinism jämfört med att skapa bevis samtidigt som inferensen körs.

För att verifierbar inferens ska bli en rutinmässig kontroll av den trafik som betjänas återstår framför allt arbete inom de områden som den här utgåvan blottlägger: att sänka kostnaden för att ta fram bevis, täcka mindre restriktiv avkodning och längre kontexter samt knyta den snabba implementationen fastare till det formella protokollet.