Anthropic, Claude ile 123 kütüphanenin güvenliğini kanıtladı

Anthropic, Claude modelinin, 123 açık kaynaklı kütüphaneden derlenen kodun tanımlanmış koşullar altında çökemeyeceğini gösteren makine onaylı matematiksel kanıtlar yazdığını belirtiyor. Şirketin Frontier Red Team ekibi tarafından 22 Ekim'de yayınlanan araştırmaya göre, model bu süreçte trilyonlarca test çalışmasına rağmen yıllardır tespit edilemeyen hatalar da buldu. Çalışma, resmi yöntemler firması Theorem ile birlikte yürütüldü.anthropic.com

Şirket bunu, "yapay zekayı üretim yazılımlarına assembly kodu düzeyinde resmi doğrulama uygulamak için kullanan ilk büyük ölçekli çaba" olarak nitelendiriyor. Anthropic, yapay zekanın artık hataları kolayca bulup istismar edebildiğini, bu nedenle yazılımı savunmak için sadece test etmenin artık yeterli olmadığını savunuyor.anthropic.com

Fuzz testlerinden kanıtlara

Ekip, Google'ın OSS-Fuzz programındaki fuzz testleriyle işe başladı ve her birini resmi bir şartnameye dönüştürdü. Kural, testin RISC-V makine koduna derlendiğinde 64 MB'tan küçük herhangi bir girişte asla çökmemesiydi. Birkaç hafta içinde Claude, 123 kütüphanedeki 239 giriş noktası için bunu kanıtladı. Anthropic'e göre kanıtlar Rocq kanıt dilinde yaklaşık 180 milyon satır koda ulaşıyor ve tipik bir kanıt yaklaşık 600.000 satır sürüyor. Interesting Engineering'in bildirdiğine göre, Rocq kanıt denetleyicisi her kanıtın kendi şartnamesiyle eşleştiğini doğruluyor, bu nedenle geliştiricilerin oluşturulan kodu satır satır incelemesine gerek kalmıyor.interestingengineering.com+1

Anthropic, kanıtların bir alt kümesinin, arkasındaki RISC-V ve Linux semantiği ile birlikte yayınlandığını belirtti. Unite.AI'nin haberine göre Theorem, OSS Verify programı aracılığıyla uygun açık kaynaklı projeler için aynı hattı ücretsiz olarak çalıştırmayı teklif ediyor. Theorem ayrıca bakım sorumlularının kaydolmasına yardımcı olmak için bir Claude yeteneği de yayınladı.unite.ai+1

Fuzzer'ların gözden kaçırdığı hatalar

Kanıtların yazılması, Claude'un düzeltilmiş kodu kanıtlamadan önce yamaladığı yüzlerce hatayı ortaya çıkardı. Bir dekompresörde, yalnızca 20 MB civarındaki girdilerde ve nadir bir düzende ortaya çıkan, sınır dışı yazmaya yol açan bir sayaç eksikliği buldu. Bir görüntü kod çözücüsündeki başka bir sınır dışı okuma hatası ise 64 MB girdi ve 2 GB'tan fazla bellek gerektiriyordu. Araştırmaya göre Claude ayrıca libexpat'teki bilinen bir güvenlik açığını yeniden keşfetti ve bir uygulamanın hangi dosyaları yükleyebileceğini kısıtlaması amaçlanan bir özelliğin her zaman uygulanmadığı bir mantık hatası buldu.anthropic.com

Garantinin sınırları

Anthropic, kanıtların kütüphanelerin hatasız olduğu anlamına gelmediği konusunda uyardı. Bunlar, Linux altında bir RISC-V CPU üzerinde çalışan, sabit bellek bütçesine sahip tek iş parçacıklı statik bir ikili dosyayı varsayıyor. Şirketin yazdığına göre, kalan hatalar ya kanıtların kapsamı dışındadır ya da donanım, işletim sistemi modelleri, teorem ifadeleri ve Rocq denetleyicisinin kendisi gibi güvenilir bileşenlerde yer almaktadır. Interesting Engineering, dağıtılan sistemlerin çoğunun diğer işlemci mimarilerini veya yapılandırmalarını kullandığını belirtti.interestingengineering.com+1

Anthropic yine de ekonominin değiştiğini düşünüyor. Ekip, "Tüm geliştiricileri, özellikle daha önce daha az yetenekli modellerle deneyip başarısız olanları, LLM'lerle resmi doğrulamayı keşfetmeye teşvik ediyoruz," diye yazdı.anthropic.com