FlashProve: Anthropic will die Identität von KI-Modellen kryptografisch nachweisen

Wer eine KI über einen Vermittlungsdienst anspricht, muss derzeit weitgehend darauf vertrauen, dass tatsächlich das bestellte Modell antwortet. Am 2. November hat Anthropic mit FlashProve einen offenen Forschungsprototyp vorgestellt, der für einzelne Antworten einen kryptografischen Nachweis erzeugen soll. Dieser lässt sich prüfen, ohne die Modellgewichte zu besitzen oder das Modell selbst auszuführen. Das Unternehmen hat dazu Code, eine Protokollbeschreibung und formale Beweise veröffentlicht. FlashProve ist allerdings weder ein Dienst für Claude-Anfragen noch eine fertige Absicherung beliebiger Chatverläufe. (Anthropic; Projekt-Repository)

Was wird eigentlich bewiesen?

Zuerst legt sich der Betreiber auf einen bestimmten Satz von Modellgewichten fest und veröffentlicht dafür eine kryptografische Bindung, ein sogenanntes Commitment. Später erzeugt sein Server zu einer Anfrage und dem geprüften Ausgabetoken einen Beweis. Ein Prüfer kann anhand des Commitments, der Eingabe und der Ausgabe kontrollieren, ob die festgelegten Gewichte genau dieses Token berechnen würden. Die Gewichte selbst bleiben verborgen. Das Verfahren beruht auf einem Zero-Knowledge-Beweis vom Typ zkSNARK: Statt die aufwendige Rechnung zu wiederholen, kontrolliert der Prüfer einen wesentlich kleineren Beleg für deren korrekte Ausführung. Verlässlich ist die Identitätsaussage nur, wenn auch bekannt ist, welchem Modell das veröffentlichte Commitment zugeordnet wurde. (Anthropic; FlashProve)

Das ist für Unternehmen interessant, die Modelle über Drittanbieter beziehen oder besonders wichtige Ausgaben nachvollziehen müssen. Ein kryptografischer Nachweis könnte etwa verhindern, dass ein Dienst unbemerkt ein anderes Modell unter dem Namen des vereinbarten Modells ausliefert. Er beurteilt aber nicht, ob eine Antwort sachlich richtig, sicher oder für eine bestimmte Aufgabe geeignet ist. (Anthropic)

Große Modelle, aber kleine Prüffälle

Anthropic hat FlashProve mit einer öffentlich verfügbaren, auf vier Bit quantisierten Fassung von Llama 4 Maverick erprobt. Das Mixture-of-Experts-Modell hat insgesamt rund 400 Milliarden Parameter, nutzt für ein Token aber nur einen Teil seiner Experten. Genau daraus zieht das Beweissystem einen Vorteil: Es muss die tatsächlich genutzten Experten prüfen und nicht bei jedem Token sämtliche Modellparameter verarbeiten. Llama 4 Maverick dient hier als dokumentierter technischer Prüffall, nicht als Empfehlung für ein derzeitiges Spitzenmodell. Die Modellgewichte gehören nicht zur FlashProve-Veröffentlichung. (Anthropic; Repository)

In Anthropics Messung bearbeitete der Beweiserzeuger auf einer H100-GPU eine Gruppe von 24 Anfragen in rund 223 Sekunden. Das entspricht nach Herstellerangaben etwa 110 Token pro Sekunde beim parallelen Verarbeiten der Eingaben; pro Anfrage wird dabei ein Ausgabetoken geprüft, nicht ein kompletter generierter Text. Jeder Beleg ist rund 18,78 MB groß. Die Prüfung dauerte auf der verwendeten CPU 17 Sekunden mit 24 Threads beziehungsweise 21 Sekunden mit einem Thread. Der Vergleich mit vLLM ergab je GPU einen ungefähr 70- bis 95-fachen Zeitaufwand für die Beweiserzeugung. Die Vergleichsläufe verwendeten zudem andere Gewichtsformate und Hardwarekonfigurationen: Der Wert beschreibt den gemessenen Aufwand, nicht einen austauschbaren Preis pro produktiver Chatantwort. (Anthropic, Evaluation)

Warum das noch kein Siegel für ganze Chats ist

FlashProve prüft derzeit Kontexte von höchstens 1.024 Token und in der beschriebenen Messung jeweils nur ein Token einer Anfrage. Das System erzeugt die Nachweise nachträglich und in Gruppen. Wer eine längere Antwort sofort beim Empfang vollständig verifizieren will, bekommt damit noch keine Lösung. Hinzu kommt eine mathematische Einschränkung: Der Beweis gilt für eine exakte ganzzahlige Modellrechnung mit deterministischer Auswahl des wahrscheinlichsten nächsten Tokens. Übliche Fließkomma-Inferenz oder eine zufallsbasierte Tokenauswahl können davon abweichen. (Anthropic, Grenzen und Messaufbau)

Auch der Sicherheitsnachweis hat einen klaren Geltungsbereich. Anthropic beschreibt formale Beweise in Lean und stellt neben dem schnellen C++-Prüfer eine ausführbare Lean-Version bereit. Die Autoren weisen jedoch darauf hin, dass der schnelle Programmcode nicht selbst formal als identisch zum bewiesenen Protokoll abgesichert ist. Zudem ist der Prototyp auf Mixture-of-Experts-Architekturen zugeschnitten. Das Repository bezeichnet die Veröffentlichung ausdrücklich als nicht gepflegtes Forschungsartefakt; wer sie produktiv einsetzen will, müsste die Implementierung prüfen, weiterentwickeln und den Betrieb selbst absichern. (Anthropic, formale Verifikation und Grenzen; FlashProve-Repository)

Fazit

FlashProve zeigt an einem großen Sprachmodell, dass sich die Identität einer Modellrechnung kryptografisch belegen lässt, ohne die Gewichte offenzulegen. Für Audits und Modellvermittlung ist das ein wichtiger technischer Baustein. Von einem allgemein einsetzbaren Echtheitsnachweis für KI-Antworten trennen den Prototyp jedoch noch lange Kontexte, vollständige Antworten, realistische Dekodierverfahren und erhebliche Betriebskosten. (Anthropic)

Quellen

Nach oben scrollen