Anthropic udostępnia FlashProve do tworzenia kryptograficznych dowodów inferencji AI

Anthropic udostępniło FlashProve 2 listopada 2026 r. — otwarty prototyp badawczy, który wykorzystuje dowody kryptograficzne, aby wykazać, że odpowiedź modelu językowego powstała na podstawie określonych wag, nie ujawniając ich. Firma podała, że generowanie dowodów dla modelu Meta Llama 4 Maverick osiągało szybkość 110 tokenów na sekundę.

Prace te dotyczą problemu weryfikacji w przypadku hostowanych systemów AI. Wysoka jakość odpowiedzi nie pozwala ustalić, który model ją wygenerował: usługa routingu mogłaby podstawić inny system, osoba oceniająca mogłaby otrzymać inny model niż ten przeznaczony do testów albo atakujący mógłby zmodyfikować strumień tokenów. Użytkownikom trudno zweryfikować wynik przez ponowne uruchomienie modelu, gdy jego wagi są prywatne, a wymagania sprzętowe znaczne.

Powiązanie odpowiedzi z ukrytymi wagami

FlashProve wykorzystuje zwięzły argument wiedzy z wiedzą zerową, czyli zkSNARK, w rozwiązaniu opartym wyłącznie na oprogramowaniu, a nie na zaufanym sprzęcie. W fazie offline dostawca publikuje krótkie zobowiązanie, które identyfikuje jeden konkretny zestaw wag, nie ujawniając ich. Dla zrealizowanych par prompt–odpowiedź system generuje dowód, że tokeny wyjściowe są wynikiem działania modelu wskazanego w zobowiązaniu. Każdy, kto ma zobowiązanie, prompt i odpowiedź, może sprawdzić dowód bez dostępu do wag.

Oczekiwane właściwości systemu to zupełność, poprawność, wiedza zerowa i zwięzłość. Uczciwy dowód powinien zostać zaakceptowany, a poświadczenie fałszywego twierdzenia powinno wymagać złamania powszechnie uznawanych za wiarygodne założeń kryptograficznych. Sprawdzenie dowodu nie powinno ujawniać ani wag, ani pośrednich wartości obliczeń. Rozwiązanie ukrywa również, które podsieci architektury typu mieszanka ekspertów działały przy przetwarzaniu poszczególnych tokenów, choć sama architektura modelu pozostaje widoczna.

Implementacja wykorzystuje architekturę typu mieszanka ekspertów modelu Maverick. Nakład pracy związany z generowaniem dowodu skaluje się wraz z około 17 miliardami parametrów aktywnych dla danego tokenu, a nie z pełnymi 400 miliardami, przy jednoczesnym ukryciu wyboru ekspertów. Wagi podzielone na segmenty są strumieniowane z pamięci hosta, dzięki czemu proces generowania dowodu mieści się na jednym procesorze GPU z 80 GB pamięci, przy około 290 GB pamięci hosta.

Anthropic opisuje możliwe zastosowania w kontrolach integralności obsługi klientów, niezależnych ocenach, narzędziach regulacyjnych i egzekwowaniu wymogu korzystania z zatwierdzonych modeli. Certyfikaty inferencji mogłyby poświadczać, że żądania obsłużył deklarowany model, ale nie dowodziłyby, że ten sam sprzęt nie służył równocześnie do trenowania innego modelu. To rozróżnienie ogranicza zakres tego, co takie certyfikaty mogłyby wykazać w odniesieniu do wymogów zgodności uzależnionych od sposobu wykorzystania mocy obliczeniowej.

Wydajność generowania dowodów i narzut związany z inferencją

W ocenie Anthropic wykorzystano publicznie dostępny model w wersji 4-bitowej. Serwer z jednym układem H100 i 24 rdzeniami procesora CPU wygenerował dowody dla partii 24 żądań w około 223 sekundy, tworząc dla każdego żądania dowód o rozmiarze 18,78 MB. Przygotowanie zobowiązania w fazie offline trwało około 39 minut.

Po stronie weryfikacji klient pobiera zobowiązanie o rozmiarze około 6,5 MB i sprawdza dowody na procesorze CPU bez użycia GPU. Anthropic zmierzyło czas weryfikacji na 17 sekund przy 24 wątkach i 21 sekund przy jednym wątku; pomiary obejmowały kontrole z fazy offline.

Pomiary te pokazują różnicę między weryfikacją działającą wyłącznie na CPU a znacznie bardziej wymagającym procesem generowania dowodów. W porównaniu Anthropic z inferencją FP8 na ośmiu układach H100 z użyciem vLLM generowanie dowodów wymagało około 72 razy więcej czasu pracy każdego GPU dla tej samej partii, a przy najwyższym testowanym obciążeniu vLLM — około 94 razy więcej. Uzyskanie takiej przepustowości wiąże się więc ze znacznym kosztem w porównaniu z obsługą modelu bez dowodów.

Weryfikacja formalna i ograniczenia praktyczne

Repozytorium FlashProve zawiera narzędzie do generowania dowodów, szybką weryfikację w C++, wolniejszą weryfikację w Lean, dowody w Lean dotyczące głównych twierdzeń matematycznych oraz interaktywną wizualizację twierdzeń. Całość udostępniono na licencji Apache 2.0. W repozytorium oznaczono wersję 0.16.0 jako nieutrzymywany artefakt badawczy, do którego nie są przyjmowane wkłady.

Prace w Lean dotyczą zupełności, poprawności i wiedzy zerowej w modelu losowej wyroczni. Twierdzenia sformułowane w sposób formalny nadal wymagają ręcznej weryfikacji, aby ustalić, czy wyrażają zamierzone gwarancje. Weryfikator Lean jest formalnie powiązany z twierdzeniem o poprawności, ale weryfikator C++, przeznaczony do rutynowego użytku, nie ma formalnych gwarancji; zamiast tego sprawdzono, czy jego wyniki są zgodne z wynikami weryfikatora Lean.

W dokumentacji projektu opisującej znane ograniczenia odnotowano, że niemal całe oprogramowanie, dowody w Lean i dokumentację napisały systemy AI działające pod nadzorem człowieka, które przeprowadziły również zgłoszone testy. Nie przeprowadzono niezależnego audytu bezpieczeństwa, a testy ukrywania wag i odporności na sfabrykowane dowody są ograniczone.

Dowody dotyczą dokładnej, całkowitoliczbowej wersji wag i dekodowania zachłannego. Inferencja zmiennoprzecinkowa lub dekodowanie z próbkowaniem mogą odbiegać od obliczeń objętych dowodem, a ogólne testy błędów nie obejmują promptów zaprojektowanych w celu przeprowadzenia ataku. Kontekst jest ograniczony do 1 024 tokenów, a ataki czasowe i inne ataki wykorzystujące kanały boczne nie są objęte gwarancją. Generowanie dowodów po zakończeniu inferencji wymaga ponownych obliczeń, opóźnia uzyskanie zapewnień i wprowadza niedeterminizm w porównaniu z generowaniem dowodów równolegle z inferencją.

Aby wnioskowanie z możliwością weryfikacji dowodami stało się rutynową kontrolą obsługiwanego ruchu, pozostałe prace koncentrują się na lukach ujawnionych przez tę wersję: obniżeniu kosztów generowania dowodów, obsłudze mniej restrykcyjnego dekodowania i dłuższych kontekstów oraz ściślejszym powiązaniu szybkiej implementacji z formalnym protokołem.