Yapay zeka dillerin anlambilimini yorumlayıcı ikilileriyle doğruluyor

Yazılım doğrulama çalışmalarında büyük dil modellerinin kullanımı artarken en büyük darboğaz, dillerin matematiksel kurallarını tanımlayan anlambilim (semantik) şartnamelerinin doğruluğu haline geldi. Basis araştırmacıları Kiran Gopinathan, Nikhil Pimpalkhare, Yiyun Liu ve Zenna Tavares, dillerin resmi anlambilimini doğrulamak için mevcut yorumlayıcıları temel alan yeni bir yöntem geliştirdi. Yöntem kapsamında, bir dilin yorumlayıcısı RISC-V makine koduna derleniyor ve yapay zeka ajanları tarafından Lean 4 ortamında bu ikili kod ile dildeki soyut kuralların birebir örtüştüğü matematiksel olarak kanıtlanıyor.

Araştırmacılar, 1.855 satırlık C dilinde yazılmış bir WHILE yorumlayıcısını GCC ile derleyerek 25 bin 336 makine koduna dönüştürdü. LLM ajanları tarafından yazılan 400 satırlık semantik kuralları, derlenmiş RISC-V ikilisiyle karşılaştırıldı. Test paketlerinin tespit edemediği 63 baytlık metin kesilmesi ve 64 bit taşma gibi örtük davranışlar, matematiksel kanıtlama aşamasında ortaya çıkarılarak düzeltildi. Bellek yönetimindeki doğrulamaları çözmek için MachCSL ayrık mantığı (separation logic) iris-lean kütüphanesine aktarıldı ve başlangıçta 1 milyon satır olan kanıt 200 bin satırın altına indirildi.

Elde edilen kesinleştirme teoremi sayesinde doğrulanmış anlambilim güvenli bir arayüze dönüştürüldü. Araştırma ekibi, Lean üzerinde doğrulanan anlambilim kurallarını temel alarak üç gün içinde tip denetleyicisi, program mantığı ve soyut yorumlayıcı gibi araçlar inşa etti. Çalışma, anlambilim belgeleri olmayan programlama dilleri için derlenmiş ikili kodların zemin gerçeklik olarak kabul edilip LLM tabanlı uçtan uca yazılım doğrulamasına zemin hazırlayabileceğini gösterdi.