Ne oldu?

Anthropic, Claude modelini yazılım doğrulama firması Theorem ile birlikte 123 açık kaynak kütüphanede biçimsel doğrulama (formal verification) için kullandığını açıkladı. Çalışma kapsamında 239 program giriş noktası için matematiksel kanıtlar üretildi ve yüzlerce hata bulundu.

Biçimsel doğrulama nedir?

Klasik testler, programı seçilen girdilerle dener; fuzzing araçları çok sayıda sıra dışı girdi üretir ama tüm olasılıkları tüketemez. Biçimsel doğrulama ise kodun belirli koşullar altında belirli kurallara uyduğunu matematiksel olarak kanıtlamaya çalışır. Anthropic, mevcut fuzz testlerini Claude ile matematiksel spesifikasyonlara dönüştürdü; model ardından bu giriş noktalarının tanımlı koşullarda çökmeyeceğini gösteren kanıtlar üretti.

Öne çıkan bulgular

  • Bir kütüphanede, sıkıştırma açma sırasında sınır dışı yazmaya yol açabilecek bir sayaç alt taşması bulundu; hatanın tetiklenmesi yaklaşık 20 MB'lık nadir düzenlemeli bir girdi gerektiriyordu.
  • Bir görüntü çözücüde, ancak 64 MB girdi ve 2 GB'tan fazla bellekle ortaya çıkan bir hata saptandı.
  • Aynı dosyaya iki tanıtıcı üzerinden erişen belirli bir işlem sırasına bağlı sınır dışı okuma hatası tespit edildi.
  • libexpat XML ayrıştırıcısındaki bilinen bir açık yeniden keşfedildi.
  • Uygulamanın yükleyebileceği dosyaları kısıtlayan bir özelliğin atlatılmasına yol açabilecek mantık hatası da bulundu.

Kanıtların sınırları

Anthropic, biçimsel doğrulanmış yazılımın otomatik olarak hatasız olmadığı uyarısını yaptı. Garantiler yalnızca her kanıtta tanımlanan özellikler, girdiler ve varsayımlar için geçerli. Mevcut çalışma tek iş parçacıklı, statik bağlı RISC-V programlarını modellenmiş bir Linux ortamında kapsıyor; çoğu üretim sistemi farklı mimari ve yapılandırmalar kullanıyor. Araştırmacıların matematiksel modellerin gerçek işlemci ve işletim sistemlerini doğru temsil etmesini sağlaması gerekiyor.

Neden önemli?

Claude yaklaşık 180 milyon satır kanıt kodu üretti; tipik bir kanıt yaklaşık 600 bin satır tutuyor. Rocq adlı ayrı bir araç kanıtları spesifikasyonlara karşı denetledi, böylece geliştiricilerin her satırı elle incelemesi gerekmedi. Anthropic, daha iyi modeller ve yeniden kullanılabilir kanıtlarla kritik yazılım bileşenlerini doğrulamanın maliyetinin düşmesini bekliyor.