Microsoft Research, Kodlama Ajanlarının Yazdığı Yazılımları PDD Kit ile Doğruluyor
Kaynak: microsoft.com ·
Microsoft Research, kodlama ajanlarının ürettiği kodların hata yapma ve standartlardan sapma riskine karşı Kanıt Odaklı Geliştirme (PDD) yaklaşımını ve PDD Kit aracını duyurdu. Bu araç, kullanıcıların niyetlerini resmi şartnamelere dönüştürerek ajan kodlarının her girdi için bu şartları karşılayıp karşılamadığını matematiksel olarak kanıtlıyor. Kanıtların ulaşamadığı dış dünya ve arayüz gibi alanlarda ise geleneksel testler devreye giriyor. Araştırmacılar sistemi, yaklaşık 5.000 satır Rust kodundan oluşan Pet Store adlı tam yığın bir web uygulamasının kimlik doğrulama mantığı üzerinde test etti.
Neden önemli?
Yapay zeka ajanları on binlerce satır kodu tek seferde üretebildiği için insan mühendislerin satır satır kod incelemesi ölçeklenebilirliğini yitiriyor. Bu durum, ajanların başlangıçtaki plandan uzaklaşarak gizli açıklar barındıran kodlar ve yanıltıcı testler üretmesine yol açabiliyor. PDD Kit, kod incelemesinin ağırlığını kodun kendisinden niyet aşamasına kaydırarak güvenilirliği artırıyor ve yazılım mühendislerinin resmi yöntem geçmişi olmasa bile matematiksel doğrulamadan yararlanmasını sağlıyor.
Bununla neler yapılabilir?
- Olası kullanım: Rust tabanlı arka uç uygulamalarında kimlik doğrulama ve oturum açma mantığının kurallara uygunluğunu matematiksel olarak doğrulamak.
- Olası kullanım: Kapsamlı satır içi kod incelemesi yapmak yerine, geliştirici niyetini ifade eden belgeler üzerinden ajanların ürettiği kod mimarisini denetlemek.
Somut sonuçlar ve kanıtlar
- Microsoft Research, Pet Store adlı yaklaşık 5.000 satırlık Rust tabanlı tam yığın web uygulamasının oturum açma mantığını PDD Kit ile doğruladı. (Kaynak)
Sınırlar ve açık kalan sorular
PDD Kit şu anda yalnızca Verus dilinin desteklendiği Rust projelerinde çalışmaktadır. Doğrulama süreci matematiksel kanıtlar sunsa da; şifreleme kütüphaneleri, veritabanı sorguları ve sistem saati gibi dış bağımlılıklar ve harici bileşenler kanıt kapsamı dışındadır ve güvenilir sınırlara dayanan geleneksel testlerle doğrulanması gerekir.