FlashProve: ZK-Beweise für KI-Inferenz, Claude-written, Lean-geprüft

Hintergrund und Phänomene: Man weiß nicht, ob die zurückgegebene Antwort tatsächlich das von einem ausgewählte Modell ist

Am 4. November 2026 veröffentlichte Anthropic den Forschungsblog „Progress on provable inference for large language models“, in dem ein System namens FlashProve vorgestellt wurde. Gleichzeitig wurden fünf Werke öffentlich gemacht: der Blog selbst, technische Berichte, Protokolle, ausführbarer Code (ein Beweiser und zwei Validatoren), Lean-Beweise sowie ein Tool zur interaktiven Visualisierung von Sätzen. Der gesamte Code, die Beweise und die Dokumentation sind unter der Apache 2.0-Lizenz veröffentlicht. Das zugehörige Repository anthropics/FlashProve wurde am 30.10.2026 erstellt und hatte bis zum 5. November 781★ Punkte. Die Version-Datei lautet 0.16.0. Der Blog hat 155▲ HN-Einträge und 77 Kommentare.

Die gestellten Fragen im Blog sind direkt: Wenn Benutzer Anfragen an das Modell stellen, gibt es keine Möglichkeit, zu überprüfen, ob die zurückgegebene Antwort tatsächlich das von einem ausgewählten Modell ist. Die Routing-Dienste könnten zum Sparen geheime günstige Modelle verwenden, und Angreifer könnten den Token-Stream manipulieren. Aus der Qualität der Antwort lässt sich nicht sicher sein – selbst eine schöne Antwort kann nicht beweisen, dass man tatsächlich das von einem ausgewählten Modell stellt. Unabhängige Bewertungsinstitutionen müssen wissen, dass es sich um das auf der Plattform laufende Modell handelt. Benutzer, die über Drittanbieter-Dienste abrufen, müssen sicherstellen, dass der Token tatsächlich vom von ihnen bezahlten Modell stammt.

Der zweite wichtige Punkt ist die Autorenstruktur und die Rolle von Claude darin. Der Blog ist unterzeichnet mit einer Mischung aus Wissenschaftlern und Forschern aus dem Bereich der Kryptografie: zwei Personen von Anthropic, drei von EPFL, sowie Forscher aus MIT, StarkWare, Succinct und RESI. Besonders auffällig ist die Selbstbeschreibung des Blogs: „Claude hat den zkSNARK für den Schlussverfahren verbessert“ und ein System entwickelt, das viel schneller ist als die bestehenden offenen Systeme. In den fünf Werken ist in den Protokolldokumenten klar angegeben, dass Claude sie geschrieben hat. Anthropic erklärt gleichzeitig die Risiken und Maßnahmen dieser Schreibweise: Claude ist gut darin, Optimierungen vorzunehmen, aber Entscheidungen in großen, komplexen Systemen sind oft schwer zu bewerten. Die Lösung besteht darin, die angeblichen Sicherheitsgarantien in einer überprütbaren Top-Level-Proposition in Lean (eine formalisierte Verifizierungssprache) aufzuschreiben.

Die erste Zeile des README beschreibt die Selbstpositionierung: „Forschungswerke: keine Wartung, keine Beiträge“. Der Blog gibt auch offen zu, dass es sich um einen vorläufigen Fortschritt handelt und nicht um ein abgeschlossenes Forschungsprogramm. Der Zweck der Veröffentlichung ist es, andere dazu zu bringen, Verbesserungen vorzunehmen.

Architektur und technische Prinzipien: drei Schritte – Commit, Prove, Verify

Das Kernstück von FlashProve ist das zkSNARK-basierte beweisbare Schlussverfahren. Der Mechanismus besteht aus drei Schritten (wie im README beschrieben). Der erste Schritt ist Commit: Der Anbieter veröffentlicht eine Commit-ID, die mit einer Gruppe von Gewichten verbunden ist. Die Gewichte selbst sind geheim, alle öffentlichen Werte der abhängigen Gewichte werden verschlüsselt, mit Ausnahme der Liste, die in docs/what-is-not-hidden.md angegeben wird. Das Designziel ist klar definiert: Es geht darum, die Gewichte zu verbergen, nicht aber die Architektur. Der zweite Schritt ist Prove: Jede Antwort wird durch die GPU des Anbieters mit einem Beweis versehen. Der dritte Schritt ist Verify: Jeder kann mit dem C++-Validator cp_verify ein paar Sekunden lang auf einer normalen CPU überprüfen, ob „diese Antwort tatsächlich vom versprochenen Modell stammt“, ohne die Gewichte zu benötigen.

