FlashProve od Anthropic. Kryptograficzny dowód, który model odpowiedział

Co pokazał Anthropic i dlaczego to ma znaczenie

Użytkownik modelu AI nie ma dziś sposobu, by sprawdzić, czy odpowiedź naprawdę wygenerował model, za który płaci. Pośrednik routujący zapytania może po cichu podstawić tańszy model, a napastnik, który przejmie serwer, może podmieniać odpowiedzi. Sama jakość tekstu niczego tu nie dowodzi. Anthropic opisuje ten problem we wpisie badawczym z 2 listopada 2026 roku i proponuje rozwiązanie nazwane dowodzeniem inferencji (provable inference).

Mechanizm działa w dwóch krokach. Dostawca najpierw publikuje zobowiązanie, czyli krótki kryptograficzny odcisk jednego konkretnego zestawu wag. Potem do każdej odpowiedzi może dołączyć plik dowodu, który potwierdza, że model o tych wagach, uruchomiony na danym poleceniu, zwraca dokładnie te tokeny. Sprawdzający potrzebuje tylko zobowiązania, polecenia, odpowiedzi i dowodu.

Badanie powstało we współpracy Anthropic z naukowcami z politechniki EPFL w Lozannie, MIT i firm StarkWare oraz Succinct. Wpis podpisało ośmioro autorów, a współtwórcą jest m.in. Alessandro Chiesa, kryptograf z EPFL.

Jak działa dowód o zerowej wiedzy

FlashProve korzysta z zkSNARK, czyli zwięzłego dowodu o zerowej wiedzy. Taki dowód przekonuje weryfikatora, że obliczenie wykonano poprawnie, nie zdradzając niczego ponad sam fakt poprawności. Jest też zwięzły, więc jego sprawdzenie zajmuje ułamek czasu potrzebnego na powtórzenie obliczenia. Podobne dowody działają od kilku lat w sieciach blockchain, m.in. w Starknecie.

Anthropic deklaruje cztery właściwości systemu. Uczciwy dowód zawsze przechodzi weryfikację, a fałszywego nie da się podrobić bez złamania powszechnie uznawanych założeń kryptograficznych. Dowód nie ujawnia wag, wartości pośrednich ani tego, które części modelu zostały użyte. Jest też mały i tani w sprawdzeniu.

System ukrywa wagi, ale nie architekturę modelu. Działa wyłącznie z modelami typu mixture of experts (MoE), w których przy każdym tokenie pracuje tylko część sieci. Dzięki temu nakład pracy przy dowodzeniu zależy od ok. 17 mld aktywnych parametrów, a nie od wszystkich 400 mld.

Wyniki testu na Llama 4 Maverick

Pomiary wykonano na publicznie dostępnej, 4-bitowej wersji modelu Llama 4 Maverick od Meta. Serwer dowodzący miał jedną kartę H100 i 24 rdzenie procesora, a weryfikator działał wyłącznie na CPU. Poniżej najważniejsze liczby z wpisu Anthropic.

• Faza wstępna (zobowiązanie do wag) - ok. 39 minut, raz na model. Zobowiązanie wystarcza na ok. 16 mln zapytań.
• Dowodzenie paczki 24 zapytań po 1024 tokeny - ok. 223 sekundy, czyli ok. 110 tokenów na sekundę.
• Rozmiar dowodu - 18,78 MB na zapytanie, do tego jednorazowo ok. 6,5 MB zobowiązania.
• Weryfikacja - ok. 17 sekund na 24 wątkach procesora i ok. 21 sekund na jednym wątku.
• Narzut względem vLLM na 8 kartach H100 - ok. 72 razy (66-77 w kolejnych przebiegach) i ok. 94 razy przy najwyższym testowanym obciążeniu.

Postęp względem wcześniejszych prób

Dowody poprawności działania sieci neuronowych badano od 2017 roku, ale dotąd udawało się to tylko dla małych modeli albo bardzo wolno. Według zestawienia Anthropic system zkLLM w 2024 roku dowodził model z 13 mld parametrów w tempie ok. 2,5 tokena na sekundę. Wcześniejsza próba dla tego samego Llama 4 Maverick, VerInf, potrzebowała 14,3 godziny na 1000 tokenów, a dowód ważył 93,6 GB.

