Anthropic lansează FlashProve pentru dovezi criptografice ale inferenței AI

Anthropic a lansat FlashProve la 2 noiembrie 2026: un prototip de cercetare cu sursă deschisă care folosește dovezi criptografice pentru a arăta că un răspuns generat de un model lingvistic provine dintr-un set de ponderi prestabilit, fără a le dezvălui. Compania a raportat o viteză de generare a dovezilor de 110 tokeni pe secundă pentru modelul Llama 4 Maverick de la Meta.

Această cercetare abordează o lacună de verificare în domeniul AI găzduite. Un răspuns de înaltă calitate nu demonstrează ce model l-a generat: un serviciu de rutare ar putea înlocui modelul cu un alt sistem, un evaluator ar putea primi un model diferit de cel prevăzut pentru testare sau un atacator ar putea modifica fluxul de tokeni. Pentru utilizatori, verificarea prin rularea din nou a modelului este nepractică atunci când ponderile sunt private, iar cerințele hardware sunt substanțiale.

Asocierea răspunsurilor cu ponderi ascunse

FlashProve folosește un argument succint de cunoaștere cu zero-cunoaștere, numit și zkSNARK, într-un proiect bazat exclusiv pe software, fără a depinde de hardware de încredere. Într-o etapă offline, furnizorul publică un angajament scurt care identifică un set exact de ponderi, păstrându-le secrete. Pentru perechile de prompt și răspuns deja generate, sistemul produce o dovadă că tokenii de ieșire sunt rezultatul modelului identificat prin angajament. Oricine deține angajamentul, promptul și răspunsul poate verifica dovada fără a avea acces la ponderi.

Proprietățile urmărite sunt completitudinea, soliditatea, zero-cunoașterea și concizia. O dovadă onestă ar trebui să fie acceptată, în timp ce certificarea unei afirmații false ar trebui să necesite încălcarea unor ipoteze criptografice considerate pe scară largă valide. Verificarea unei dovezi nu ar trebui să dezvăluie nici ponderile, nici valorile intermediare ale calculelor. Proiectul ascunde și care subrețele ale arhitecturii mixture-of-experts au fost activate pentru fiecare token, deși arhitectura modelului în sine rămâne vizibilă.

Implementarea exploatează structura mixture-of-experts a modelului Maverick. Volumul de lucru al generatorului dovezii crește proporțional cu cele aproximativ 17 miliarde de parametri activi pentru un token, nu cu totalul de 400 de miliarde, ascunzând totodată alegerile experților. Ponderile segmentate sunt transferate în flux din memoria gazdă, astfel încât generatorul dovezii să poată funcționa pe un singur GPU de 80 GB, împreună cu aproximativ 290 GB de memorie gazdă.

Anthropic descrie posibile utilizări pentru verificările integrității clienților, evaluări independente, instrumente de reglementare și aplicarea cerințelor privind modelele aprobate. Certificatele de inferență ar putea atesta că solicitările au fost procesate de modelul declarat, dar nu ar demonstra că același hardware nu a fost folosit și pentru antrenarea unui alt model. Această distincție limitează ceea ce astfel de certificate ar putea demonstra în privința cerințelor de conformitate bazate pe modul de utilizare a capacității de calcul.

Performanța dovezilor și costul suplimentar al inferenței

Evaluarea Anthropic a folosit o conversie pe 4 biți a modelului, disponibilă public. Un server cu un H100 și 24 de nuclee CPU a generat dovezi pentru un lot de 24 de solicitări în aproximativ 223 de secunde, producând o dovadă de 18,78 MB pentru fiecare solicitare. Etapa offline de creare a angajamentului a durat aproximativ 39 de minute.

Pentru verificare, clientul descarcă un angajament de aproximativ 6,5 MB și verifică dovezile pe un CPU, fără GPU. Anthropic a măsurat un timp de verificare de 17 secunde cu 24 de fire de execuție și de 21 de secunde cu un singur fir, incluzând verificările din etapa offline.

Aceste măsurători disting un proces de verificare care folosește doar CPU-ul de o operațiune de generare a dovezilor mult mai solicitantă. În comparația realizată de Anthropic cu inferența FP8 pe opt H100 care rulează vLLM, generarea dovezilor a necesitat de aproximativ 72 de ori mai mult timp per GPU pentru același lot și de aproximativ 94 de ori mai mult la cea mai mare încărcare vLLM testată. Prin urmare, debitul obținut presupune un cost substanțial față de servirea modelului fără dovezi.

Verificare formală și limite practice

Depozitul FlashProve conține un generator de dovezi, un verificator rapid în C++, un verificator Lean mai lent, dovezi Lean pentru afirmații matematice de nivel superior și un instrument interactiv de vizualizare a teoremelor, toate sub licența Apache 2.0. Versiunea 0.16.0 este descrisă drept un artefact de cercetare neîntreținut, pentru care nu se acceptă contribuții.

Lucrările în Lean abordează completitudinea, soliditatea și zero-cunoașterea în modelul oracolului aleatoriu. Afirmațiile formale necesită în continuare o examinare manuală pentru a stabili dacă exprimă garanțiile urmărite. Verificatorul Lean este conectat formal la teorema de soliditate, însă verificatorul C++ destinat utilizării curente nu oferă nicio garanție formală; în schimb, a fost testat pentru a confirma că oferă rezultate concordante cu verificatorul Lean.

Documentația proiectului privind limitele cunoscute consemnează că sistemele AI aflate sub îndrumarea oamenilor au scris aproape tot software-ul, dovezile Lean și documentația și au rulat testele raportate. Nu a fost efectuat niciun audit independent de securitate, iar testarea protecției ponderilor și a dovezilor adversariale rămâne limitată.

Dovezile acoperă o versiune întreagă exactă a ponderilor în condițiile decodării greedy. Inferența în virgulă mobilă sau decodarea prin eșantionare se pot abate de la calculul demonstrat, iar testarea generică a erorilor nu acoperă prompturile concepute în mod adversarial. Contextele sunt limitate la 1.024 de tokeni, iar atacurile de sincronizare și alte atacuri prin canale laterale nu intră în sfera garanției. În comparație cu generarea dovezilor în paralel cu inferența, generarea ulterioară introduce recalculare, garanții întârziate și nedeterminism.

Pentru ca inferența verificabilă să devină o verificare de rutină a traficului procesat, munca rămasă se concentrează asupra lacunelor evidențiate de această versiune: reducerea costului generării dovezilor, extinderea acoperirii la metode de decodare mai puțin restrictive și contexte mai lungi, precum și conectarea mai solidă a implementării rapide la protocolul formal.