Der Teil „Lean“ ist der andere Schwerpunkt des Repos. Insgesamt gibt es 30.902 Dateien beim lokalen Clone, davon 29.563 .lean-Dateien und nur 185 .py-Dateien, mit einer Gesamtoberfläche von 723MB. Die Ordner enthalten prover, verifier, lean, paper (technische Berichte in PDF-Format), docs (19 Artikel), guide (8 Artikel), tests, toy, scales usw. Das Dokument lean/THEOREM.md listet sechs Theoreme auf, die alle auf dieselbe Gruppe von committern, prover und verifier angewendet werden und für jede offizielle Setup-Implementierung gelten: sound (die Wahrscheinlichkeit, dass der Betrüger bei q Hash-Abfragen den Verifier täuscht, beträgt nicht mehr als ca. q/2^124 + 2^-101; die Originalbeschreibung besagt „Dies ist ein Grenzwert, kein Sicherheitsniveau“); soundAndBinding (niemand kann die Versprechen in eine andere Gewichtungsgruppe umwandeln, außer mit einer Wahrscheinlichkeit von ca. q/2^124 + 2^-100); completeOnCanServe (die Wahrscheinlichkeit, dass eine ehrliche Beweisführung auf einer Anfrage falsch abgelehnt wird, beträgt nicht mehr als 2^-40); zeroKnowledgeOnCanServe (bei 2^64 Hash-Abfragen und 688.127 Antworten liegt die Offenbarung nicht über 2^-154; Simulatoren erhalten keine Gewichtungen); refusedHandsOutNoProof (Abgelehnte Anfragen können nur leere Beweise zurückgeben, aber „ob die Ablehnung richtig ist“, gehört nicht zum Beweisumfang); repliesFit (die Übereinstimmung zwischen 688.127 Antworten und der Anzahl der Tabellen).

Zwei Grenzen sollten besonders erwähnt werden, beides sind Selbstangaben des Repos. Erstens verlangen alle sechs Theoreme eine „genaue Übereinstimmung“, doch der Verifier überprüft dies nicht: Wenn der Dienstleister nachdem er die Anfrage gesehen hat die offizielle Datei-Strategie ändert, gelten die Theoreme nicht. Zweitens werden alle Testpakete mit synthetischen Gewichtungen durchgeführt; das Originaldokument SUITE.md besagt: Die erfolgreichen Tests zeigen nur, dass das Programm auf synthetische Eingaben die erwarteten Antworten gibt, und lassen wenig über Zuverlässigkeit und Verborgenheit aussagen.

Schlüsseldaten: 110 Toks/s, 93-facher Kostenvertrag und sechs Wahrscheinlichkeitsgrenzen

Die Leistungsdaten stammen aus dem Dokument guide/performance.md und README des Repos. Es gibt keine unabhängige Wiederholbarkeit der Daten.

Zu testende Modelle: Llama 4 Maverick in voller Größe (400B Parameter MoE), mit einer extern veröffentlichten 4-bit-Konvertierung (Downloadvolumen 232GB), 1.024-token Kontextfenster, ein H100-Block 80GB. Geschwindigkeit: Bei einem Batch-Update von 24 Stunden beträgt die Rate 111.23±0.92 Toks/s, in README ca. 110; bei einem Batch von 1 nur 17.41; bei einem Batch von 64 erreicht die Rate 123.31, doch der Repos selbst bezeichnete 80GB als Problem bei einem Batch von 64, da es unzuverlässig ist. Die GPU-RAM wird auf 80.629/81.559 MiB erhöht, und bei 8 Versuchen mit synthetischen Gewichtungen scheiterten alle CUDA-Aufrufe.

