Anthropic ver­öf­fent­licht mit FlashProve einen For­schungs­pro­totyp, der kryp­to­gra­fisch belegt, welches Modell geant­wortet hat

Anthropic hat am 2. November FlashProve veröffentlicht, einen quelloffenen For­schungs­pro­totyp, mit dem ein Anbieter belegen kann, welches Modell eine Anfrage beantwortet hat. Die Gewichte des Modells bleiben dabei geheim. Das Verfahren hat drei Schritte. Zuerst veröffentlicht der Anbieter eine Kennung, die ihn an einen festen Satz Gewichte bindet; jeder veröffentlichte Wert, der von ihnen abhängt, ist maskiert, bis auf eine ausdrücklich erklärte Liste. Dann erzeugt seine GPU zu jeder Antwort einen Beweis, dass sie die Ausgabe genau dieses Modells ist. Diesen Beweis prüft jeder mit dem Programm cp_verify auf einer gewöhnlichen CPU in Sekunden, ohne die Gewichte zu kennen.

Am Text der Antwort ist das Modell nicht zu erkennen

Wer heute ein Modell abfragt, kann nicht prüfen, ob die Antwort wirklich vom zugesagten Modell stammt. Ein Routing-Dienst könnte aus Kostengründen ein anderes unterschieben, ein Angreifer den Strom der Token unterwegs verändern. An der Qualität der Antwort lässt sich das nach Einschätzung der Autoren nicht zuverlässig ablesen, auch wenn sie gut ist. Nachrechnen scheitert an zwei Dingen: Die Gewichte der meisten führenden Modelle sind privat, und wer sie hätte, bräuchte für den Abgleich mehr Rechenleistung, als ein Nutzer oder auch eine Prüfstelle aufbringen kann. Gebraucht würde der Nachweis von Prüfern, die ein Modell vor und nach der Veröffentlichung testen und wissen müssen, dass im Betrieb dasselbe läuft, und von Kunden eines Routing-Dienstes, die das bezahlte Modell bekommen wollen. Die Autoren nennen außerdem Vorgaben zum Entwicklungstempo der KI, deren Einhaltung ein Anbieter so belegen könnte.

Ein Beweis für 400 Milliarden Parameter auf einer H100

Das Werkzeug dafür war bekannt: ein kryptografischer Beweis der Bauart zkSNARK. Der Anbieter schickt mit der Antwort einen kurzen Beweis von einigen Megabyte, den der Nutzer schnell prüft; weicht die Antwort vom festgelegten Modell ab, schlägt die Prüfung fehl, und über die Gewichte verrät der Beweis nichts. Bisher galt das für große Sprachmodelle als zu langsam, und die bisherigen quelloffenen Systeme liegen nach Angabe des Berichts um Größenordnungen hinter dem jetzigen Stand. Die Verbesserungen hat Claude erarbeitet, indem es aktuelle Werkzeuge aus der Kryptografie auf neue Art anwandte und sich dabei an bewährte Bauprinzipien für Beweissysteme hielt.

Getestet ist das an Metas Llama 4 Maverick in voller Größe, einem Modell mit 400 Milliarden Parametern in der Bauform Mixture of Experts, mit Gewichten in 4 Bit und einem Kontextfenster von 1.024 Token. Eine einzelne H100 erzeugt Beweise mit rund 110 Token pro Sekunde, bei 24 Anfragen je Stapel und mit Ganz­zahl­arith­metik im Prefill, auf den sich diese Rate bezieht. Ein Beweis für eine Anfrage von 1.024 Token ist etwa 19 MB groß. Gleich daneben nennt der Bericht den Aufwand: Das Beweisen kostet das 70- bis 95-Fache der GPU-Zeit, die das Modell selbst unter vLLM braucht, einer verbreiteten quelloffenen Bibliothek, mit der man Modelle laufen lässt.

Lean 4 prüft, was Claude gebaut hat

Dass Claude das System gebaut hat, sehen die Autoren selbst als Risiko: Claude beschleunige gut, treffe in großen, verwickelten Systemen aber oft Entscheidungen, die sich schwer beurteilen lassen. Dagegen setzen sie Aussagen auf oberster Ebene in Lean, einer Sprache für formale Verifikation, die ein Prüfer nachlesen kann. Belegt ist dort die Zuverlässigkeit des Protokolls: Ein Anbieter, der fremde Ausgabe als die des zugesagten Modells ausgibt, fliegt auf, außer mit einer Wahr­schein­lich­keit von etwa q geteilt durch 2 hoch 124 plus 2 hoch minus 101 nach q Hash-Abfragen. Neben Beitrag, technischem Bericht und einer von Claude geschriebenen Pro­to­koll­be­schrei­bung liegen ein Beweiser und zwei Prüfprogramme bei, ein schnelles in C++ und ein nachweislich korrektes in Lean, dazu eine interaktive Darstellung der Lean-Sätze für die Prüfung. Alles steht unter der Lizenz Apache 2.0. Sichtbar bleibt der Aufbau des Modells, das System soll allein die Gewichte schützen.

FlashProve ist laut README ein For­schungs­ar­te­fakt in Version 0.16.0: Es wird nicht gepflegt und nimmt keine Beiträge an, und der Beitrag versteht sich als Zwischenstand, den andere übernehmen und verbessern sollen. Der Beweiser läuft nur auf Linux, mit einer H100 mit 80 GB, die nichts anderes tut, und mit CUDA 13.2. Wer die echten Gewichte von Maverick einsetzt, lädt eine öffentliche Umwandlung in 4 Bit von 232 GB, braucht 330 GB Arbeitsspeicher und wartet Stunden auf den Beweis für ein einzelnes Token. Einen mitgelieferten Beispielbeweis zu prüfen, geht auf einem gewöhnlichen Rechner; das Repository richtet sich dafür an Coding-Agenten, weil Bauen und Prüfen lange Bauläufe und viele exakte Vergleiche verlangen.

Offen bleibt die Stelle, an der das Vertrauen wieder hereinkommt. Der Beweis bindet eine Antwort an die Kennung, die Kennung an einen Satz Gewichte. Welches Modell hinter dieser Kennung steht, muss der Nutzer anderswoher wissen: Die README verlangt, die Kennung von einer Stelle zu beziehen, der er vertraut, nie vom geprüften Server und nie aus Dateien, die mit dem Beweis kommen. Vorgeführt ist das Verfahren an einem offenen Modell von Meta, mit einem Kontextfenster von 1.024 Token und mit Kosten, die das Beweisen um ein Vielfaches teurer machen als das Antworten.

Einordnung

Die Lücke, die FlashProve schließen will, besteht bei jedem Zugang über einen Zwischenhändler oder Routing-Dienst: Welches Modell geantwortet hat, steht dort nur in der Zusage des Betreibers. Bis Verfahren dieser Art bezahlbar werden, bleiben die Wahl des Betreibers und seine schriftliche Zusage die eigentliche Absicherung. Was ein Betreiber zusagt und warum zu demselben Modell je nach Betreiber eine andere Zusage gehört, beschreibt Beurteilen und Einordnen, Kapitel 01.