FlashProve: Wie Anthropic kryptographische Beweise für KI-Inferenz voranbringt

Quellcode auf einem grossen Monitor in einem abgedunkelten Raum, warmes Licht einer Schreibtischlampe
Deine Reaktion:

Ein Prüfer einer Aufsichtsbehörde öffnet an einem Montagmorgen eine Datei von 19 Megabyte. Darin steht kein Zwischenstand der Modellgewichte, kein Serverprotokoll und keine Abrechnung über GPU-Stunden, sondern eine Zahlenkette, die sich in Sekunden auf einem gewöhnlichen Prozessor nachrechnen lässt. Sie soll belegen, dass die Antworten, die ein Anbieter in der vergangenen Woche ausgeliefert hat, von dem Modell stammen, das dieser Anbieter angegeben hat.

Das ist kein Formalienproblem. Ein Team um Roy Rinberg und Alex Allain von Anthropic beschreibt in einem jetzt veröffentlichten Bericht, wie sich diese Lücke schließen lässt: mit kryptographischen Beweisen für KI-Inferenz, also einem Verfahren, bei dem der Anbieter für jede Antwort einen prüfbaren Beleg mitliefert. Wenn du heute eine Anfrage an ein Modell schickst, hast du kaum eine Möglichkeit zu erkennen, ob wirklich das Modell antwortet, das dir versprochen wurde – oder eine billigere Variante, die ein Routing-Dienst dazwischengeschaltet hat.

Der Beitrag ist als Zwischenstand markiert, nicht als fertiges Programm. Er zeigt, wie weit die Verfahren sind, was sie kosten und welche Fragen offenbleiben.

Warum eine Antwort nicht verrät, von welchem Modell sie stammt

Die Qualität einer Antwort sagt nichts über ihre Herkunft. Ein Modell kann gut formulieren und trotzdem nicht das sein, das der Anbieter zugesagt hat. Drei Fälle nennt der Bericht. Ein Routing-Dienst könnte aus Kostengründen stillschweigend ein kleineres Modell einsetzen. Ein Angreifer könnte den Token-Strom auf dem Weg zum Nutzer verändern. Oder ein fähigeres Modell könnte sich als schwächeres ausgeben, um Klassifikatoren und Überwachung zu umgehen.

Die naheliegende Lösung – einfach die Gewichte veröffentlichen und den Nutzer nachrechnen lassen – scheitert an zwei Dingen. Erstens sind die Gewichte kommerziell sensibel. Zweitens bräuchte man für die Prüfung einer einzigen Antwort ungefähr so viel Rechenleistung wie für ihre Erzeugung. Für einen einzelnen Nutzer oder einen unabhängigen Prüfer ist das nicht leistbar.

Hier setzt nachweisbare Inferenz an: Eine Person mit begrenzter Rechenleistung und ohne Wissen über die Gewichte soll überprüfen können, dass eine Antwort aus dem angeforderten Modell stammt. Der Anbieter legt dazu zusammen mit der Antwort einen kurzen Beweis vor, der sich schnell prüfen lässt. Weicht die Antwort vom angegebenen Modell ab, schlägt die Prüfung fehl. Die Grundidee ist älter als die Sprachmodelle – neu ist der Versuch, sie auf Modelle dieser Größe anzuwenden.

Was ein zkSNARK leistet – die Quittung, die nichts über den Laden verrät

Das Verfahren heißt zkSNARK, ein zero-knowledge succinct argument of knowledge. Der Begriff ist lang, die Sache lässt sich an einer Quittung erklären. Wer eine Rechnung bezahlt, bekommt einen Kassenzettel, der belegt, dass ein Geschäft mit diesen Posten zu diesem Preis abgerechnet wurde. Der Zettel beweist die Transaktion, ohne die Rezeptur der Ware preiszugeben.

Ein zkSNARK funktioniert ähnlich, nur strenger. Ein Beweiser überzeugt einen Prüfer davon, dass eine bestimmte Berechnung korrekt ausgeführt wurde, und zwar mit einem Beleg, der zwei Eigenschaften hat. Er ist zero-knowledge, verrät also nichts über die Eingaben jenseits der bloßen Korrektheit – hier: nichts über die Modellgewichte. Und er ist succinct, das heißt exponentiell schneller zu prüfen als nachzurechnen. Für die Praxis heißt das: Der Prüfer braucht weder Spezialhardware noch Zugang zum Modell.

Der Beweis hat eine Grenze. Er bindet sich an eine Festlegung, ein Commitment, auf die Gewichte des Modells. Er verbirgt diese Gewichte, aber er verbirgt nicht die Architektur. Wer wissen will, ob das richtige Modell läuft, bekommt eine Antwort. Wer wissen will, wie es gebaut ist, bekommt keine.

FlashProve: die Zahlen hinter dem Prototyp

Das System, das die Autoren vorstellen, heißt FlashProve. Für Llama 4 Maverick, ein Modell mit 400 Milliarden Parametern in Mixture-of-Experts-Bauweise, erzeugt eine einzelne H100-GPU Beweise für etwa 110 Token pro Sekunde, bei 4-Bit-quantisierten Gewichten und Ganzzahl-Arithmetik im Prefill. Ein Beweis für eine Anfrage über 1.024 Token ist rund 19 Megabyte groß.

Das ist das 70- bis 95-Fache der GPU-Zeit, die vLLM, eine verbreitete Open-Source-Bibliothek, für dieselbe Anfrage benötigt. Man zahlt also fast zwei Größenordnungen mehr Rechenzeit, um einen Beweis zu erhalten. Frühere Open-Source-Systeme liegen laut Bericht um Größenordnungen darüber. Der Fortschritt kommt weniger von einem neuen Trick als von der konsequenten Anwendung bekannter kryptographischer Werkzeuge.

