Anthropic julkaisee FlashProven kryptografiset todisteet tekoälyn päättelystä

Anthropic julkaisi FlashProven 2. marraskuuta 2026. Kyseessä on avoimen lähdekoodin tutkimusprototyyppi, joka käyttää kryptografisia todisteita osoittamaan, että kielimallin vastaus on tuotettu sitoutumisessa määritellyillä painoilla paljastamatta niitä. Yhtiön mukaan todistusten tuottamisnopeus oli 110 tokenia sekunnissa käytettäessä Metan Llama 4 Maverick -mallia.

Työ vastaa isännöityyn tekoälyyn liittyvään varmennuspuutteeseen. Laadukas vastaus ei osoita, mikä malli sen tuotti: reitityspalvelu voisi korvata mallin toisella järjestelmällä, arvioija voisi saada testattavaksi tarkoitetun mallin sijaan jonkin muun mallin tai hyökkääjä voisi muuttaa tokenvirtaa. Mallin suorittaminen uudelleen tarkistusta varten ei ole käyttäjille käytännöllistä, kun painot ovat yksityisiä ja laitteistovaatimukset huomattavat.

Vastausten sitominen piilotettuihin painoihin

FlashProve käyttää ohjelmistopohjaista nollatietoista tiivistä tiedon argumenttia eli zkSNARK-todistetta sen sijaan, että se tukeutuisi luotettuun laitteistoon. Palveluntarjoaja julkaisee offline-vaiheessa lyhyen sitoumuksen, joka yksilöi täsmälleen yhden painojoukon mutta pitää sen salassa. Järjestelmä tuottaa valmiille kehote–vastauspareille todisteen siitä, että tulostokenit ovat sitoumuksessa määritellyn mallin tuottamia. Kuka tahansa, jolla on sitoumus, kehote ja vastaus, voi tarkistaa todisteen ilman pääsyä painoihin.

Tavoiteltuja ominaisuuksia ovat täydellisyys, pitävyys, nollatietoisuus ja tiiviys. Rehellinen todiste pitäisi hyväksyä, kun taas väärän väitteen todistamisen pitäisi edellyttää yleisesti uskottujen kryptografisten oletusten murtamista. Todisteen tarkistamisen ei pitäisi paljastaa painoja eikä laskennan väliarvoja. Rakenne salaa myös sen, mitkä asiantuntijasekoitemallin aliverkot suorittivat kunkin tokenin laskennan, vaikka mallin arkkitehtuuri itsessään pysyy näkyvissä.

Toteutuksessa hyödynnetään Maverickin asiantuntijasekoiterakennetta. Todistajan työmäärä skaalautuu tokenia kohden aktiivisten noin 17 miljardin parametrin mukaan kaikkien 400 miljardin parametrin sijaan, mutta asiantuntijavalinnat pysyvät silti salassa. Jaetuiksi osiin pilkotut painot siirretään isäntäkoneen muistista suoratoistona, minkä ansiosta todistaja mahtuu yhdelle 80 Gt:n grafiikkasuorittimelle, jonka rinnalla on noin 290 Gt isäntäkoneen muistia.

Anthropicin mukaan mahdollisia käyttökohteita ovat asiakkaiden eheyden tarkistukset, riippumattomat arvioinnit, sääntelyyn liittyvät työkalut ja hyväksyttyjen mallien käyttövaatimusten valvonta. Päättelyä koskevilla sertifikaateilla voitaisiin vahvistaa, että pyynnöt käsitteli väitetty malli, mutta niillä ei voitaisi osoittaa, ettei samalla laitteistolla myös koulutettu toista mallia. Tämä ero rajoittaa sitä, mitä tällaisilla sertifikaateilla voidaan osoittaa vaatimusten noudattamisesta silloin, kun vaatimukset perustuvat laskentakapasiteetin käyttötapaan.

Todisteiden suorituskyky ja päättelyn lisäkustannukset

