Anthropic Merilis FlashProve untuk Bukti Inferensi AI Kriptografis

Anthropic merilis FlashProve pada 2 November 2026: sebuah prototipe riset sumber terbuka yang menggunakan bukti kriptografis untuk menunjukkan bahwa respons model bahasa berasal dari bobot yang telah dikomitmenkan, tanpa mengungkapkannya. Perusahaan melaporkan bahwa bukti dapat dihasilkan dengan kecepatan 110 token per detik untuk Llama 4 Maverick dari Meta.

Penelitian ini mengatasi celah verifikasi pada layanan AI terhosting. Jawaban berkualitas tinggi tidak membuktikan model mana yang menghasilkannya: layanan perutean dapat menggantinya dengan sistem lain, evaluator dapat menerima model yang berbeda dari model yang seharusnya digunakan untuk pengujian, atau penyerang dapat mengubah aliran token. Bagi pengguna, memeriksanya dengan menjalankan ulang model tidak praktis ketika bobotnya bersifat privat dan kebutuhan perangkat kerasnya besar.

Mengikat Respons pada Bobot Tersembunyi

FlashProve menggunakan argumen pengetahuan ringkas tanpa pengetahuan, atau zkSNARK, dalam rancangan yang sepenuhnya berbasis perangkat lunak, alih-alih bergantung pada perangkat keras tepercaya. Dalam tahap luring, penyedia menerbitkan komitmen singkat yang mengidentifikasi satu set bobot tertentu secara tepat, tetapi merahasiakannya. Untuk pasangan prompt dan respons yang telah selesai, sistem menghasilkan bukti bahwa token keluaran merupakan keluaran model yang diidentifikasi oleh komitmen tersebut. Siapa pun yang memiliki komitmen, prompt, dan balasan dapat memeriksa bukti tanpa mengakses bobotnya.

Sifat yang hendak dicapai adalah kelengkapan, soundness, tanpa pengetahuan, dan keringkasan. Bukti yang jujur semestinya diterima, sedangkan pengesahan atas pernyataan palsu seharusnya mengharuskan pelanggaran terhadap asumsi kriptografis yang secara luas dianggap benar. Pemeriksaan bukti semestinya tidak mengungkapkan bobot ataupun nilai komputasi perantara. Rancangan ini juga menyembunyikan subjejaring campuran pakar mana yang dijalankan untuk setiap token, meskipun arsitektur model itu sendiri tetap terlihat.

Implementasi ini memanfaatkan struktur campuran pakar milik Maverick. Beban kerja pembuktian sebanding dengan sekitar 17 miliar parameter yang aktif untuk satu token, bukan seluruh 400 miliar parameter, sekaligus tetap menyembunyikan pilihan pakarnya. Bobot yang dibagi menjadi beberapa segmen dialirkan dari memori host, sehingga pembuktian dapat dijalankan pada satu GPU 80 GB dengan sekitar 290 GB memori host yang menyertainya.

Anthropic menjelaskan kemungkinan penggunaan untuk pemeriksaan integritas pelanggan, evaluasi independen, perangkat regulasi, dan penegakan persyaratan penggunaan model yang disetujui. Sertifikat inferensi dapat membuktikan bahwa permintaan dilayani oleh model yang diklaim, tetapi tidak membuktikan bahwa perangkat keras yang sama tidak sekaligus digunakan untuk melatih model lain. Perbedaan ini membatasi hal-hal yang dapat dibuktikan oleh sertifikat tersebut terkait persyaratan kepatuhan yang didasarkan pada penggunaan kapasitas komputasi.

Kinerja Pembuktian dan Beban Tambahan Inferensi

Evaluasi Anthropic menggunakan versi konversi 4-bit model yang tersedia untuk umum. Sebuah server dengan satu H100 dan 24 inti CPU membuktikan satu batch berisi 24 permintaan dalam waktu sekitar 223 detik, dengan menghasilkan bukti berukuran 18,78 MB untuk setiap permintaan. Tahap komitmen luring memerlukan waktu sekitar 39 menit.

Di sisi verifikasi, klien mengunduh komitmen berukuran sekitar 6,5 MB dan memeriksa bukti menggunakan CPU tanpa GPU. Anthropic mengukur waktu verifikasi sebesar 17 detik dengan 24 utas dan 21 detik dengan satu utas, termasuk pemeriksaan pada tahap luring.

Pengukuran tersebut membedakan proses pemeriksaan yang hanya menggunakan CPU dari operasi pembuktian yang jauh lebih berat. Dalam perbandingan Anthropic dengan inferensi FP8 pada delapan H100 yang menjalankan vLLM, pembuktian memerlukan waktu per GPU sekitar 72 kali lebih lama untuk batch yang sama dan sekitar 94 kali lebih lama pada beban vLLM tertinggi yang diuji. Dengan demikian, laju pemrosesan tersebut disertai biaya yang jauh lebih besar dibandingkan dengan melayani model tanpa bukti.

Verifikasi Formal dan Batasan Praktis

Repositori FlashProve memuat pembukti, verifier C++ yang cepat, verifier Lean yang lebih lambat, bukti Lean untuk pernyataan matematis tingkat tinggi, serta visualisator teorema interaktif, semuanya berlisensi Apache 2.0. Repositori tersebut menyebut versi 0.16.0 sebagai artefak riset yang tidak lagi dipelihara dan tidak menerima kontribusi.

Karya Lean ini membahas kelengkapan, soundness, dan sifat tanpa pengetahuan dalam model oracle acak. Pernyataan formalnya masih memerlukan peninjauan manual untuk memastikan bahwa pernyataan tersebut benar-benar mengungkapkan jaminan yang dimaksud. Verifier Lean terhubung secara formal dengan teorema soundness, tetapi verifier C++ yang ditujukan untuk penggunaan rutin tidak memiliki jaminan formal; sebagai gantinya, verifier tersebut diuji untuk memastikan kesesuaiannya dengan verifier Lean.

Dokumentasi batasan yang diketahui dari proyek ini mencatat bahwa sistem AI yang diarahkan manusia menulis hampir seluruh perangkat lunak, bukti Lean, dan dokumentasi, serta menjalankan pengujian yang dilaporkan. Belum ada audit keamanan independen, dan pengujian atas penyembunyian bobot serta bukti adversarial masih terbatas.

Bukti ini mencakup versi bilangan bulat yang persis dari bobot dalam kondisi dekode greedy. Inferensi titik mengambang atau dekode dengan pengambilan sampel dapat menyimpang dari komputasi yang dibuktikan, dan pengujian kesalahan umum tidak mencakup prompt yang dirancang secara adversarial. Konteks dibatasi hingga 1.024 token, sementara serangan pengukuran waktu dan serangan saluran samping lainnya berada di luar jaminan. Pembuktian setelah proses inferensi juga menimbulkan komputasi ulang, jaminan yang tertunda, dan nondeterminisme dibandingkan dengan pembuktian yang dilakukan bersamaan dengan inferensi.

Agar inferensi yang dapat dibuktikan menjadi pemeriksaan rutin atas lalu lintas yang dilayani, pekerjaan yang tersisa berfokus pada kesenjangan yang terungkap dalam rilis ini: menurunkan biaya pembuktian, mencakup metode dekode yang tidak terlalu ketat dan konteks yang lebih panjang, serta menghubungkan implementasi cepat dengan protokol formal secara lebih kokoh.