Der Kostenvertrag ist ebenfalls eine Selbstangabe des Repos: Pro GPU beträgt der Zeitaufwand 93,0-fach langsamer als beim nativem prefill von vLLM (bei höchster Last), 71,4-fach langsamer als bei einem Batch von 24 von vLLM. Zudem handelt es sich um „berechnete, optimale Werte“, ohne Start- und Versprechenzeiten. Für die Basisversion werden weiterhin 8×H100-Blocken für FP8 verwendet.

Beweis und Speichervolumen: Der durchschnittliche Beweis beträgt 18,78 MB; der Client muss jeweils 6,24 MB einmal herunterladen; der Anbieter muss jeweils 2,15 GB speichern. Die Erfüllung dieser Anforderungen dauert etwa 39 Minuten, und ein Versprechen kann mehrfach verwendet werden; die Host-Speicher des Anbieters sollten mindestens 330 GB betragen, der Speicherplatz 245 GB. Der Beweiskosten ist das asymmetrischste Element im gesamten System: cp_verify dauert in einem Thread etwa 21 Sekunden, benötigt bis zu 3,53 GB RAM und erfordert keine GPU; die „Corruptible Verifier“-Version von Lean benötigt etwa 24 Minuten für einen vollständigen Beweis, bis zu 14,13 GB RAM.

Das Repository gibt seine Schwächen ziemlich offenbar: Der Startzeitraum beträgt 68-79 Sekunden; nachdem die Beweiskosten auf die ersten 1.000 Anfragen verteilt wurden, liegt die stabile Rate bei 88,81 tok/s, was nicht dem selbst festgelegten Ziel von 100 tok/s entspricht. Die Datei performance.md gibt direkt zu, dass das Ziel nicht erreicht wurde.

Auswirkungen und Bedeutung: „Welches Modell sagt“ als prüfbarkeitstechnisches Merkmal

Erstens, im Hinblick auf Compliance und Audit-Szenarien. Der Blog erklärt ausdrücklich, dass zkSNARK als Werkzeug zur Überprüfung der Compliance-Anforderungen für AI verwendet werden kann: Die Aufsichtsbehörden fordern von Anbietern Zertifikate für einen bestimmten Zeitraum der Berechnungen. Der Anbieter kann diese nicht fälschen, es sei denn, das Hardware-System läuft tatsächlich mit dem angeblichen Modell. Gleichzeitig erhalten die Aufsichtsbehörden keine Informationen über die exklusiven Rechte. Ein hochbewerteter Kommentar bedeutet dasselbe: In Compliance-Audits, Proxy-Chains und Regulierungs-Szenarien ist „Welches Modell sagt“ selbst ein wichtiges Merkmal.

Zweitens, das Vertrauensproblem bei der Aggregationstransmission. Ein Kommentar weist darauf hin, dass Aggregate wie OpenRouter Anfragen an andere Modelle weiterleiten können. Dieses System kann solche Fälle erkennen; ein weiterer Kommentar beschreibt konkretere Betrugsfälle, bei denen Claude-Händler in bestimmten Märkten versprechen, Zugang zu bieten, aber tatsächlich andere Modelle verwenden. Dies kann als Prüfbarkeit für solche Fälle verwendet werden. Es wird auch erwähnt, dass es Gerüchte über Modelle mit demselben Namen auf bestimmten Hosts gibt, die deutlich schlechter performen und möglicherweise unveröffentlichte Quantisierungsversionen verwenden (der Kommentator geht von einem Gerücht aus). Es wird gefragt, ob dieses System solche Fälle erkennen kann.

Drittens, offene Gewichtungsmodelle können ebenfalls damit ihre Integrität beweisen. Ein hochbewerteter Kommentar, der die Dokumentation des Repositories gelesen hat, weist darauf hin: Wenn öffentliche Gewichtungen für Versprechen verwendet werden und Saatgut veröffentlicht wird, kann jeder aus den Hugging Face-Dateien die Versprechen neu berechnen, um zu überprüfen, ob der Anbieter tatsächlich die angegebenen Checkpoints und Quantisierungsbit-Werte verwendet. Das bedeutet, dass dieses System nicht nur geschlossene Hersteller unterstützt, sondern der Community zunächst ein Selbstprüfungswerkzeug bietet.

