Amazon'ın Verus'u, Firecracker ve Lambda'daki Rust koduna mekanik doğruluk kanıtları getiriyor

Verus incelemez, kanıtlar

Amazon, Firecracker ve AWS Lambda'da kullandığı Rust programlama dili doğrulayıcısı Verus hakkında bir blog yazısı yayımladı. Duyuruyu inceleyen Cole Halton'ın bir dev.to yazısına göre Verus, koda bir inceleyici gibi yaklaşmıyor. Annotate edilmiş fonksiyonlar, her olası girdi için matematiksel bir spesifikasyona karşı kontrol ediliyor ve bu kontrolde hiçbir makine öğrenmesi modeli yer almıyor. Sonuç ikili: bir implementasyon ya spesifikasyonunu karşılıyor ya da karşılamıyor; böylece doğruluk bir yargı meselesi olmaktan çıkıp geçer veya kalır durumuna geliyor.

Yazıya göre bu özellik, doğrulamayı her türlü incelemeden — ister insan ister AI — ayıran şey. "Bu diff doğru mu?" sorusunu yanıtlayan bir inceleyicinin buna eşdeğer bir aracı yok. Derleyiciler, tip kontrolcüleri ve test paketlerinin her biri gerçek bir kod tabanında "doğru" kelimesinin anlamının bir dilimini kapsar ama hiçbiri bütününü tanımlamaz.

Pekiştirmeli öğrenme karşılaştırması

Bu boşluğun neden önemli olduğunu göstermek için yazı, cite ettiği ayrı bir deneye işaret ediyor: Bu deneyde yaklaşık 4 milyar parametreli bir model, Postgres sorgu planları üretmesi için agent tabanlı pekiştirmeli öğrenmeyle post-train edildi. Ortaya çıkan planların, join ağırlıklı sorgularda Postgres'in varsayılan planlayıcısından %44,7 daha iyi olduğu raporlanıyor — oysa model başlangıçta 113 test sorgusunun 99'u için geçerli bir plan üretemiyordu.

Yazıya göre bunun işe yaramasının nedeni, ödülün — sorgu yürütme süresinin — her denemede döndürülen tek, ucuz ve nesnel bir ölçüm olması. Sorgu planlaması tam olarak ödül doğrulanabilir olduğu için eğitilebilir. Kod incelemesi ise değil: "bu değişiklik bir bug mı getirdi" sorusu için, kendisi dar bir vekil olmayan hızlı ve nesnel bir sayı yok. Yazar, otonom incelemenin tıkanmasının yapısal nedeninin bu olduğunu savunuyor — ölçemediğiniz bir davranışı pekiştiremezsiniz ve yargı bir inceleyicinin bir saatlik dikkatinden geliyorsa, pekiştirmeli öğrenmenin optimize edebileceği temiz bir şey kalmıyor.

Doğrulanamayan kısmı küçültmek

Yazının vardığı sonuç, artan hacimde AI tarafından üretilen kodu incelemenin cevabının daha iyi bir inceleyici modeli olmadığı. Doğrulanamayan kısmı küçültmek: kesin spesifikasyonlar ve gerçek testler yazmak, tip güvenliğine ve kanıtlanabilir kontrollere yaslanmak ve incelemenin mümkün olduğunca büyük kısmını bir aracın yargılayabileceği değil doğrulayabileceği kategorilere taşımak.

"Bir insan doğru olduğunu düşünüyor" durumundan "araç spesifikasyonla eşleştiğini kanıtladı" durumuna taşınan her satır, RL ile eğitilmiş sistemler dahil otomatik araçların gerçekten iyileşebileceği bir satır haline geliyor. Verus bu yelpazenin en uç noktasında duruyor ama yazar, ilkenin her titizlik düzeyinde geçerli olduğunu savunuyor: inceleyiciye doğrulanabilir bir hedef verin, görev tahminlere bağımlı olmaktan çıkar.

Yazı ayrıca bir modelin koda verdiği notun da asıl mesele olmadığına dikkat çekiyor — asıl mesele doğrulanabilir eksendir. Bu çerçevede kendi çıktısını inceleyen modeller, insan incelemesiyle aynı sorunu devralır: döngüdeki hiçbir şey iddiayı gerçekten kontrol etmez.

Neden önemli

Makine tarafından kontrol edilen kanıtlar, Firecracker ve Lambda'da çalışan Rust koduna uygulanacak kadar pratikse, resmi doğrulama artık araştırma ortamlarıyla sınırlı değil — büyük ölçekli üretim trafiğine hizmet altyapının arkasındaki toolchain'in bir parçası.

Yazının çıkardığı daha geniş sonuç kapasiteyle ilgili. AI kod üretimini hızlandırdıkça inceleme darboğaz haline geliyor ve inceleyici saatleri ölçeklenmiyor. Yargıyı doğrulamaya dönüştürmek — spesifikasyonlar, testler, tipler ve prover'lar üzerinden — incelemeyi üretimle birlikte ölçeklemenin tek kalıcı yolu olarak sunuluyor.

Açık soru kapsam. Yazının kendisi de hiçbir mevcut doğrulayıcının, Verus dahil, gerçek bir kod tabanında "doğru" kelimesinin bütün anlamını yakalamadığını kabul ediyor; yani yargı tamamen kaybolmuyor. Ama belirlenen yön somut: doğruluğun ne kadarı bir aracın kontrol edebileceği bir spesifikasyon olarak ifade edilebilirse, o kadarı otomatikleştirilebilir hale geliyor — ve o kadar azı görüşe bağımlı kalıyor.