KI-Modelle und Plattformen
Anthropic veröffentlicht FlashProve für kryptografische Nachweise der KI-Inferenz
Unite.AI zu deinen bevorzugten Quellen auf Google hinzufügen
Anthropic veröffentlichte FlashProve am 2. November 2026: einen quelloffenen Forschungsprototyp, der kryptografische Nachweise verwendet, um zu belegen, dass eine Antwort eines Sprachmodells mit den gebundenen Gewichten erzeugt wurde, ohne diese offenzulegen. Das Unternehmen gab an, dass für Meta’s Llama 4 Maverick Nachweise mit einer Geschwindigkeit von 110 Tokens pro Sekunde erstellt wurden.
Die Arbeit schließt eine Verifikationslücke bei gehosteter KI. Eine hochwertige Antwort belegt nicht, welches Modell sie erzeugt hat: Ein Routingdienst könnte ein anderes System einsetzen, ein Evaluator könnte ein anderes Modell als das für den Test vorgesehene erhalten oder ein Angreifer könnte den Tokenstrom verändern. Für Nutzer ist es unpraktisch, das Modell erneut auszuführen, um die Antwort zu überprüfen, wenn die Gewichte privat sind und erhebliche Hardwareanforderungen bestehen.
Antworten an verborgene Gewichte binden
FlashProve verwendet in einem rein softwarebasierten Design ein wissenskompaktes Zero-Knowledge-Beweisargument, auch zkSNARK genannt, statt auf vertrauenswürdige Hardware angewiesen zu sein. In einer Offline-Phase veröffentlicht der Anbieter ein kurzes Commitment, das einen ganz bestimmten Gewichtsatz identifiziert, ohne die Gewichte offenzulegen. Für abgeschlossene Paare aus Prompt und Antwort erzeugt das System einen Nachweis, dass die Ausgabetokens vom durch das Commitment gebundenen Modell stammen. Jeder, der über das Commitment, den Prompt und die Antwort verfügt, kann den Nachweis überprüfen, ohne Zugriff auf die Gewichte zu haben.
Zu den angestrebten Eigenschaften gehören Vollständigkeit, Unfälschbarkeit, Zero Knowledge und Kompaktheit. Ein ehrlicher Nachweis sollte akzeptiert werden; eine falsche Aussage zu zertifizieren, sollte dagegen voraussetzen, weithin als gültig angesehene kryptografische Annahmen zu brechen. Bei der Überprüfung eines Nachweises sollten weder die Gewichte noch Zwischenwerte der Berechnung offengelegt werden. Das Design verbirgt außerdem, welche Teilnetze des Mixture-of-Experts-Modells für jedes Token ausgeführt wurden, während die Architektur des Modells selbst sichtbar bleibt.
Die Implementierung nutzt die Mixture-of-Experts-Struktur von Maverick. Der Rechenaufwand für die Beweiserstellung skaliert mit den rund 17 Milliarden Parametern, die für ein Token aktiv sind, statt mit allen 400 Milliarden, und verbirgt dabei weiterhin die Auswahl der Experten. Die segmentierten Gewichte werden aus dem Host-Speicher gestreamt, sodass die Beweiserstellung auf einer einzelnen GPU mit 80 GB und zusätzlich rund 290 GB Host-Speicher möglich ist.
Anthropic nennt Integritätsprüfungen für Kunden, unabhängige Evaluierungen, regulatorische Werkzeuge und die Durchsetzung von Vorgaben zur Verwendung zugelassener Modelle als mögliche Anwendungsbereiche. Inferenz-Zertifikate könnten belegen, dass Anfragen von einem bestimmten Modell bearbeitet wurden. Sie würden jedoch nicht nachweisen, dass dieselbe Hardware nicht gleichzeitig auch zum Training eines anderen Modells verwendet wurde. Diese Unterscheidung schränkt ein, was solche Zertifikate über Compliance-Anforderungen aussagen könnten, die davon abhängen, wie die Rechenkapazität genutzt wird.
Leistung der Nachweiserstellung und zusätzlicher Aufwand bei der Inferenz
Für die Evaluierung verwendete Anthropic eine öffentlich verfügbare 4-Bit-Konvertierung des Modells. Ein Server mit einer H100 und 24 CPU-Kernen erstellte für einen Stapel von 24 Anfragen in rund 223 Sekunden Nachweise; jeder Nachweis war 18,78 MB groß. Die Offline-Phase zur Erstellung des Commitments dauerte rund 39 Minuten.
Für die Überprüfung lädt der Client ein Commitment von etwa 6,5 MB herunter und prüft die Nachweise auf einer CPU ohne GPU. Anthropic maß für die Verifizierung 17 Sekunden mit 24 Threads und 21 Sekunden mit einem Thread, einschließlich der Prüfungen der Offline-Phase.
Diese Messwerte stellen einen reinen CPU-Prüfvorgang einem deutlich aufwendigeren Vorgang zur Nachweiserstellung gegenüber. Im Vergleich von Anthropic mit einer FP8-Inferenz auf acht H100, auf denen vLLM lief, erforderte die Nachweiserstellung für denselben Stapel pro GPU etwa 72-mal so viel Rechenzeit und bei der höchsten getesteten vLLM-Auslastung etwa 94-mal so viel. Der Durchsatz ist somit mit erheblichen Kosten verbunden, verglichen mit der Bereitstellung des Modells ohne Nachweise.
Formale Verifizierung und praktische Grenzen
Das FlashProve-Repository umfasst einen Prover, einen schnellen C++-Verifier, einen langsameren Lean-Verifier, Lean-Beweise für mathematische Aussagen auf oberster Ebene sowie einen interaktiven Theorem-Visualisierer. Es steht unter der Apache-2.0-Lizenz. Version 0.16.0 wird als nicht gewartetes Forschungsartefakt bezeichnet, für das keine Beiträge angenommen werden.
Die Arbeit mit Lean behandelt Vollständigkeit, Unfälschbarkeit und Zero Knowledge im Random-Oracle-Modell. Die formalen Aussagen müssen weiterhin manuell überprüft werden, um sicherzustellen, dass sie die beabsichtigten Garantien ausdrücken. Der Lean-Verifier ist formal mit dem Unfälschbarkeitssatz verknüpft. Für den C++-Verifier, der für den Routineeinsatz vorgesehen ist, gibt es dagegen keine formale Garantie; stattdessen wurde geprüft, ob er mit dem Lean-Verifier übereinstimmt.
In der Dokumentation zu bekannten Einschränkungen des Projekts steht, dass KI-Systeme unter menschlicher Anleitung nahezu die gesamte Software, die Lean-Beweise und die Dokumentation verfasst sowie die gemeldeten Tests ausgeführt haben. Es gab kein unabhängiges Sicherheitsaudit, und die Tests zum Verbergen der Gewichte sowie zu adversarialen Beweisen sind weiterhin begrenzt.
Die Nachweise decken eine exakte ganzzahlige Version der Gewichte bei Greedy Decoding ab. Inferenz mit Fließkommazahlen oder Decoding mit Stichproben kann von der nachgewiesenen Berechnung abweichen, und die allgemeinen Fehlertests decken keine gezielt adversarial gestalteten Prompts ab. Der Kontext ist auf 1.024 Tokens begrenzt; Angriffe über Laufzeitmessungen und andere Seitenkanäle fallen nicht unter die Garantie. Eine nachträgliche Beweiserstellung führt im Vergleich zur Beweiserstellung während der Inferenz außerdem zu erneuten Berechnungen, verzögerten Zusicherungen und Nichtdeterminismus.
Damit sich nachweisbare Inferenz zu einer Routineprüfung der tatsächlich ausgelieferten Anfragen entwickelt, konzentriert sich die verbleibende Arbeit auf die Lücken, die diese Veröffentlichung aufzeigt: die Kosten für die Nachweiserstellung zu senken, weniger restriktive Decodierverfahren und längere Kontexte abzudecken und die schnelle Implementierung enger mit dem formalen Protokoll zu verknüpfen.
