Anthropic lanserer FlashProve for kryptografiske bevis på KI-inferens

Anthropic lanserte FlashProve 2. november 2026: en åpen forskningsprototyp som bruker kryptografiske bevis for å vise at et svar fra en språkmodell stammer fra forpliktende fastsatte vekter, uten å røpe dem. Selskapet oppga at bevisgenereringen nådde 110 tokener per sekund for Meta’s Llama 4 Maverick.

Arbeidet tar sikte på å tette et verifiseringsgap innen drift av KI-tjenester. Et svar av høy kvalitet viser ikke hvilken modell som produserte det: En rutingstjeneste kan bytte den ut med et annet system, en evaluator kan få en annen modell enn den som var ment å testes, eller en angriper kan endre tokenstrømmen. Det er upraktisk for brukerne å kontrollere dette ved å kjøre modellen på nytt når vektene er private og maskinvarekravene er betydelige.

Knytte svar til skjulte vekter

FlashProve bruker et kortfattet nullkunnskapsbasert kunnskapsargument, eller zkSNARK, i en ren programvareløsning som ikke er avhengig av pålitelig maskinvare. I en frakoblet fase publiserer leverandøren en kort kryptografisk forpliktelse som identifiserer ett bestemt vektesett, samtidig som vektene holdes hemmelige. For ferdigbehandlede prompt- og svarpar lager systemet et bevis på at utdataene er resultatet fra modellen som forpliktelsen identifiserer. Alle som har forpliktelsen, prompten og svaret, kan kontrollere beviset uten tilgang til vektene.

Egenskapene løsningen skal ha, er fullstendighet, sundhet, nullkunnskap og kortfattethet. Et gyldig bevis skal godtas, mens det å bekrefte en uriktig påstand skal kreve at man bryter kryptografiske antakelser som er allment anerkjent. Kontroll av et bevis skal ikke røpe verken vektene eller mellomliggende beregningsverdier. Løsningen skjuler også hvilke delnettverk i blandingen av eksperter som ble kjørt for hvert token, selv om selve modellarkitekturen fortsatt er synlig.

Implementeringen utnytter Mavericks struktur med blanding av eksperter. Arbeidsmengden for bevisgeneratoren skalerer med de omtrent 17 milliardene parameterne som er aktive for et token, i stedet for alle de 400 milliardene, samtidig som ekspertvalgene holdes skjult. Vektene er delt inn i segmenter som strømmes fra vertsminnet, slik at bevisgeneratoren får plass på én GPU med 80 GB minne, med omtrent 290 GB vertsminne i tillegg.

Anthropic beskriver mulige bruksområder innen integritetskontroller for kunder, uavhengige evalueringer, regulatoriske verktøy og håndheving av krav om godkjente modeller. Inferens-sertifikater kan bekrefte at forespørsler ble behandlet av en oppgitt modell, men de kan ikke fastslå at den samme maskinvaren ikke også ble brukt til å trene en annen modell. Dette skillet begrenser hva slike sertifikater kan dokumentere når det gjelder krav til etterlevelse som bygger på hvordan datakapasiteten brukes.

Bevisytelse og inferensbelastning

Anthropics evaluering brukte en offentlig tilgjengelig 4-bitsversjon av modellen. En server med én H100 og 24 CPU-kjerner genererte bevis for en gruppe på 24 forespørsler på omtrent 223 sekunder, og produserte et bevis på 18,78 MB for hver forespørsel. Den frakoblede forpliktelsesfasen tok omtrent 39 minutter.

På verifiseringssiden laster klienten ned en forpliktelse på omtrent 6,5 MB og kontrollerer bevisene på en CPU uten GPU. Anthropic målte verifiseringstiden til 17 sekunder med 24 tråder og 21 sekunder med én tråd, inkludert kontrollene i den frakoblede fasen.

Disse målingene viser forskjellen mellom en kontrollprosess som bare bruker CPU, og en langt mer krevende bevisgenerering. I Anthropics sammenligning med FP8-inferens på åtte H100-er som kjørte vLLM, krevde bevisgenereringen omtrent 72 ganger så mye tid per GPU for den samme forespørselsgruppen, og omtrent 94 ganger så mye ved den høyeste vLLM-belastningen som ble testet. Gjennomstrømningen har dermed en betydelig kostnad sammenlignet med å betjene modellen uten bevis.

Formell verifisering og praktiske begrensninger

FlashProve-arkivet inneholder en bevisgenerator, en rask C++-verifikator, en tregere Lean-verifikator, Lean-bevis for overordnede matematiske påstander og en interaktiv visualisering av teoremer, lisensiert under Apache 2.0. Versjon 0.16.0 er merket som et forskningsprodukt som ikke vedlikeholdes, og som ikke tar imot bidrag.

Lean-arbeidet tar for seg fullstendighet, sundhet og nullkunnskap i tilfeldig-orakelmodellen. De formelle påstandene må fortsatt gjennomgås manuelt for å fastslå om de uttrykker de tiltenkte garantiene. Lean-verifikatoren er formelt knyttet til sundhetsteoremet, men C++-verifikatoren, som er ment for rutinemessig bruk, har ingen formell garanti. I stedet er den testet for å kontrollere at resultatene samsvarer med Lean-verifikatoren.

Prosjektets dokumentasjon om kjente begrensninger opplyser at KI-systemer under menneskelig styring skrev nesten all programvaren, Lean-bevisene og dokumentasjonen, og kjørte de rapporterte testene. Det er ikke gjennomført noen uavhengig sikkerhetsrevisjon, og testingen av vektbeskyttelse og fiendtlige bevis er fortsatt begrenset.

Bevisene dekker en eksakt heltallsversjon av vektene ved grådig dekoding. Inferens med flyttall eller samplingbasert dekoding kan avvike fra beregningen det føres bevis for, og den generelle feiltestingen dekker ikke prompt utformet med fiendtlige hensikter. Konteksten er begrenset til 1 024 tokener, og tidsangrep og andre sidekanalangrep omfattes ikke av garantien. Etterfølgende bevisgenerering medfører også nye beregninger, forsinket bekreftelse og manglende determinisme sammenlignet med å generere bevis samtidig med inferensen.

For at inferens med bevis skal bli en rutinemessig kontroll av trafikken som betjenes, gjenstår det særlig å tette hullene denne lanseringen avdekker: redusere kostnadene ved å generere bevis, støtte mindre restriktiv dekoding og lengre kontekster, og knytte den raske implementeringen tettere til den formelle protokollen.