Anthropic, Kriptografik Yapay Z zekâ Çıkarım Kanıtları için FlashProve’u Yayımladı

Anthropic, 2 Kasım 2026’da FlashProve’u yayımladı: Dil modeli yanıtlarının, ağırlıkları açığa çıkarmadan, önceden belirlenmiş ağırlıklardan üretildiğini kriptografik kanıtlarla göstermeyi amaçlayan açık kaynaklı bir araştırma prototipi. Şirket, Meta’nın Llama 4 Maverick modeli için saniyede 110 token hızında kanıt üretebildiğini bildirdi.

Bu çalışma, barındırılan yapay zekâ sistemlerinde bir doğrulama açığını ele alıyor. Bir yanıtın kaliteli olması, onu hangi modelin ürettiğini kanıtlamaz: Bir yönlendirme hizmeti başka bir sistemi devreye sokabilir, bir değerlendiriciye test edilmesi amaçlanan model yerine farklı bir model sunulabilir ya da bir saldırgan token akışını değiştirebilir. Ağırlıklar gizli ve donanım gereksinimleri yüksek olduğunda, kullanıcıların modeli yeniden çalıştırarak kontrol yapması pratik değildir.

Yanıtları Gizli Ağırlıklara Bağlamak

FlashProve, güvenilir donanıma dayanan bir tasarım yerine yalnızca yazılımla çalışan bir yaklaşımda sıfır bilgi kısa bilgi argümanı (zkSNARK) kullanıyor. Çevrimdışı aşamada sağlayıcı, ağırlıkları gizli tutarken tam olarak belirli bir ağırlık kümesini tanımlayan kısa bir taahhüt yayımlıyor. Sistem, tamamlanmış istem-yanıt çiftleri için çıktı tokenlarının taahhütte belirtilen modelin çıktısı olduğunu gösteren bir kanıt üretiyor. Taahhüde, isteme ve yanıta sahip olan herkes, ağırlıklara erişmeden kanıtı doğrulayabiliyor.

Hedeflenen özellikler tamlık, sağlamlık, sıfır bilgi ve kısalıktır. Dürüstçe oluşturulmuş bir kanıtın kabul edilmesi; yanlış bir ifadeyi doğrulamanın ise yaygın biçimde kabul gören kriptografik varsayımları çürütmeyi gerektirmesi beklenir. Bir kanıtı doğrulamak ne ağırlıkları ne de ara hesaplama değerlerini açığa çıkarmalıdır. Tasarım, modelin mimarisi görünür kalmaya devam etse de her token için hangi uzman karışımı alt ağlarının çalıştığını da gizler.

Uygulama, Maverick’in uzman karışımı yapısından yararlanıyor. Kanıtlayıcının iş yükü, uzman seçimlerini gizli tutarken tüm 400 milyar parametre yerine token başına etkin olan yaklaşık 17 milyar parametreyle orantılı olarak ölçekleniyor. Ağırlıklar bölümler hâlinde ana makine belleğinden aktarılıyor; böylece kanıtlayıcı, yanında yaklaşık 290 GB ana makine belleği bulunan tek bir 80 GB GPU’ya sığabiliyor.

Anthropic, olası kullanım alanları arasında müşteri bütünlüğü kontrollerini, bağımsız değerlendirmeleri, düzenleyici araçları ve onaylanmış model kullanma gerekliliklerinin uygulanmasını sayıyor. Çıkarım sertifikaları, isteklerin iddia edilen model tarafından işlendiğini doğrulayabilir; ancak aynı donanımın başka bir modeli eğitmek için de kullanılmadığını göstermez. Bu ayrım, bu tür sertifikaların bilgi işlem kapasitesinin nasıl kullanıldığına dayanan uyumluluk gereklilikleri konusunda kanıtlayabileceklerini sınırlar.

Kanıt Performansı ve Çıkarım Ek Yükü

Anthropic’in değerlendirmesinde modelin herkese açık 4 bitlik bir dönüşümü kullanıldı. Bir H100 ve 24 CPU çekirdeğine sahip sunucu, 24 istekten oluşan bir grup için yaklaşık 223 saniyede kanıt oluşturdu; her istek için 18,78 MB’lık bir kanıt üretti. Çevrimdışı taahhüt aşaması yaklaşık 39 dakika sürdü.

