Anthropic opublikowało FlashProve 2 listopada 2026 roku jako otwarty prototyp badawczy. Ma on pozwolić sprawdzić, czy wybrane tokeny odpowiedzi odpowiadają konkretnemu zestawowi wag modelu. Dowód ukrywa wagi, ale nie architekturę. W opisie projektu Anthropic określa też, jakie obliczenie obejmuje ta weryfikacja i jakie koszty wiązały się z jej testami.

Co sprawdza dowód FlashProve

FlashProve wykorzystuje zkSNARK, czyli zwięzły dowód kryptograficzny, który pozwala zweryfikować określone obliczenie bez ujawniania wag modelu. System działa w dwóch etapach. Najpierw dostawca publikuje commitment, czyli kryptograficzne zobowiązanie wiążące późniejsze sprawdzenie z jednym, konkretnym zestawem wag. Następnie tworzy dowód dla promptu i wskazanych tokenów odpowiedzi. Osoba mająca commitment, prompt, odpowiedź i dowód może sprawdzić, czy ustalony model wygenerował te tokeny.

Dowód dotyczy pochodzenia wyjścia, a nie jego jakości: nie potwierdza, że odpowiedź jest prawdziwa ani że model jest bezpieczny. Ukrywa wagi, wartości pośrednie obliczeń i informację o tym, które eksperckie podmodele działały przy generowaniu tokenu. Architektura modelu pozostaje jawna.

Wyniki testu i koszt dowodzenia

Anthropic przetestowało FlashProve na modelu Llama 4 Maverick, mieszance ekspertów o 400 mld parametrów, z których około 17 mld jest używanych przy generowaniu jednego tokenu. W teście wykorzystano publiczne, czterobitowe wagi pochodzące z konwersji przygotowanej przez podmiot zewnętrzny. Serwer dowodzący korzystał z jednego układu H100 i 24 rdzeni CPU.

Partia 24 żądań zajęła około 223 sekund; Anthropic podało przepustowość dowodzenia na poziomie około 110 tokenów na sekundę. Każdy dowód sprawdzał jeden token i miał 18,78 MB. Okno żądania obejmowało 1 024 tokeny, a system obsługuje konteksty do tej długości. Wstępne przygotowanie commitmentu dla modelu trwało około 39 minut; według Anthropic można go użyć przy około 16 mln żądań, po czym trzeba przygotować go ponownie.

Weryfikacja działała na CPU: Anthropic podało 17 sekund przy 24 wątkach i 21 sekund przy jednym wątku. Klient pobierał też commitment o rozmiarze około 6,5 MB. Są to wyniki ewaluacji opisanej przez Anthropic, a nie uniwersalny pomiar dla innych modeli czy konfiguracji.

Koszt dowodzenia był wysoki w zestawieniu ze zwykłym wnioskowaniem. W porównaniu Anthropic użyło vLLM do obsługi tej samej partii 24 żądań, z wersją FP8 tego samego modelu na ośmiu układach H100. Firma podała około 72 razy więcej czasu GPU na GPU dla dowodzenia; w kolejnych próbach wynik wynosił 66–77 razy, a przy najwyższym testowanym obciążeniu vLLM około 94 razy. Liczba 110 tokenów na sekundę opisuje tempo dowodzenia w teście, nie zwykłe tempo generowania odpowiedzi przez model.

Zakres obliczeń i ograniczenia

Opisany dowód dotyczy całkowitoliczbowej wersji modelu i dekodowania zachłannego, czyli wyboru tokenu o najwyższym prawdopodobieństwie na każdym kroku. Wynik z obliczeń zmiennoprzecinkowych albo z dekodowania próbkowanego może się różnić od obliczenia objętego dowodem. Opis FlashProve nie daje też ogólnego poświadczenia dowolnych ustawień usługi, takich jak temperatura czy nakład wyszukiwania.

Dowody powstają post hoc, po wygenerowaniu tekstu, i obejmują wybrane tokeny, a nie każdy token w chwili jego tworzenia. W teście pojedynczy dowód sprawdzał jeden token. Anthropic wskazuje, że takie podejście oznacza dodatkowe obliczenia, opóźnienie przed uzyskaniem gwarancji oraz problemy wynikające z niedeterminizmu.

Pozostaje także kwestia zgodności implementacji z formalnym opisem. Anthropic sformalizowało w Lean kluczowe twierdzenia o zupełności, odporności na fałszywe dowody i zerowej wiedzy. Firma zaznacza jednak, że szybki kod wykonywalny, publikacja i protokół zapisany w Lean nie mają formalnej gwarancji wzajemnej zgodności. Szybki weryfikator w C++ nie ma takiej formalnej gwarancji; Anthropic podaje, że w jego testach akceptował te same dowody co weryfikator Lean. Czas tworzenia dowodu może też potencjalnie ujawniać informacje o wagach przez kanał boczny.

Co obejmuje otwarte wydanie

Anthropic opublikowało kod z narzędziem tworzącym dowody, szybką implementacją weryfikatora w C++ i weryfikatorem w Lean, a także specyfikację protokołu, formalizację Lean i interaktywny wizualizator twierdzeń. Kod, dowody Lean i dokumentacja są udostępnione na licencji Apache 2.0. Wagi Llama 4 Maverick użyte w ewaluacji nie są częścią wydania.