Viertens, die methodische Bedeutung von Claude bei der Erstellung von Kryptografie-Code und Lean als Sicherheitsmaßnahme mag größer sein als das System selbst. „Schwierige AI-Berechnungen“ werden in formaler Sprache zu prüfbarn Top-Level-Prämissen umgewandelt, sodass Maschinen die von Menschen geschriebenen Code-Teile überprüfen können. Dies ist ein wiederverwendbarer Engineering-Paradigma, wenn AI an der Entwicklung von kritischen Infrastrukturen teilnimmt (das ist meine Einschätzung).

Kontroversen und Risiken: PR-Aktion oder Erfüllung eines leeren Raums

Die stärksten Kommentare im HN-Forum waren ironisch. Der höchstbewertete Kommentar betrachtet dies als eine PR-Aktion. Ein Nutzer zog frühere Berichte heran und wies darauf hin, dass dieselbe Firma bereits wegen des stillen Weiterleitens von ML-Anfragen an schwächere Modelle in der Presse war (der Kommentator geht auf diese Aussage nicht ein). Aber auch hier gibt es Widersprüche: Das Weiterleiten von Modellen ist das häufigste Problem der Nutzer, und es gab zuvor keinen Beweismechanismus. Wenn dieses System erfolgreich sein könnte, wäre dies von großer Bedeutung.

Der Wertstreit geht tiefer. Einige glauben, dass es die Eigenschaft beweist, die als „grundlegende Anforderung“ gilt: Allerdings liefert es keine nützlichen Informationen außer der Bestätigung, dass es nicht durch billigere Modelle oder Zwischenhändler ersetzt wurde. Andere dachten zunächst, dass es die „Richtigkeit der Ausgabe“ beweisen müsse, stellten jedoch fest, dass es nur nachweist, welches Modell verwendet wird. Sie sagten, wenn man den Anbieter nicht vertraut, wäre das Spiel längst vorbei. Die Gegenpartei antwortete: Kunden kümmern sich um die Richtigkeit der Ausgabe, Hersteller kümmern sich darum, dass die Ausgabe aus ihrem eigenen Modell stammt – diese Lösung befasst sich mit letzterem. Es gab auch Kommentare, die vorhersagten, dass es letztendlich zur FUD gegen billige Routen verwendet werden könnte (das ist eine Vermutung des Kommentators über den Motiv). Meine Meinung: Die beiden Seiten stehen eigentlich nicht im Widerspruch zueinander. „Richtigkeit der Ausgabe“ und „Ausgabe aus dem angeblichen Modell“ sind zwei unabhängige Überprüfungsfragen. Die erste ist noch nicht gelöst, die zweite hat momentan nur eine mögliche Lösung in Form von Kryptografie (das ist meine Einschätzung).

Es gibt drei harte Grenzen für technische Risiken. Erstens, das Problem der genauen Übereinstimmung: Alle sechs Theoreme verlangen, dass die offiziellen Dokumente genau mit den Zusagen übereinstimmen. Da die Überprüfer dies nicht überprüfen, fällt es unter die Garantie, wenn der Anbieter nach dem Empfang des Requests seine Strategie ändert. Das ist ein bekanntes Loch im System. Zweitens, die Hürde für den Einsatz: Der GPU-Stack erfordert x86-64 Linux 4.14+ mit SHA-Erweiterung, eine exklusive H100-CPU mit 80GB Speicher und CUDA 13.2 Update 2 (die aktuellen Toolkits werden nicht unterstützt). Für den echten Modellansatz sind 330GB RAM und 245GB Festplattenspeicher erforderlich, was für Einzelpersonen und kleine Teams kaum machbar ist. Drittens, alle Leistungswerte stammen von dem Anbieter selbst, es gibt keine Third-Party-Reproduktionen. Die 93-fache Verlangsamung bedeutet, dass es in der kurzen Frist eher wie ein Audit-Tool wirkt als eine produktive Funktion.

Schlussfolgerungen und Perspektiven: Das Repository selbst ist ein zweites Experiment