Auch der Entstehungsweg ist ungewöhnlich. Claude selbst hat laut Bericht wesentliche Verbesserungen an den zkSNARK-Verfahren für die Inferenz erarbeitet, während das Team die Designentscheidungen traf. Veröffentlicht ist alles unter der Apache-2.0-Lizenz, zusammen mit einem technischen Bericht, einer von Claude geschriebenen Protokollspezifikation, ausführbarem Code mit zwei Verifizierern und den formalen Beweisen. Wer nachbauen will, muss nicht bei null anfangen.

Lean-Beweise für KI-Sicherheit: die zweite Ebene der Kontrolle

Ein Modell, das schnell optimiert und knapp begründet, erzeugt ein eigenes Prüfproblem. Die Autoren schreiben selbst, solche Entscheidungen seien oft schwer zu bewerten, besonders in großen, komplexen Systemen. Ein Beweis auf Basis eines unklaren Arguments ist als Sicherheitszusage wenig wert.

Dazu kommt eine zweite Ebene. Die zentralen Sicherheitsaussagen des Systems sind in Lean formuliert, einer Sprache, in der jede Behauptung maschinell geprüft wird. Dazu liefert das Team zwei Verifizierer: einen schnellen in C++ und einen, dessen Korrektheit selbst in Lean bewiesen ist. Ein interaktiver Visualisierer soll das Audit der Theoreme erleichtern. Lean-Beweise für KI-Sicherheit sind hier kein Forschungsziel, sondern Teil eines Inferenz-Prototyps.

Der Gewinn ist verschobenes Vertrauen. Man muss dem Team nicht glauben, dass sein System die zugesagten Eigenschaften hat. Man kann die Aussage selbst nachprüfen. In einem Feld, in dem Anbieter über ihre eigenen Systeme berichten, macht das einen Unterschied.

Drei Anwendungsfälle: Pacing, Manipulationsschutz, Herkunft von Text

Der Bericht nennt drei Szenarien. Im ersten geht es um die Steuerung des Entwicklungstempos. Wenn ein Anbieter verpflichtet wird, seine Hardware für Inferenz statt für das Training eines neuen Modells einzusetzen, könnte er versuchen, diese Zusage zu unterlaufen. Eine Aufsichtsbehörde könnte Zertifikate über die abgewickelten Anfragen anfordern; ohne dass das angegebene Modell tatsächlich läuft, lassen sie sich nicht erzeugen. Die Autoren räumen ein, dass damit nicht bewiesen ist, dass die Hardware nicht nebenbei trainiert.

Im zweiten Szenario geht es um Manipulation. Wird ein Inferenzserver kompromittiert, kann ein Angreifer Schadsoftware an Nutzer ausliefern und sich zwischen echten Antworten verstecken. Ein Beweis, der an das Commitment der Gewichte gebunden ist, zertifiziert nicht irgendein Modell, sondern das festgelegte. Wer unterschieben will, müsste gültige Beweise für die erwarteten Gewichte liefern, was er nicht kann. Anthropic verweist in diesem Zusammenhang auf ein Ziel aus der eigenen Frontier-Safety-Roadmap, das über ein separates Projekt erreicht wurde: das Signieren des Inferenzverkehrs mit Neuberechnung auf einem vertrauenswürdigen Server.

Im dritten Szenario geht es um die Herkunft von Text. Ein Entwickler behauptet, seine Bibliothek sei von einem Frontier-Modell auf Schwachstellen geprüft worden. Chat-Protokolle lassen sich fälschen, und ein billigeres Modell kann sie ebenso erzeugen. Ein mitgelieferter zkSNARK macht die Behauptung überprüfbar, ohne dass der Prüfer das Modell laufen lassen oder Zugang zu den Gewichten haben muss.

Was das praktisch bedeutet

Der Aufschlag bleibt der erste Punkt: 70- bis 95-mal so viel GPU-Zeit pro Anfrage ist kein Wert, mit dem man jeden Consumer-Chat absichern wird. Kryptographische Beweise für Large Language Models bleiben vorerst ein Instrument für Stichproben, Audits und regulierte Kontexte. Dort sind sie brauchbar.

Entscheidend ist etwas anderes. Bisher hing die Prüfbarkeit einer Modellantwort an der Rechenleistung des Prüfers. Ein zkSNARK trennt beides: Wer prüft, muss nicht rechnen; wer rechnet, muss nichts preisgeben. Diese Trennung ist der wichtigere Punkt, nicht die einzelne Zahl im Benchmark.

Eine Grenze bleibt. Ein Beweis sagt, dass eine Antwort aus dem festgelegten Modell stammt. Er sagt nichts darüber, ob diese Antwort richtig, hilfreich oder sicher ist. Modellverifikation und Qualitätsurteil sind zwei verschiedene Dinge. Wer sie verwechselt, schreibt der Kryptographie mehr zu, als sie leistet. FlashProve beantwortet die erste Frage. Für die zweite braucht es weiterhin Menschen, die hinschauen.

Quelle: anthropic.com

Deine Reaktion:
Artikel teilen:
Krötzsch-Check0 — 100
Fakten 80
Relevanz 85
Hype 25
Einschätzung 75
Redaktion 50 Stand 50 · noch keine Stimmen
Ist das Hype?
Sebastian Krötzsch
Autor

Sebastian Krötzsch

Sebastian Krötzsch schreibt auf sebask.de über Künstliche Intelligenz, Automatisierung, digitale Systeme und die Frage, was davon im Alltag wirklich nützlich ist. Ohne Buzzword-Nebel, dafür mit klarem Blick auf Praxis, Tools und echte Wirkung.