Anthropic FlashProve: Beweis per Kryptografie, welches KI-Modell geantwortet hat

Worum es geht

Anthropic hat am 2. November 2026 FlashProve veröffentlicht, einen Open-Source-Prototyp für „Provable Inference“, also beweisbare KI-Inferenz. Das System soll belegen, dass eine Antwort wirklich von einem bestimmten, vorher festgelegten Modell erzeugt wurde. Nutzer sollen das prüfen können, ohne die Gewichte des Modells zu kennen und ohne das Modell selbst nachzurechnen.

Das Problem: Wer heute eine Anfrage an ein KI-Modell schickt, kann nicht sicher wissen, welches Modell antwortet. Ein Routing-Dienst könnte aus Kostengründen heimlich ein billigeres Modell einsetzen. Ein Angreifer könnte den Token-Strom manipulieren. Auch an der Qualität der Antwort lässt sich das laut Anthropic nicht zuverlässig erkennen. Anthropic betont, das Ergebnis sei ein Zwischenstand der Forschung und kein fertiges Produkt.

Veröffentlicht wurden fünf Artefakte: ein Blogbeitrag, ein technischer Bericht, eine (von Claude geschriebene) Protokollspezifikation, ausführbarer Code mit einem Beweiser und zwei Prüfern (schnell in C++, formal abgesichert in Lean) sowie Lean-Beweise der zentralen Aussagen samt interaktivem Visualisierer. Alles steht unter Apache 2.0 im GitHub-Repository anthropics/FlashProve. Beteiligt waren neben Anthropic-Leuten (Roy Rinberg, Alex Allain) Forschende von EPFL, MIT und aus dem Umfeld von StarkWare und Succinct.

So funktioniert FlashProve

Grundlage ist ein zkSNARK („zero-knowledge succinct argument of knowledge“). Das ist ein kryptografischer Beweis, mit dem eine Seite (der Beweiser) eine andere (den Prüfer) davon überzeugt, dass eine Berechnung korrekt lief. Dabei verrät der Beweis nichts über geheime Eingaben (zero-knowledge) und ist viel schneller zu prüfen als die Berechnung selbst (succinct). Die gleiche Technik wird in der Blockchain-Welt eingesetzt, etwa bei Layer-2-Netzen wie Starknet.

Der Ablauf hat zwei Phasen:

• Offline-Phase: Der Anbieter veröffentlicht eine „Commitment“, eine Art kurzer Fingerabdruck, der genau einen Satz Gewichte festlegt, während die Gewichte geheim bleiben. Sie dauert etwa 39 Minuten pro Modell, das Commitment ist rund 6,5 MB groß und reicht für etwa 16 Millionen Anfragen.
• Online-Phase: Zu Prompt und Antwort erzeugt der Anbieter eine Beweisdatei für die Aussage „Das festgelegte Modell erzeugt diese Ausgabe-Tokens“. Wer Commitment, Prompt und Antwort hat, kann das prüfen.

Vier Eigenschaften sollen gelten: Ehrliche Beweise werden akzeptiert (Vollständigkeit). Falsche Beweise lassen sich praktisch nicht fälschen, ohne gängige kryptografische Annahmen zu brechen (Korrektheit). Der Prüfer erfährt nichts über Gewichte, Zwischenwerte oder darüber, welche Experten pro Schicht liefen (Zero-Knowledge). Und der Beweis ist klein und billig zu prüfen (Succinctness). Die Architektur des Modells bleibt dagegen sichtbar; sie zu verbergen ist kein Ziel.

Das Verfahren ist hashbasiert, nutzt ein „interactive oracle proof“ und bietet laut Anthropic sogar Post-Quanten-Sicherheit. Es ist ein reiner Software-Ansatz. Anders als Lösungen mit vertrauenswürdiger Hardware (Trusted Execution Environments) hängt die Sicherheit nicht an einem Chiphersteller, sondern an der Schwierigkeit mathematischer Probleme. Anthropic sieht beide Ansätze als komplementär.

Zahlen und Benchmarks

Getestet wurde Llama 4 Maverick, ein Mixture-of-Experts-Modell (pro Token wird nur ein Teil der „Experten“-Teilnetze genutzt) mit rund 400 Mrd. Parametern, davon etwa 17 Mrd. aktiv pro Token, in öffentlich verfügbaren 4-bit-Gewichten (ca. 232 GB). Der Beweiser lief auf einem Server mit einer H100 und 24 CPU-Kernen.

Der Vergleich bezieht sich auf vLLM mit der FP8-Version des Modells auf acht H100; verglichen wurde pro GPU. Insgesamt nennt Anthropic 70 bis 95 Mal die GPU-Zeit.

Zum Vergleich mit früheren Arbeiten (Zahlen laut Anthropic): zkLLM bewies 2024 ein 13B-Modell mit etwa 2,5 Tokens/s im Batch. Die einzige bekannte frühere Arbeit zu Maverick, VerInf, brauchte 14,3 Stunden für 1.000 Tokens auf einem DGX Spark, mit einem 93,6 GB großen Beweis, dessen Prüfung fast einen Tag dauerte. Eine kommerzielle Firma, Attestable, berichtet 53–77 Tokens/s für Gemma 4 31B auf einer H100, hat dazu aber keine Open-Source-Bibliothek veröffentlicht.

