Claude, 123 Açık Kaynak Kütüphanenin Çökmeyeceğini Matematiksel Olarak Kanıtladı

Anthropic, Claude modelinin 123 açık kaynaklı kütüphanenin derlenmiş kodunun belirli koşullarda çökemeyeceğini gösteren, makine tarafından doğrulanmış matematiksel kanıtlar yazdığını açıkladı. Şirketin Frontier Red Team ekibi ve biçimsel yöntemler firması Theorem’in 22 Ekim’de duyurduğu çalışma, yıllardır gözden kaçan hataları da ortaya çıkardı.

Fuzz testlerinden matematiksel kanıtlara

Ekip, Google’ın OSS-Fuzz programındaki fuzz testlerini (yazılıma rastgele girdiler göndererek hata arayan testler) biçimsel birer şartnameye dönüştürdü. Kural basitti: RISC-V makine koduna derlenen program, 64 MB’tan küçük hiçbir girdide çökmemeliydi. Claude birkaç hafta içinde bunu 123 kütüphanedeki 239 giriş noktası için kanıtladı. Kanıtlar Rocq kanıt dilinde toplamda yaklaşık 180 milyon satıra ulaşıyor; bir kanıt ortalama 600 bin satır tutuyor. Rocq denetleyicisi her kanıtın şartnameyle uyuştuğunu otomatik doğruluyor, yani geliştiricilerin kodu satır satır okumasına gerek kalmıyor.

Trilyonlarca testin kaçırdığı hatalar

Kanıtların yazımı sırasında yüzlerce hata ortaya çıktı. Claude bunları yamaladı ve düzeltilmiş kodu yeniden kanıtladı. Bir açıcı (decompressor) programında bellek sınırları dışına yazmaya yol açan bir sayaç taşması bulundu; hata yalnızca yaklaşık 20 MB’lık ve nadir bir düzene sahip girdilerde tetikleniyordu. Bir görüntü kod çözücüsündeki sınır dışı okumayı tetiklemek için ise 64 MB’lık girdi ve 2 GB’tan fazla bellek gerekiyordu. Claude ayrıca libexpat’taki bilinen bir güvenlik açığını yeniden keşfetti ve bir dosya kısıtlama özelliğinin her zaman uygulanmadığı bir mantık hatası buldu.

Garantinin sınırları ve yeni dönem

Anthropic, kanıtların kütüphanelerin hatasız olduğu anlamına gelmediğini vurguluyor. Kanıtlar, Linux üzerinde RISC-V işlemcide çalışan, sabit bellek bütçeli ve tek iş parçacıklı statik bir ikili dosyayı varsayıyor. Kalan hatalar ya kapsam dışında kalıyor ya da donanım ve işletim sistemi modelleri, teorem ifadeleri ve Rocq denetleyicisi gibi güvenilen bileşenlerde bulunuyor. Yine de şirket, yapay zekâ hata bulmayı kolaylaştırdığı için yalnızca test yapmanın yetmeyeceğini savunuyor. Theorem ise OSS Verify programıyla uygun açık kaynak projeler için aynı süreci ücretsiz çalıştırmayı teklif ediyor.