Giriş
Son yıllarda Yapay Zeka (YZ), uygulamalı formel yöntemler alanında büyük ilerlemeler kaydetti. Bu yazıda Specula ekibi, Büyük Dil Modelleri (LLM'ler) üzerinde TLA+ ile sistem kodunu modelleme deneyimlerini paylaşıyor. LLM'lerin, karmaşık bir uygulamadan mantığı soyutlayıp doğru bir formel model haline getirip getiremeyeceğini sorgulayan önemli bulgular sunuyor.
SysMoBench Nedir?
SysMoBench, LLM'lere on bir farklı sistemi sunarak, ürettikleri TLA+ spesifikasyonlarını otomatik olarak değerlendiriyor. Bu sistemler, eşzamanlı senkronizasyon ve dağıtık protokolleri kapsıyor. Her görev için kaynak kodu, iz toplama harnesi ve bir invariat şablonu sağlanıyor.
Değerlendirme Aşamaları
SysMoBench, dört aşamada değerlendirme yapıyor:
Sözdizimi Aşaması: Spesifikasyonun derlenip derlenmediğini kontrol ediyor.
Çalışma Zamanı Aşaması: TLC'nin (TLA+ Model Checker) spesifikasyonu hatasız çalıştırıp çalıştırmadığını kontrol ediyor.
Uyum Aşaması: İz doğrulaması yaparak, spesifikasyonun kodla tutarlılığını kontrol ediyor.
Invariat Aşaması: Spesifikasyonun temel güvenlik ve canlılık özelliklerini karşılayıp karşılamadığını kontrol ediyor.
Bu aşamalar, yalnızca ders kitabını ezberleyen bir spesifikasyon ile sistemi gerçekten modelleyen bir spesifikasyon arasındaki farkları ortaya koyuyor.
LLM Modelleme Desenleri
Bugünün önde gelen LLM'lerini SysMoBench üzerinde test ettiğimizde, iki ana sorun ortaya çıkıyor: 1) Spesifikasyon, gerçek sistemin asla ulaşamayacağı durumlara giriyor; 2) Spesifikasyon, gerçek sistemin her zaman ulaşması gereken durumlara ulaşamıyor. Bu iki hata modu, uyum ve invariat puanlarında doğrudan kendini gösteriyor. Örneğin, LLM'ler ortalama %46 uyum ve %41 invariat puanı alıyor.
Örnek: ZooKeeper Hızlı Lider Seçimi
LLM'lerin, ZooKeeper'ın hızlı lider seçim algoritması için yazdığı spesifikasyon, bu hata modlarını net bir şekilde gösteriyor. LLM, her sunucunun alıcı kümesini (recvset) bir küme birleştirmesi olarak tanımlıyor. Ancak gerçek sistem, yalnızca yeni oyu tutarak eski oyu güncelliyor. Bu tür bir yanlış anlama, seçim sürecinde sorunlara yol açıyor.
Geçiş Doğrulama: Eylem Granülaritesinde Okuma
SysMoBench, her aşamada eylem ya da invariat granülaritesinde detaylar sunarak, eylemlerin nasıl yanlış eşleştiğini ortaya koyuyor. Geçiş doğrulama, gerçek sistemlerin çalışma izlerini toplayarak, her bir geçişin doğru olup olmadığını kontrol ediyor. Bu, hangi spesifik eylemin uyumsuz olduğunu belirtmek açısından son derece değerlidir.
Sonuçlar: Puanların Farklılaştığı Yerler
Yapılan değerlendirmeler, LLM'lerin yalnızca sözdizimsel ve çalışma zamanı aşamalarında başarılı olduğunu, ancak gerçek sistemleri modelleme aşamasında ciddi sorunlar yaşadığını gösteriyor. Bu durum, LLM'lerin yalnızca ders kitaplarını temel alarak modelleme yaptığını ortaya koyuyor. Gerçek uygulamalara özgü detayları göz ardı ediyorlar.
Gelecek Perspektifleri
LLM'lerin gerçek dünya sistemlerini modelleme yetenekleri üzerine daha fazla araştırma yapılması gerekiyor. SysMoBench, bu alandaki boşlukları kapatmak için önemli bir adım olarak öne çıkıyor. LLM’lerin potansiyeli büyük, ancak bu potansiyeli gerçekleştirmek için daha derinlemesine bir anlayışa ihtiyaç var.
