Büyük Dil Modelleri İçin Kanıtlanabilir Çıkarım (Provable Inference) Konusunda İlerlemeler

Bölüm 01: Yönetici Özeti#

Yüz yüze konuştuğunuz bir arkadaşınızın gerçekten o kişi olduğunu anlamanın pek çok yolu vardır: onu görebilir, duyabilir ve elini sıkabilirsiniz. Ancak bir yapay zeka modeliyle konuşurken bu doğrulama imkanlarının neredeyse hiçbirine sahip değilsinizdir. Bugün bir modeli sorgulayan bir kullanıcı veya geliştirici, gelen yanıtların gerçekten sağlayıcının iddia ettiği spesifik modelden gelip gelmediğini kontrol edemez. Bir yönlendirme (routing) servisi maliyetleri düşürmek amacıyla arka planda gizlice daha ucuz bir model kullanıyor olabilir ya da bir saldırgan token akışına müdahale etmiş olabilir. Çıktı yüksek kaliteli görünse bile yalnızca modelin yanıtlarına bakarak doğrulama yapmak güvenilir değildir.

Kriptografik çıkarım kanıtları (cryptographic proofs of inference) bu sorunu çözer: Model sağlayıcısının belirli bir modele taahhüt vermesini (commit) ve ardından üretilen her yanıtın gerçekten o model tarafından oluşturulduğunu matematiksel olarak kanıtlamasını sağlar. Bu tür kanıtlar, tüketici ürünlerinden kurum içi güvenliğe kadar pek çok uygulamayı mümkün kılabilir ve yapay zeka uyumluluk denetimleri için kritik bir doğrulama aracı sunabilir.

Anthropic araştırmacıları (EPFL, MIT, StarkWare ve Succinct iş birliğiyle), güçlü gizleme ve verimlilik özellikleri sayesinde kanıtlanabilir çıkarım için benzersiz biçimde uygun olan zkSNARK adlı kriptografik kanıt türünde önemli ilerlemeler kaydetti. Bu ilerlemeler, FlashProve adı verilen sistem üzerinden paylaşılıyor.

Teknik Özet ve Mimari Bulgular#

Sistemin sağladığı temel teknik ilerlemeler şunlardır:

Yüksek Hızlı zkSNARK Çıkarımı: Claude, çıkarım süreçleri için zkSNARK'lar üzerinde iyileştirmeler üreterek önceki açık kaynaklı sistemlerden önemli ölçüde daha hızlı bir sistem inşa etti.
Büyük Modellerde Performans Metrikleri: Büyük bir modelde (Llama 4 Maverick, 400B parametreli Mixture of Experts), 4-bit kuantize ağırlıklar ve prefill aşamasında tamsayı aritmetiği kullanıldığında, tek bir H100 GPU saniyede yaklaşık 110 token hızında kanıt üretmektedir. 1.024 token'lık bir istek için kanıt boyutu yaklaşık 19 MB'tır. Bu süre, modeli yaygın bir açık kaynak kütüphanesi olan vLLM üzerinde çalıştırmanın yaklaşık 70-95 katı GPU zamanına denk gelse de önceki açık kaynak sistemlerden katbekat daha hızlıdır.
Kriptografik Tasarım İlkeleri: Claude, kriptografik kanıt sistemleri için kabul görmüş tasarım ilkelerine bağlı kalarak, kriptografi ve güvenlik literatüründeki en güncel araçları uygulamanın özgün yollarını buldu.
Ağırlıkların Gizliliği: Modele yapılan taahhüt ve sonrasındaki çıkarım kanıtları modelin ağırlıklarını (weights) gizler; ancak model mimarisini gizlemek bu sistemin bir amacı değildir.
Biçimsel Doğrulama (Formal Verification): Claude optimizasyon konusunda başarılı olsa da özellikle büyük ve karmaşık sistemlerde değerlendirilmesi güç kararlar alabilir. Araştırma ekibi bu riski, iddia edilen güvenlik garantileri için biçimsel bir doğrulama dili olan Lean ile yazılmış üst düzey denetlenebilir ifadeler sunarak dengeliyor.

Yayınlanan 5 Temel Çıktı (Artifact)#

Araştırma kapsamında Apache 2.0 lisansı altında beş temel bileşen paylaşılıyor:

Sistemin genel hatlarını ve potansiyel uygulamalarını özetleyen mevcut blog yazısı;
Sistemin detaylarını açıklayan kapsamlı bir teknik rapor;
Claude tarafından yazılmış bir protokol spesifikasyon dokümanı;
Bir kanıtlayıcı (prover) ve iki doğrulayıcı (C++ ile yazılmış hızlı bir doğrulayıcı ve Lean ile yazılmış kanıtlanabilir doğruluğa sahip bir doğrulayıcı) içeren çalıştırılabilir kod;
Denetimi kolaylaştırmak amacıyla Lean teoremlerinin etkileşimli bir görselleştiricisi ile birlikte üst düzey matematiksel ifadeler için Lean kanıtları.

Yazılım Geliştiriciler İçin Pratik Çıkarımlar#

Üretim ortamında LLM API'leri ve model yönlendiricileri (API Gateway / Router) kullanan mühendisler için bu gelişme iki kritik ders barındırıyor:

AI Tedarik Zinciri ve Model Doğrulama: Üçüncü parti API sağlayıcıları üzerinden model tüketirken "model ikamesi" (model substitution) ve çıkarım müdahaleleri gerçek birer güvenlik ve kalite riskidir. Gelecekte yüksek güvenlikli sistemlerde API yanıtlarının yanında kriptografik kanıtların (zkSNARK doğrulaması) talep edilmesi standart bir Model Doğrulama pratiği haline gelebilir.
Yapay Zeka Destekli Mühendislikte Biçimsel Doğrulama: Claude gibi modeller karmaşık sistem optimizasyonlarında çığır açıcı hızlanmalar sağlayabilir; ancak ürettikleri karmaşık kodların doğruluğunu garanti altına almak için Lean gibi biçimsel doğrulama (formal verification) araçlarıyla güvenlik sınırlarını matematiksel olarak kanıtlamak, modern yazılım mühendisliğinde yeni bir kalite standardı oluşturmaktadır.

Orijinal makaleye buradan ulaşabilirsiniz.