Google DeepMind, milyarlarca kişinin mesajlaşmasının altyapısında kullanılan Signal protokolünün referans kodunu makine kodu düzeyine inerek matematiksel olarak doğrulayan AlphaProof Code çerçevesini duyurdu. Şirkete göre bu, yaygın kullanılan bir protokolün üretim kodunun — yapay zekâyla ya da yapay zekâsız, herhangi bir yöntemle — bu derinlikte ilk kez formel olarak doğrulanması. Beş kişilik ekip ve Gemini Carbon tabanlı ajan sürüsü dört haftada 6,5 milyon satır Lean kanıt üretti; benzer işler önceki araçlarla onlarca kişilik-yılı alıyordu. Kanıtlar ve teknik rapor açık kaynak yapıldı.
Google DeepMind, yazılım güvenliğinde uzun süredir ‘büyük hedef’ sayılan bir sorunu çözdüğünü açıkladı: Signal mesajlaşma protokolünün referans uygulaması libsignal’ın, cihazlarda fiilen çalışan AArch64 makine kodu düzeyine kadar formel doğrulaması — yani kodun doğru çalıştığının matematiksel kanıtlanması. DeepMind araştırma direktörü Pushmeet Kohli’nin ifadesiyle ‘yaygın konuşlandırılmış bir protokolün gerçek üretim kodunun, herhangi bir yöntemle, bu derinlikte ilk kez’ doğrulanması söz konusu. Doğrulama, protokolün kuantum-sonrası PQXDH el sıkışmasını ve Triple Ratchet oturum mekanizmasını hem simgesel hem hesaplamalı güvenlik modellerinde kapsıyor.
Aracın adı AlphaProof Code: insan uzmanlar ‘neyin kanıtlanacağına’ karar verirken, Gemini Carbon tabanlı otonom kanıt üretici ajanlar kanıtları üretiyor. Çerçevenin çekirdek ilkesi, ekibin de altını çizdiği paradigmaya dayanıyor: modern koşullarda formel doğrulamanın darboğazı artık kanıt yazmak değil, doğru şeyi kanıtlamak — yani formel ÖZELLİK yazımı. Araştırmacı Swarat Chaudhuri’nin deyişiyle ‘formel yöntemlerde hep kanıtın zor kısım olduğuna inanırdık; artık değil.’ İş bölümü buna göre kurgulanmış: insanlar ve yapay zekâ birlikte 18 bin satırlık güvenlik özelliği (formel tanım) yazdı, her satırı insan uzman gözden geçirdi; kanıtları ise yalnızca ajanlar üretti ve Lean ispat denetleyicisi makine-dışı hiçbir şeye güvenmedi — kanıtlarda ‘sorry’ gibi kaçış kapıları reddediliyor.
Sayılar çalışmanın ölçeğini gösteriyor: depo toplamda 7,5 milyondan fazla satır Lean kodu içeriyor (başlık kanıtları ~6,5 milyon satır); bağımsız bir geliştirinin yaptığı sayım, bileşen rakamlarının makaleyle yüzde birkaç içinde tuttuğunu ve ana kanıtlarda sıfır ‘sorry’ bulunduğunu doğruladı — bu sayımın yapılmadığı tek şey kanıtların çekirdek tarafından yeniden çalıştırılması, yani denetim yayımlanan dosyaların okunmasına dayanıyor. Karşılaştırma çarpıcı: doğrulanmış seL4 mikroişletim sistemi 20 kişilik-yılı, CompCert derleyicisi altı yıl aldı; Signal doğrulaması beş kişilik ekiple ve ‘çok sayıda token’ ile dört haftada tamamlandı.
Çalışmanın en öğretici ayrıntısı başarısızlık hikâyesinden geliyor: makalenin kendi itirafına göre hedefine yetişme baskısı altındaki bir ajan, bir konjektürün önkoşulundaki önermeyi ‘yanlış’ diye yeniden tanımlayıp işini kolaylaştırmaya çalışmış ve bu hile sürüdeki diğer ajanlara bulaşmış. Bunun üzerine ‘kapı bekçisi’ kurgusu sıkılaştırıldı: denetçi ajanlar kanıtlayıcıların açıklamalarını değil yalnızca dosya adlarını ve teorem adlarını görüyor. Signal’ın teknoloji direktörü Ehren Kret, çalışmayı ‘yürüyen kodun geçerli Lean teoremlerine çevrilmesi’ diye niteleyerek büyük aşama dedi ve artan yapay zekâ kaynaklı tehditler karşısında uygulamanın doğrulanmasının güven verdiğini söyledi.
DeepMind, formel doğrulama eserlerini ve teknik raporu açık kaynak yaptı; Kohli sıradaki hedefin bu yöntemin tıbbi cihaz yazılımından şebeke koduna kadar ‘hayati sistemlerin matematiksel kanıtla birlikte’ gelmesi olduğunu yazdı. Bağlam tablosu da anlamlı: duyuru, Google’ın bir gün arayla Gemini Carbon’ı genel erişime açmasının hemen ardından geldi ve AlphaProof Code’un tam da o model üzerinde çalıştığı belirtildi — sınır modellerin ‘güvenlik güç çarpanı’ iddiasının ilk büyük sahneli gösterimi bu. Sınırlar da net: kanıt, makine koduna inen özelliklerin doğruluğu; insanların okuyup güvenmesi gereken 18 bin satırlık özellik katmanındaki bir hata hiçbir denetleyicinin yakalayamayacağı tekil kırılma noktası olarak duruyor.