Drei Konstruktionsentscheidungen machen das möglich: Der Aufwand skaliert mit den tatsächlich aktiven Experten (rund 17 Mrd. statt 400 Mrd.), ohne zu verraten, welche das waren. Anfragen werden nachträglich im Batch bewiesen, wobei das Commitment nur einmal pro Batch geöffnet wird. Und die Gewichte werden schichtweise aus dem Hauptspeicher gestreamt, sodass eine 80-GB-GPU plus etwa 290 GB Host-Speicher genügt.

Anwendungen und Vertrauen durch Lean

Anthropic nennt vier Anwendungsfelder:

• Pacing/Regulierung: Aufsichtsbehörden könnten Beweise verlangen, dass Hardware tatsächlich Inferenz bediente. Das belegt aber nicht, dass nebenbei nicht trainiert wird.
• Manipulationserkennung: Ein kompromittierter Server oder ein Modell, das sich als schwächeres ausgibt, könnte keine gültigen Beweise für die erwarteten Gewichte liefern. Anthropic hatte sich in seiner Frontier Safety Roadmap vorgenommen, bis 30. September 2026 einen Prototyp zu bauen; dieses Ziel sei über ein separates Projekt erreicht worden, das Traffic signiert und auf einem vertrauenswürdigen Server neu berechnet.
• Textherkunft: Etwa ein „Proof of Failure“, dass ein Modell mindestens eine Million Tokens aufwandte und keinen Fehler in einem Patch fand.
• Modellfreigabe: Regulierer könnten durchsetzen, dass nur zugelassene Modelle laufen.

Kryptografischer Code ist fehleranfällig, daher spezifiziert Anthropic Protokoll und Sicherheitseigenschaften im Beweisassistenten Lean (Vollständigkeit, Korrektheit, Zero-Knowledge, im Random-Oracle-Modell). Zwei Lücken bleiben: Die formalen Aussagen müssen manuell geprüft werden (dafür gibt es den Visualisierer), und der ausführbare Code muss dem Protokoll entsprechen. Für die Korrektheit zählt nur der Prüfer: Der Lean-Prüfer ist langsam, aber formal an den Korrektheitssatz gebunden. Der schnelle C++-Prüfer hat keine Garantie und stimmte in allen Tests mit dem Lean-Prüfer überein. Laut unite.ai halten die Projektunterlagen zudem fest, dass KI-Systeme unter menschlicher Leitung fast die gesamte Software, die Lean-Beweise und die Dokumentation schrieben, dass keine unabhängige Sicherheitsprüfung stattfand und dass Tests zu Gewichtsverbergung und Angriffsbeweisen begrenzt sind. Das Repository ist als nicht gepflegtes Forschungsartefakt (Version 0.16.0) gekennzeichnet und nimmt keine Beiträge an.

Einschränkungen

• Der Beweis gilt für eine exakte Integer-Version der Gewichte bei Greedy Decoding (immer das wahrscheinlichste Token). Antworten aus Gleitkomma-Implementierungen oder gesampelte Ausgaben können abweichen. Gegen speziell konstruierte Prompts ist das nicht getestet.
• Das System setzt eine MoE-Architektur voraus und nutzt sie für Effizienz; dichte Modelle sind nicht abgedeckt.
• Kontexte sind auf 1.024 Tokens begrenzt, viel weniger als in Chat-Szenarien üblich.
• Seitenkanalangriffe wie das Messen der Beweiszeit sind ausdrücklich nicht abgedeckt.
• Nachträgliches Beweisen bringt Neuberechnung, verzögerte Garantien und Nicht-Determinismus mit sich.
• Code, Paper und Lean-Protokoll müssen nicht exakt übereinstimmen.

Was du zum Ausprobieren brauchst

Für Heimanwender ist das nichts: Der Beweiser benötigt laut Quelle eine 80-GB-GPU (H100), 24 CPU-Kerne und rund 290 GB Arbeitsspeicher, dazu die Maverick-Gewichte mit etwa 232 GB. Das Prüfen läuft dagegen auf einer normalen Mehrkern-CPU ohne GPU in Sekunden. Es ist ein Forschungsartefakt für Entwickler und Kryptografie-Interessierte, kein Tool für den Alltag.

Einordnung

FlashProve zeigt, dass kryptografische Beweise für ein Modell der 400-Milliarden-Klasse auf einer einzelnen GPU praktikabel werden. Der Sprung gegenüber früheren offenen Systemen ist gewaltig (Faktor 5.000 und mehr gegenüber VerInf), wobei die Zahlen von Anthropic stammen und laut BigGo noch nicht unabhängig reproduziert wurden. Für den Alltag ist es dennoch weit entfernt: 70- bis 95-facher Aufwand und 19 MB pro Anfrage taugen eher für Stichproben und Audits als für jede Interaktion. Dazu kommen die enge Greedy-Integer-Annahme, die 1.024-Token-Grenze und die fehlende Unabhängigkeit der Prüfung. Interessant ist es für unabhängige Evaluatoren, Anbieter von Routing-Diensten und Regulierungsansätze, für die ein nachprüfbarer Modellnachweis bislang fehlt. Dass Claude große Teile der Entwicklung übernahm, ist bemerkenswert, macht aber die formale Verifikation umso wichtiger. Anthropic nennt keinen Zeitplan und keine Kommerzialisierungspläne.