Der Kernaussage: FlashProve nutzt zkSNARK, um zu beweisen, dass „die Antwort aus dem versprochenen Gewicht stammt“, was jeder auf einem normalen CPU in Sekunden erledigen kann. Der Preis dafür ist eine Anwendungshürde von 70-95-facher GPU-Zeit und RAM auf der Ebene von 330GB. Gleichzeitig verwendet es 29.563 Lean-Dokumente, um die Frage „Kann das von Claude geschriebene Kryptografiekode vertrauenswürdig sein?“ in sechs überprüfbare Theoreme zu übersetzen.

Ein interessantes Phänomen: Im README gibt es einen Abschnitt mit dem Titel „Bauweise für die Ausführung durch einen Agent“. Der Autor schlägt vor, dass der Leser seinen eigenen Coding-Agenten auf dieses Repository richtet. Er hat einen direkt einzufügbaren Befehlstext und teilt den Überprüfungsweg in vier Bereiche auf: Weg 1 erfordert nur Linux und g++13 sowie 2GB RAM, die Konstruktion dauert 1-2 Minuten, die Überprüfung der vorhandenen Beweise 2 Sekunden; Weg 2 dauert etwa 1 Minute, um ein Spielbeweis auf der CPU auszuführen; Weg 3 erfordert eine kompakte kleine Modellstruktur mit acht Schichten und dem vollen H100-Stack, die Konstruktion dauert etwa 29 Minuten; Weg 4 ist das echte Llama 4 Maverick, das Stunden dauert. Die Sicherheitsmaßnahmen sind ebenfalls passend: Root/Sudo sind während der gesamten Zeit verboten, der Sandbox verwendet Landlock. Diese Designs sind an sich ein Experiment „um einen Agenten sicher in einem fremden Repository auszuführen“. Der erste Leser der Repository-Dokumente könnte gerade vom Menschen zum Agenten werden.

Zwei Dinge verdienen in Zukunft Aufmerksamkeit. Erstens: Die README-Erklärung, dass das Projekt nicht weiter gepflegt und keine Beiträge mehr akzeptiert wird, sowie die Aufforderung im Blog, andere dazu aufzufordern, Verbesserungen vorzunehmen. Es ist sehr wahrscheinlich, dass die fünf Arbeitspakete des Apache 2.0-Standards von der Wissenschaft und dem Sicherheits- und Start-up-Szenario weitergeführt werden. Ob es möglich ist, eine unabhängige, nachweisbare Implementierung zu entwickeln, ist eine härtere Überprüfung als das Hinzufügen eines Sternchens. Zweitens: Ob die genauen Grenzen ergänzt werden können, was entscheidend dafür ist, ob dieses System aus den Audits in den normalen Produktionsprozessen übernommen werden kann.

Meine Schlussfolgerung in einem Satz: FlashProve ist es wert, untersucht zu werden – nicht weil es das Problem der Vertrauensbildung bei der Reasoning gelöst hat (das hat es nicht, und die offiziellen Stellen geben dies selbst zu). Vielmehr hat es zwei Dinge, die bisher nur verbal garantiert werden konnten, in nachweisbare Aussagen verwandelt: Die Identität der Modelle und die Richtigkeit der von AI geschriebenen Sicherheitscode. Das Erste bezieht sich auf den Vertrauensgrundstein für den Reasoning-Markt, das Letztere auf die Qualitätskontrolle in der Ära der AI-Programmierung.

Referenzquellen

• Anthropic Forschungsblog „Progress on provable inference for large language models“: anthropic.com/research/provable-inference (veröffentlicht am 2026-11-04; alle Aussagen zu Claude stammen vom Blog selbst)
• HN-Eintrag: story 50368626 (155▲ / 77 Kommentare, Snapshot vom 2026-11-05)
• Repository: github.com/anthropics/FlashProve (781★ / Apache 2.0 / created 2026-10-30 / VERSION 0.16.0, Snapshot vom 2026-11-05)
• Lokaler leichter Clone-Test (gemessen am 2026-11-05, ohne Ausführung des Repository-Codes): README.md, guide/performance.md, lean/THEOREM.md, SUITE.md, docs/, AGENTS.md; 30.902 Dateien / 723MB lokal gemessen
• HN-Kommentarpool: hn-provable.json (47 Belege, der gesamte Text wurde wiedergegeben, direkte Zitate nicht verwendet)

Unterschrift: Yongliang