Anthropic aus den USA veröffentlicht FlashProve, ein Verifikationssystem für die Inferenz großer Modelle

de.wedoany.com-Bericht: Am 2. November veröffentlichte das US-amerikanische KI-Unternehmen Anthropic die Forschungsergebnisse FlashProve zur verifizierbaren Inferenz großer Sprachmodelle. Dabei wird die Technik der Zero-Knowledge Succinct Non-Interactive Argument of Knowledge (zkSNARK) eingesetzt, um für den Inferenzberechnungsprozess eines bestimmten Modells einen kryptografischen Beweis zu erzeugen. Das Forschungsteam führte Tests auf dem Mixture-of-Experts-Modell Llama 4 Maverick mit insgesamt etwa 400 Milliarden Parametern durch und erreichte unter bestimmten Batch-Verarbeitungsbedingungen einen Beweiserzeugungsdurchsatz von etwa 110 Token pro Sekunde bei einer Größe der einzelnen Beweisdatei von etwa 18,78 Megabyte. Der technische Bericht, die Protokollspezifikation und der zugehörige Code wurden veröffentlicht.

Die Forschung verwendet das von Meta entwickelte Modell Llama 4 Maverick, bei dem pro Token tatsächlich etwa 17 Milliarden Parameter aktiviert werden. Für die Tests wurden öffentlich verfügbare 4-Bit-quantisierte Modellgewichte verwendet, das Kontextfenster einer einzelnen Inferenz auf 1024 Token festgelegt und für den Berechnungsprozess eines daraus erzeugten Tokens ein Beweis erstellt. Das System bindet das Verifikationsergebnis über einen Modellgewichts-Commitment-Mechanismus an die spezifischen Modellparameter.

Der Beweiserzeugungsserver von FlashProve ist mit einer NVIDIA H100 GPU und 24 CPU-Kernen ausgestattet. Der Initialisierungsprozess des Modellgewichts-Commitments dauert etwa 39 Minuten; für den Online-Test wurde eine Batch-Aufgabe aus 24 Anfragen verwendet, deren Beweiserzeugung etwa 223 Sekunden benötigt. Unter diesen Testbedingungen erreicht das System einen Beweiserzeugungsdurchsatz von etwa 110 Token pro Sekunde; dieser Wert gibt nicht die tatsächliche Textgenerierungsgeschwindigkeit des Modells wieder.

Jede kryptografische Beweisdatei ist etwa 18,78 Megabyte groß, die Modellgewichts-Commitment-Daten umfassen etwa 6,5 Megabyte. Das Forschungsteam berechnet, dass ein einzelnes Modellgewichts-Commitment etwa 16 Millionen Anfragen unterstützen kann. Der Verifikationsprozess benötigt keine GPU; in einer 24-Thread-CPU-Umgebung beträgt die Verifikationszeit für einen einzelnen Beweis etwa 17 Sekunden, unter Single-Thread-Bedingungen etwa 21 Sekunden.

Das Forschungsteam führte mit dem Inferenz-Framework vLLM Leistungsbenchmarks für dasselbe Modell durch. Die Testergebnisse zeigen, dass die für die FlashProve-Beweiserzeugung benötigte GPU-Rechenzeit pro Einheit etwa das 70- bis 95-Fache der gewöhnlichen Modellinferenz beträgt. Das System verwendet Batch-Verarbeitung sowie die Erzeugung des Beweises nach Abschluss der Inferenz; die entsprechenden Leistungsdaten stammen aus der vom Forschungsteam festgelegten experimentellen Umgebung.

Bei der Rechenressourcenkonfiguration setzt FlashProve auf ein segmentiertes Verarbeitungsschema für Modellgewichte, bei dem die Gewichte großer Modelle im Hauptspeicher des Hosts gespeichert und je nach Rechenaufgabe batchweise an die GPU übertragen werden. Das Testsystem verfügt über 80 GB Grafikspeicher und etwa 290 GB Hauptspeicher und führt die Beweiserzeugung für die Berechnungen des 400-Milliarden-Parameter-Modells mit einer einzelnen H100 GPU durch.

Das Forschungsteam nutzte die formale Verifikationssprache Lean, um computergestützte mathematische Beweise für Vollständigkeit, Korrektheit und Zero-Knowledge-Eigenschaften des Protokolls zu erstellen. Die veröffentlichten Softwarematerialien umfassen das Beweiserzeugungsprogramm, einen C++-Verifizierer, einen Lean-Verifizierer sowie zugehörige formale Beweisdateien; der Code wird unter der Apache-2.0-Lizenz veröffentlicht.

FlashProve befindet sich derzeit im Stadium eines Forschungsprototyps; der getestete Verifikationsumfang deckt hauptsächlich Kontexte bis 1024 Token, Ganzzahlberechnungen und Greedy-Decoding-Bedingungen ab. Die formalen Lean-Beweise beziehen sich auf das mathematische Modell des Protokolls und sind nicht gleichbedeutend mit einer formalen Verifikation des gesamten hochperformanten Ausführungscodes. Das System verifiziert die Konsistenz des Berechnungsprozesses des angegebenen Modells und der Herkunft seiner Ausgaben; die faktische Richtigkeit der Antworten des Modells wird dabei nicht beurteilt.