Doğrulama tarafında istemci, yaklaşık 6,5 MB’lık bir taahhüt indiriyor ve GPU kullanmadan CPU üzerinde kanıtları kontrol ediyor. Anthropic, çevrimdışı aşamaya ilişkin kontroller de dâhil olmak üzere doğrulamanın 24 iş parçacığıyla 17 saniye, tek iş parçacığıyla 21 saniye sürdüğünü ölçtü.

Bu ölçümler, yalnızca CPU kullanan kontrol sürecini çok daha ağır olan kanıt oluşturma işleminden ayırıyor. Anthropic’in vLLM çalıştıran sekiz H100 üzerindeki FP8 çıkarımıyla yaptığı karşılaştırmada, aynı istek grubu için kanıt oluşturma GPU başına yaklaşık 72 kat, test edilen en yüksek vLLM yükünde ise yaklaşık 94 kat daha fazla süre gerektirdi. Dolayısıyla bu verim, modeli kanıt üretmeden sunmaya kıyasla önemli bir maliyet getiriyor.

Biçimsel Doğrulama ve Uygulamadaki Sınırlar

FlashProve deposunda bir kanıtlayıcı, hızlı bir C++ doğrulayıcı, daha yavaş bir Lean doğrulayıcı, üst düzey matematiksel ifadelerin Lean kanıtları ve Apache 2.0 lisansı kapsamında etkileşimli bir teorem görselleştiricisi bulunuyor. Depo, 0.16.0 sürümünü bakımı yapılmayan ve katkı kabul etmeyen bir araştırma ürünü olarak nitelendiriyor.

Lean çalışması, rastgele kehanet modelinde tamlık, sağlamlık ve sıfır bilgi özelliklerini ele alıyor. Biçimsel ifadelerin amaçlanan güvenceleri gerçekten ifade ettiğini belirlemek için yine de elle incelenmeleri gerekiyor. Lean doğrulayıcı, sağlamlık teoremine biçimsel olarak bağlı; ancak rutin kullanım için tasarlanan C++ doğrulayıcı biçimsel bir güvence sunmuyor ve bunun yerine Lean doğrulayıcıyla aynı sonuçları verdiği test ediliyor.

Projenin bilinen sınırlara ilişkin belgeleri, yazılımın, Lean kanıtlarının ve belgelerin neredeyse tamamının insan yönlendirmesi altındaki yapay zekâ sistemleri tarafından yazıldığını ve bildirilen testlerin de bu sistemler tarafından çalıştırıldığını kaydediyor. Bağımsız bir güvenlik denetimi yapılmadı; ağırlıkların gizliliği ve hasmane kanıtlara ilişkin testler de sınırlı kaldı.

Kanıtlar, açgözlü çözümleme altında ağırlıkların tam sayı biçiminin birebir aynısını kapsıyor. Kayan noktalı çıkarım veya örneklemeli çözümleme, kanıtlanan hesaplamadan sapabilir; genel hata testleri de hasmane amaçlarla tasarlanmış istemleri kapsamıyor. Bağlam uzunluğu 1.024 tokenla sınırlı; zamanlama ve diğer yan kanal saldırıları ise güvencenin kapsamı dışında. Çıkarım sonrasında kanıt oluşturmak, çıkarım sırasında kanıt oluşturmaya kıyasla yeniden hesaplama gerektiriyor, güvenceleri geciktiriyor ve belirlenimci olmama durumunu beraberinde getiriyor.

Kanıtlanabilir çıkarımın hizmet verilen trafik üzerinde rutin bir denetime dönüşmesi için, yapılması gerekenler bu sürümün ortaya çıkardığı eksikliklerde yoğunlaşıyor: kanıt üretme maliyetini düşürmek, daha az kısıtlayıcı kod çözme yöntemlerini ve daha uzun bağlamları kapsamak, ayrıca hızlı uygulamayı biçimsel protokole daha sağlam biçimde bağlamak.