Komercyjna firma Attestable podaje 53-77 tokenów na sekundę dla gęstego modelu Gemma 4 31B, ale nie udostępniła kodu. W ocenie autorów narzut rzędu dwóch rzędów wielkości jest dużo mniejszy, niż przewidywano jeszcze niedawno. Te liczby to wyniki własne zespołu, niepotwierdzone przez niezależny audyt.

Rola Claude i formalnej weryfikacji

Anthropic pisze, że znaczną część usprawnień zaprojektował Claude, który zastosował znane techniki kryptograficzne w nowy sposób. Firma przyznaje jednocześnie, że decyzje modelu w dużym systemie trudno ocenić. Dlatego najważniejsze gwarancje, czyli poprawność, niepodrabialność i zerową wiedzę, zapisano i udowodniono w Lean, języku do formalnej weryfikacji matematycznej.

Ta weryfikacja ma luki, które autorzy opisują wprost. Ktoś musi ręcznie sprawdzić, czy twierdzenia w Lean mówią to, co mają mówić. Szybki weryfikator w C++, przeznaczony do codziennego użytku, nie ma formalnej gwarancji, a jedynie w testach zgadza się z wolniejszym weryfikatorem w Lean. Podobne podejście firma stosowała wcześniej przy formalnej weryfikacji bibliotek open source.

Do czego może służyć dowodzenie inferencji

Anthropic wskazuje cztery zastosowania. Pierwsze to kontrola tempa rozwoju AI, gdy regulator chce mieć pewność, że sprzęt dostawcy obsługuje deklarowany model, a nie trenuje po cichu nowy. Drugie to wykrywanie podmiany modelu po włamaniu na serwer. Trzecie to potwierdzanie pochodzenia tekstu, np. że kod przeskanował konkretny model bezpieczeństwa. Czwarte to pilnowanie, by udostępniano wyłącznie modele zatwierdzone jako bezpieczne.

Dla klientów biznesowych najbardziej praktyczny jest drugi i trzeci scenariusz. Firma kupująca dostęp do modelu przez pośrednika mogłaby wymagać dowodu, że płaci za model, który faktycznie odpowiada. Niezależni ewaluatorzy mogliby z kolei sprawdzić, że testowali ten sam model, który trafił do użytkowników.

Ograniczenia prototypu

Autorzy podkreślają, że to wynik pośredni, a nie gotowy produkt. W repozytorium na GitHubie FlashProve opisano jako prototyp badawczy, który nie będzie utrzymywany. Anthropic nie zapowiedział dołączania takich dowodów do odpowiedzi Claude ani nie podał terminu wdrożenia.

• Kontekst zapytania ma maksymalnie 1024 tokeny, podczas gdy czaty i agenci pracują na setkach tysięcy tokenów.
• Dowód dotyczy całkowitoliczbowej wersji modelu i dekodowania zachłannego. Odpowiedź z losowym próbkowaniem albo z obliczeń zmiennoprzecinkowych może w którymś miejscu się od niego odchylić.
• System działa tylko z modelami MoE i nie ukrywa architektury, którą dostawcy często traktują jako tajemnicę.
• Ataki boczne, np. pomiar czasu tworzenia dowodu, mogą potencjalnie zdradzać informacje o wagach. Autorzy wyłączyli je z zakresu badania.
• Dowodzenie odbywa się po fakcie i dla części ruchu, więc gwarancja przychodzi z opóźnieniem.

Co to oznacza dla firm w Polsce i UE

Na dziś nic nie zmienia się w codziennej pracy z Claude, ChatGPT czy Gemini. Zmienia się natomiast perspektywa audytu. AI Act nakłada na dostawców modeli ogólnego przeznaczenia obowiązki dokumentacyjne i daje Urzędowi ds. AI uprawnienia do ewaluacji modeli. Narzędzie, które pozwala sprawdzić, że ewaluowany model jest tym samym, który obsługuje klientów, bez ujawniania wag, odpowiada na realny problem nadzoru. Unijne przepisy nie wymagają jednak takich dowodów.

W naszej ocenie warto śledzić ten kierunek przy wyborze pośredników API i platform agregujących modele. Firmy, które kupują dostęp do modeli przez routery, już teraz mogą pytać dostawców o sposób potwierdzania, który model obsłużył zapytanie, oraz zapisywać to w umowach. Zespoły badawcze, np. przy polskich uczelniach zajmujących się kryptografią, mają z kolei otwarty kod do dalszych prac.