CPython'ın yapay zekâ ile yazılmış Lean formalleştirmesi 418 hata bildirimi ortaya çıkardı

Ne oldu

Hacker News'in ana sayfasında öne çıkan bir proje, neredeyse tüm Python kodunu çalıştıran CPython'ın iç yapısını, makine tarafından doğrulanan ispatlar için tasarlanmış bir dil olan Lean'a çevirmek üzere yapay zekâ ajanları kullandı. broyojo.com'daki proje raporuna göre ekip, Opus 5.5 modelini CPython 3.15.2'ye yönlendirerek ajanların iç fonksiyonlarını Lean'da yeniden yazmasını ve ardından bunlar hakkında özellikler kanıtlamasını sağladı.

Şimdiye kadar elde edilen çıktı: 1.539 dosyaya yayılan 613.318 satır Lean kodu; 18.898 teorem ve lemma içeriyor ve hepsi her derlemede Lean'ın ispat denetleyicisi tarafından mekanik olarak doğrulanıyor. Yaklaşık 4.071 fonksiyon, ikinci bir ajanın karşıt incelemesinden geçti. Bu süreçte çalışma, Python'a karşı 418 hata bildirimi üretti; bunların kabaca 55'i sıradan Python koduyla yorumlayıcıyı çökertebilen veya belleği bozabilen kusurları tanımlıyor.

Her fonksiyon nasıl ele alınıyor

Rapora göre her fonksiyon dört aşamadan geçiyor. Önce kopyalanıyor: Orijinal C veya Python kodu hata mesajları ve 2^64'ü aşan işaretsiz aritmetik sarması gibi tuhaflıklar dahil yakından takip edilerek Lean'da yeniden yazılıyor. Sonra test ediliyor: Lean modeli, gerçek Python ile yan yana, bilinçli olarak zorlayıcı en az 50.000 girdi üzerinde çalıştırılıyor ve herhangi bir uyuşmazlık modelin yanlış olduğu anlamına geliyor. Ardından kanıtlanıyor: ajanlar her zaman geçerli olması gereken bir şeyi ifade ediyor ve bilgisayara ispatı kontrol ettiriyor ya da iddia yanlış çıkarsa bunun yerine onu kanıtlıyorlar. Son olarak, yazım işine hiç katılmamış ayrı bir ajan sonucu orijinalle karşılaştırıyor ve bozmaya çalışıyor; yalnızca ayakta kalabilenler sayılıyor.

Kapsam alanlara göre büyük farklılık gösteriyor. Dilbilgisi kuralları tamamen bitmiş durumda; parser yüzde 31'de, yerleşik tipler yüzde 35'te, C modülleri yüzde 19'da, yorumlayıcı çekirdeği yüzde 10'da ve standart kütüphane yüzde 9'da; CPython'un tamamı için oran yüzde 16. Bellek muhasebesi gibi doğrulanacak anlamlı bir şey içermeyen kodlar bu sayıma dâhil edilmiyor.

Doğru ispatların hiçbir şey söylemediği durum

Projenin en zor sorunu ajanlara ispat yazdırmak değil, anlamlı ispatlar yazdırmaktı. Erken bir deneme her fonksiyon için en az bir ispat olacak şekilde genişlik istedi ve ajanlar bunu teslim etti. Sonraki bir inceleme, incelenen fonksiyonların yarısından azının ayakta kaldığını, bir dosyada ise yalnızca yüzde 21'inin tuttuğunu ortaya koydu. İspatların hepsi sağlam biçimde denetlenmişti; sadece trivially doğru, yani içleri boştu. "Bu fonksiyon bir sayı döndürürse o sayı sıfırdan büyüktür ya da sıfıra eşittir" gibi bir ifade, her zaman çöken bir fonksiyon tarafından da aynı şekilde sağlanır.

Çözüm, daha keskin bir inceleme ölçütü oldu: her ispat için, fonksiyonun bozuk bir versiyonunun da aynı ifadeyi sağlayıp sağlayamayacağı soruluyor. Sağlayabiliyorsa ispat reddediliyor ve kopya genellikle daha gerçekçi hâle getiriliyor; örneğin kullanıcı kodunun fonksiyonun ortasında bir hata yükseltmesine izin veriliyor.

Kabul oranı inceleme turları boyunca yükseliyor ama tekdüze değil. Objects/genobject.c beş turda 56 fonksiyonun 1'i kabul edilmiş durumdayken 56'nın 56'sına ulaştı; Objects/typeobject.c beş turda 142'nin 135'ine ulaştı; Objects/setobject.c için yedi tur gerekti. Bir gözlemci, kabul edilmiş bir ispatın gerçek Python'u yanlış tanımladığını fark ederse, ona dayanan her şey geri çekiliyor.

Bir denetleyicinin kapatamayacağı boşluk

Doğrulanmış bir ispat yalnızca bir ifadenin Lean kopyasından çıktığını garanti eder; kopyanın gerçek CPython'la eşleştiğini garanti edemez ve fark testi yalnızca birinin denemeyi akıl ettiği girdileri kapsar. Bu yüzden kabul edilen her ifade gerçek Python üzerinde ayrıca çalıştırılıyor; bu adım, mantıksal olarak geçerli olup uygulamanın gerçek davranışı konusunda yine de yanlış olan birkaç ispatı yakaladı.

Neden önemli

Python'ın kesin bir yazılı tanımı yok; pratikte dil, CPython ne yapıyorsa odur ve referans kılavuzu, bir nesnenin arama ortasında bir sözlüğü değiştirmesi ya da bir değerin C kodunun yazıldığı sınırın bir ötesinde durması gibi hataların yaşadığı garip köşeler hakkında pek bir şey söylemez. Davranış hakkında kesin ve eksiksiz ifadeler dayatmak, kodun herkesin varsaydığını yapmadığı yerleri ortaya çıkarma yollarından biri. Bu proje, yapay zekâ emeğinin mekanik doğrulamayla birleşince, anlamsız ispat sorunu karşıt inceleme ve fark testiyle mühendislik yoluyla ortadan kaldırıldığı sürece, resmî doğrulamayı büyük ve onlarca yıllık bir C kod tabanına taşıyabileceğini gösteriyor. Somut getiri, yorumlayıcıyı çökertebilen veya belleği bozabilen onlarca tanesiyle birlikte 418 gerçek kusur bildirimi.