Anthropic, 123 açık kaynak kütüphanede 239 giriş noktasını doğruladı

Anthropic, Claude’u kullanarak 123 açık kaynak kütüphanesindeki 239 test giriş noktasının belirli koşullar altında güvenli olduğunu matematiksel olarak kanıtladı.

Anthropic Frontier Red Team, 22’sinde yayımladığı araştırmada doğrulama şirketi Theorem ile birlikte çalıştığını bildirdi. Araştırmacılar mevcut testleri doğrulama koşullarına dönüştürdü ve Claude’un yazdığı kanıtları ayrı bir araçla kontrol etti.

İncelenen kütüphaneler, Google’ın açık kaynak hata bulma projesi OSS-Fuzz’da yer alıyor. Araştırmacılar mevcut fuzz testlerini, “64 MB’tan küçük herhangi bir girdi programın beklenmedik şekilde sonlanmasına, bellek güvenliği hatasına veya doğrulama koşulunun ihlaline yol açmaz” önermesine dönüştürdü. Kanıtları Claude yazdı, Rocq ise doğruladı.

Araştırmacılar, Claude’un bulduğu hataları birkaç hafta boyunca düzelttikten sonra 123 kütüphanedeki 239 test giriş noktasını doğruladıklarını açıkladı. Giriş noktası, bir programın belirli bir işlevini sınamak için kullanılan girdi yoludur. Kanıtlar, insanların okuduğu kaynak kodu yerine derlenmiş RISC-V komutları üzerinde oluşturuldu. Hazırlanan Rocq kanıtı yaklaşık 180 milyon satırdan oluşuyor.

Biçimsel doğrulama, bir programın açıkça belirtilen kurallara uyup uymadığını matematiksel olarak kontrol etme yöntemidir. Girdileri çalıştırarak hata arayan geleneksel testlerden farklı olarak, belirlenen koşullara giren tüm girdiler için bir önermeyi kanıtlar. Kanıt oluşturma sürecinde mevcut testlerin bulamadığı hatalar da ortaya çıktı. Araştırmacılar bu hataları düzeltti ve güncellenen koda uygun doğrulama koşulları hazırladı.

Sonuçlar, sabit miktarda bellek kullanan ve Linux’ta çalışan tek iş parçacıklı, statik bağlantılı RISC-V programlarıyla sınırlı. Her kütüphanenin tüm işlevleri ya da gerçek dağıtım ortamlarının tamamı doğrulanmadı. Anthropic, kanıt araçlarının bir önermenin geçerli olup olmadığını kontrol edebildiğini, ancak önermenin gerçek kullanım koşullarını eksiksiz kapsayıp kapsamadığını değerlendiremediğini belirtti.

Araştırmacılar ayrı bir deneyde Claude’un Linux çekirdeğindeki zlib uygulamasını x86 çalıştırılabilir dosya düzeyinde doğruladığını da bildirdi. Ayrıca Rust ile yazılmış bir Python yorumlayıcısını 1,7 milyondan fazla rastgele oluşturulmuş programla sınadıklarını ve CPython ile davranış eşleşmesinin %99,95 olduğunu açıkladı. Bu iki deneyin kapsamı ve yöntemi, 123 kütüphane üzerinde yapılan RISC-V doğrulamasından farklı.

Anthropic, 36 küçük doğrulama görevini karşılaştıran sonuçları da paylaştı. Claude Opus 5.5, görevlerin yarısını kanıtlamak için Opus 5’e kıyasla yaklaşık %40 daha az token kullandı. Araştırmacılar kanıtların bir bölümünü, diğer geliştiricilerin inceleyip yeniden kullanabilmesi için yayımladı.