Anthropic udgiver FlashProve til kryptografiske beviser for AI-inferens

Anthropic udgav FlashProve den 2. november 2026: en open source-forskningsprototype, der bruger kryptografiske beviser til at vise, at et svar fra en sprogmodel stammer fra de fastlåste vægte uden at afsløre dem. Virksomheden rapporterede en bevisgenerering på 110 tokens i sekundet for Metas Llama 4 Maverick.

Arbejdet adresserer et hul i verificeringen af hostet AI. Et svar af høj kvalitet fastslår ikke, hvilken model der har genereret det: En routingtjeneste kan erstatte modellen med et andet system, en evaluator kan få en anden model end den, der var tiltænkt testen, eller en angriber kan ændre tokenstrømmen. Det er upraktisk for brugerne at kontrollere svaret ved at køre modellen igen, når vægtene er private, og hardwarekravene er betydelige.

Svar knyttes til skjulte vægte

FlashProve bruger et kortfattet nulvidensargument for viden, eller zkSNARK, i et rent softwarebaseret design, der ikke er afhængigt af betroet hardware. I en offlinefase offentliggør udbyderen en kort forpligtelse, der identificerer ét bestemt sæt vægte, samtidig med at vægtene holdes hemmelige. For færdige prompt-og-svar-par genererer systemet et bevis på, at outputtokens er output fra den model, som forpligtelsen angiver. Alle, der har forpligtelsen, prompten og svaret, kan kontrollere beviset uden adgang til vægtene.

De tilsigtede egenskaber er fuldstændighed, sundhed, nulviden og kortfattethed. Et ærligt bevis bør accepteres, mens det bør kræve, at man bryder bredt accepterede kryptografiske antagelser, at certificere et falsk udsagn. Kontrol af et bevis bør hverken afsløre vægtene eller mellemliggende beregningsværdier. Designet skjuler også, hvilke subnetværk i blandingen af eksperter der blev kørt for hvert token, selvom selve modellens arkitektur fortsat er synlig.

Implementeringen udnytter Mavericks blanding-af-eksperter-struktur. Bevisarbejdet skalerer efter de omtrent 17 milliarder parametre, der er aktive for et token, i stedet for alle 400 milliarder, samtidig med at valget af eksperter fortsat skjules. Vægtene opdelt i segmenter streames fra værtslageret, så bevisgeneratoren kan køre på én GPU med 80 GB sammen med omkring 290 GB værtslager.

Anthropic beskriver mulige anvendelser til integritetskontrol hos kunder, uafhængige evalueringer, regulatoriske værktøjer og håndhævelse af krav om godkendte modeller. Inferenscertifikater kan dokumentere, at forespørgsler blev besvaret af den angivne model, men de kan ikke fastslå, at den samme hardware ikke også blev brugt til at træne en anden model. Denne forskel begrænser, hvad sådanne certifikater kan dokumentere om overholdelse af krav, der afhænger af, hvordan computerkapaciteten anvendes.

Bevisernes ydeevne og inferensoverhead

Anthropics evaluering brugte en offentligt tilgængelig 4-bit-konvertering af modellen. En server med én H100 og 24 CPU-kerner genererede beviser for en batch på 24 forespørgsler på omkring 223 sekunder og producerede et bevis på 18,78 MB for hver forespørgsel. Det tog omkring 39 minutter at oprette offlineforpligtelsen.

På verificeringssiden downloader klienten en forpligtelse på cirka 6,5 MB og kontrollerer beviser på en CPU uden GPU. Anthropic målte verificeringstiden til 17 sekunder med 24 tråde og 21 sekunder med én tråd, inklusive kontrollerne i offlinefasen.

Disse målinger viser forskellen mellem en kontrolproces, der kun bruger CPU, og en langt mere ressourcekrævende bevisgenerering. I Anthropics sammenligning med FP8-inferens på otte H100’er, der kørte vLLM, krævede bevisgenereringen omkring 72 gange så meget tid pr. GPU for den samme batch og omkring 94 gange så meget ved den højeste testede belastning på vLLM. Gennemløbet kommer derfor med en betydelig omkostning sammenlignet med at betjene modellen uden beviser.

Formel verifikation og praktiske begrænsninger

FlashProve-kodearkivet indeholder en bevisgenerator, en hurtig C++-verifikator, en langsommere Lean-verifikator, Lean-beviser for overordnede matematiske udsagn og en interaktiv visualisering af teoremer under Apache 2.0-licensen. Version 0.16.0 er mærket som et ikke-vedligeholdt forskningsartefakt, der ikke modtager bidrag.

Lean-arbejdet behandler fuldstændighed, sundhed og nulviden i tilfældig-orakel-modellen. De formelle udsagn kræver stadig manuel gennemgang for at fastslå, at de udtrykker de tilsigtede garantier. Lean-verifikatoren er formelt knyttet til sundhedssætningen, men C++-verifikatoren, der er tiltænkt rutinemæssig brug, har ingen formel garanti og blev i stedet testet for at sikre, at den stemmer overens med Lean-verifikatoren.

Projektets dokumentation om kendte begrænsninger anfører, at AI-systemer under menneskelig styring skrev næsten al softwaren, Lean-beviserne og dokumentationen og kørte de rapporterede tests. Der er ikke foretaget nogen uafhængig sikkerhedsrevision, og test af skjulning af vægte og adversarielle beviser er fortsat begrænset.

Beviserne dækker en eksakt heltalsversion af vægtene under grådig afkodning. Inferens med flydende tal eller afkodning med sampling kan afvige fra den beregning, der bevises, og den generiske fejlafprøvning dækker ikke prompts, der er udformet adversarielt. Kontekster er begrænset til 1.024 tokens, mens timingangreb og andre sidekanalangreb ikke er omfattet af garantien. Efterfølgende bevisgenerering medfører også genberegning, forsinkede garantier og manglende determinisme sammenlignet med at generere beviser sideløbende med inferensen.

For at inferens med beviser kan blive en rutinemæssig kontrol af den trafik, der behandles, består det resterende arbejde i at lukke de huller, som denne udgivelse afdækker: at reducere omkostningerne ved at generere beviser, understøtte mindre restriktiv afkodning og længere kontekster samt knytte den hurtige implementering tættere til den formelle protokol.