Anthropicin arvioinnissa käytettiin mallista julkisesti saatavilla olevaa 4-bittistä muunnosta. Yhden H100-grafiikkasuorittimen ja 24 suoritinytimen palvelin tuotti todisteet 24 pyynnön erälle noin 223 sekunnissa; kunkin pyynnön todisteen koko oli 18,78 Mt. Offline-sitoumuksen luominen kesti noin 39 minuuttia.

Varmennuspuolella asiakas lataa noin 6,5 Mt:n sitoumuksen ja tarkistaa todisteet suoritinytimellä ilman grafiikkasuoritinta. Anthropicin mittauksissa varmentaminen kesti 17 sekuntia 24 säikeellä ja 21 sekuntia yhdellä säikeellä. Aikoihin sisältyivät offline-vaiheen tarkistukset.

Mittaukset erottelevat pelkällä suorittimella tehtävän tarkistuksen huomattavasti raskaammasta todistusten tuottamisesta. Anthropicin vertailussa kahdeksalla H100-grafiikkasuorittimella vLLM:n avulla tehtyyn FP8-päättelyyn todistusten tuottaminen vaati samaa erää kohden noin 72 kertaa enemmän grafiikkasuoritinaikaa ja testatuista vLLM:n kuormitustasoista korkeimmalla noin 94 kertaa enemmän. Suorituskyky merkitsee siis huomattavaa kustannusta verrattuna mallin tarjoamiseen ilman todisteita.

Muodollinen verifiointi ja käytännön rajoitukset

FlashProven tietovarasto sisältää todistajan, nopean C++-varmentimen, hitaamman Lean-varmentimen, ylimmän tason matemaattisten väitteiden Lean-todistukset sekä vuorovaikutteisen lauseiden visualisointityökalun. Se on julkaistu Apache 2.0 -lisenssillä. Versio 0.16.0 on merkitty ylläpidottomaksi tutkimusartefaktiksi, johon ei oteta vastaan kontribuutioita.

Lean-työssä käsitellään täydellisyyttä, pitävyyttä ja nollatietoisuutta satunnaisoraakkelimallissa. Muodolliset väitteet on silti tarkistettava käsin, jotta voidaan varmistaa niiden vastaavan tarkoitettuja takuita. Lean-varmennin on muodollisesti kytketty pitävyyslauseeseen, mutta rutiinikäyttöön tarkoitettuun C++-varmentimeen ei liity muodollista takuuta. Sen sijaan on testattu, että se antaa samat tulokset kuin Lean-varmennin.

Projektin tunnettuja rajoituksia käsittelevässä dokumentaatiossa kerrotaan, että ihmisen ohjauksessa toimivat tekoälyjärjestelmät kirjoittivat lähes kaiken ohjelmiston, Lean-todistukset ja dokumentaation sekä suorittivat raportoidut testit. Riippumatonta tietoturva-auditointia ei ole tehty, ja painojen piilottamista sekä vastustajien laatimia todisteita on testattu vain rajallisesti.

Todisteet kattavat painojen täsmällisen kokonaislukuesityksen ahneella dekoodauksella. Liukulukupohjainen päättely tai otantaan perustuva dekoodaus voi poiketa todennettavasta laskennasta, eivätkä yleiset virhetestit kata tarkoituksella vastustajan tarpeisiin laadittuja kehotteita. Kontekstin pituus on rajattu 1 024 tokeniin, eivätkä ajoitus- ja muut sivukanavahyökkäykset kuulu takuun piiriin. Jälkikäteen tehtävä todistusten tuottaminen aiheuttaa lisäksi uudelleenlaskentaa, viivästyttää varmistusta ja tuo mukanaan epädeterminismiä verrattuna siihen, että todisteet tuotettaisiin päättelyn yhteydessä.

Jotta todennettavissa olevasta päättelystä tulisi palvelun käsittelemän liikenteen rutiininomainen tarkistus, jäljellä oleva työ keskittyy tämän julkaisun esiin tuomiin puutteisiin: todistamisen kustannusten alentamiseen, vähemmän rajoittavan dekoodauksen ja pidempien kontekstien kattamiseen sekä nopean toteutuksen tiiviimpään kytkemiseen formaaliin protokollaan.