Anthropic, Claude modelinin mevcut kodlar için otomatik olarak biçimsel doğrulama kanıtları üretebildiğini duyurdu. Google’ın OSS‑Fuzz projesindeki 123 kütüphaneyle yapılan bir testte Claude, birkaç hafta içinde yaklaşık 180 milyon satır kanıt üretti. Kanıtlar Rocq doğrulayıcısı tarafından kontrol edildi. Anthropic, süreçte neredeyse hiç insan denetçiye ihtiyaç duyulmadığını söylüyor.
Sistem gerçekte ne yaptı?
Claude yeni programlar yazmadı. Bunun yerine çökme testlerindeki örnekleri matematiksel ifadelere dönüştürdü, derlenmiş makine kodunu analiz etti ve kodun bu ifadeleri karşıladığını gösteren biçimsel kanıtlar üretti. Model bir hatayla karşılaştığında kodu kendisinin düzeltmesine izin verildi. Claude, popüler bir PDF okuyucuyu bir hafta boyunca incelerken, genellikle bir yılda bildirilen sayıda güvenlik hatası buldu. Başka bir kütüphanede ise on yılı aşkın süredir gizli kalmış mantıksal bir hatayı ortaya çıkardı.
Sınırlamalar ve maliyetler
Anthropic, kanıtların yalnızca belirli bir işlemci mimarisinde çalışan, tek iş parçacıklı ve 64 MB’ın altındaki girdileri kullanan programlar için geçerli olduğu konusunda uyarıyor. İşlem gücü ihtiyacı yüksek; tek bir kanıtın üretimi yüz milyonlarca token gerektirebiliyor. Ancak şirket toplam harcamayı açıklamadı. Daha küçük çaplı bir testte, yeni Opus 5.5 modelinin kanıtların yarısını önceki modele göre yaklaşık %40 daha az token kullanarak tamamlayabildiği görüldü.
Neden önemli
Yapay zekâ kodu otomatik olarak doğrulayabilirse geliştiriciler, özellikle güvenlik açısından kritik yazılımlarda, hata aramaya ve yamaları incelemeye daha az zaman ayırabilir. Ancak mevcut yaklaşım donanım ve girdi boyutu bakımından katı sınırlara sahip; bu nedenle günlük uygulamaların çoğunda geleneksel testlere hâlâ ihtiyaç var.
