Anthropic brengt FlashProve uit voor cryptografische bewijzen van AI-inferentie

Anthropic bracht FlashProve uit op 2 november 2026: een open-sourceonderzoeksprototype dat cryptografische bewijzen gebruikt om aan te tonen dat een antwoord van een taalmodel afkomstig is van vastgelegde gewichten, zonder die gewichten prijs te geven. Het bedrijf meldde dat het voor Meta’s Llama 4 Maverick bewijzen genereerde met een snelheid van 110 tokens per seconde.

Dit onderzoek pakt een lacune aan in de verificatie van gehoste AI. Een antwoord van hoge kwaliteit bewijst niet welk model het heeft gegenereerd: een routeringsdienst kan een ander systeem inzetten, een beoordelaar kan een ander model krijgen dan het model dat bedoeld was voor de test, of een aanvaller kan de tokenstroom wijzigen. Voor gebruikers is het onpraktisch om dit te controleren door het model opnieuw te draaien wanneer de gewichten privé zijn en de hardwarevereisten aanzienlijk zijn.

Antwoorden koppelen aan verborgen gewichten

FlashProve gebruikt een beknopt zero-knowledge-argument van kennis, ofwel een zkSNARK, in een ontwerp dat uitsluitend op software berust en niet afhankelijk is van vertrouwde hardware. Tijdens een offlinefase publiceert de aanbieder een korte commitment die één exacte set gewichten identificeert, terwijl die gewichten geheim blijven. Voor voltooide prompt-antwoordparen genereert het systeem een bewijs dat de uitvoertokens afkomstig zijn van het vastgelegde model. Iedereen met de commitment, de prompt en het antwoord kan het bewijs controleren zonder toegang tot de gewichten.

De beoogde eigenschappen zijn volledigheid, deugdelijkheid, nulkennis en beknoptheid. Een eerlijk bewijs moet worden geaccepteerd, terwijl het certificeren van een onjuiste bewering het doorbreken van algemeen aanvaarde cryptografische aannames zou moeten vereisen. Het controleren van een bewijs mag noch de gewichten, noch tussenliggende berekeningswaarden onthullen. Het ontwerp verbergt ook welke subnetwerken van het mixture-of-experts-model voor elke token actief waren, hoewel de architectuur van het model zelf zichtbaar blijft.

De implementatie maakt gebruik van de mixture-of-experts-structuur van Maverick. De benodigde rekenkracht voor het genereren van een bewijs schaalt mee met de ongeveer 17 miljard parameters die actief zijn voor een token, in plaats van met alle 400 miljard, terwijl de keuzes van de experts verborgen blijven. De gewichten worden in segmenten vanuit het hostgeheugen gestreamd, zodat het genereren van een bewijs mogelijk is op één GPU van 80 GB, met daarnaast ongeveer 290 GB hostgeheugen.

Anthropic noemt mogelijke toepassingen voor integriteitscontroles bij klanten, onafhankelijke evaluaties, regelgevingstools en de handhaving van vereisten voor goedgekeurde modellen. Inferentiecertificaten kunnen bevestigen dat verzoeken door een opgegeven model zijn verwerkt, maar bewijzen niet dat dezelfde hardware niet ook wordt gebruikt om een ander model te trainen. Dat onderscheid beperkt wat zulke certificaten kunnen aantonen over nalevingsvereisten die afhangen van het gebruik van rekenkracht.

Bewijsprestaties en overhead bij inferentie

Anthropic gebruikte voor de evaluatie een publiek beschikbare 4-bitsconversie van het model. Een server met één H100 en 24 CPU-kernen genereerde in ongeveer 223 seconden bewijzen voor een batch van 24 verzoeken; elk verzoek leverde een bewijs van 18,78 MB op. De offline commitmentstap duurde ongeveer 39 minuten.

Aan de verificatiekant downloadt de client een commitment van ongeveer 6,5 MB en controleert die de bewijzen op een CPU, zonder GPU. Anthropic mat een verificatietijd van 17 seconden met 24 threads en 21 seconden met één thread, inclusief de controles van de offlinefase.

Deze metingen laten zien dat een controleproces dat alleen op een CPU draait, sterk verschilt van de veel zwaardere taak om bewijzen te genereren. In de vergelijking van Anthropic met FP8-inferentie op acht H100’s met vLLM kostte het genereren van bewijzen voor dezelfde batch ongeveer 72 keer zoveel tijd per GPU, en ongeveer 94 keer zoveel bij de hoogste geteste belasting van vLLM. De doorvoer brengt dus aanzienlijke kosten met zich mee vergeleken met het aanbieden van het model zonder bewijzen.

Formele verificatie en praktische beperkingen

De FlashProve-repository bevat een programma om bewijzen te genereren, een snelle C++-verificateur, een tragere Lean-verificateur, Lean-bewijzen van wiskundige beweringen op het hoogste niveau en een interactieve stellingvisualisator, onder de Apache 2.0-licentie. Versie 0.16.0 wordt aangeduid als een niet-onderhouden onderzoeksartefact waarvoor geen bijdragen worden geaccepteerd.

Het Lean-werk behandelt volledigheid, deugdelijkheid en nulkennis in het random-orakelmodel. De formele beweringen moeten nog handmatig worden beoordeeld om vast te stellen of ze de beoogde garanties weergeven. De Lean-verificateur is formeel gekoppeld aan de deugdelijkheidsstelling, maar voor de C++-verificateur, die bedoeld is voor routinematig gebruik, geldt geen formele garantie; in plaats daarvan is getest of deze overeenkomt met de Lean-verificateur.

In de documentatie over bekende beperkingen van het project staat dat AI-systemen onder menselijke aansturing vrijwel alle software, Lean-bewijzen en documentatie hebben geschreven en de gerapporteerde tests hebben uitgevoerd. Er is geen onafhankelijke beveiligingsaudit geweest en het testen van het verbergen van gewichten en van adversariële bewijzen is beperkt gebleven.

De bewijzen hebben betrekking op een exacte versie van de gewichten met gehele getallen, bij greedy decoding. Inferentie met drijvendekommagetallen of decodering op basis van sampling kan afwijken van de berekening waarvoor het bewijs geldt, en de algemene fouttests omvatten geen prompts die speciaal zijn ontworpen om het systeem aan te vallen. De context is beperkt tot 1.024 tokens, terwijl timingaanvallen en andere aanvallen via zijkanalen buiten de garantie vallen. Bewijzen achteraf leiden bovendien tot herberekeningen, vertraagde zekerheid en niet-determinisme in vergelijking met het genereren van bewijzen tijdens de inferentie.

Om bewijsbare inferentie een routinecontrole op het verwerkte verkeer te maken, moet vooral nog worden gewerkt aan de tekortkomingen die deze release blootlegt: de kosten van het genereren van bewijzen verlagen, minder restrictieve decoding en langere contexten ondersteunen, en de snelle implementatie steviger koppelen aan het formele protocol.