Yaklaşık 16 milyon satır matematik kodu yayımlandı; AI’ın yazdığı bölümler insan incelemesi bekliyor

Axiom Math, Stacks Project’te biçimselleştirilebilen matematiksel içerikleri yaklaşık 16 milyon satırlık Lean kodu olarak yayımladı. AI ajanlarının yazdığı kanıtlar bilgisayarla denetlenebiliyor; ancak bu bölümlerin kaynak metinle karşılaştırılarak insanlar tarafından incelenmesi gerekiyor.

Axiom Math, ayın 4’ünde yayımladığı açıklamada yaklaşık 7.500 sayfalık Stacks Project’i yeniden kullanılabilir tek bir biçimsel matematik kütüphanesine dönüştürdüğünü bildirdi. Açık depoda kaynak metindeki maddeler, bunlara karşılık gelen biçimsel önermelerle eşleştiriliyor.

Açık deponun README dosyasına göre kod Lean 4 ve Mathlib matematik kütüphanesini temel alıyor ve Apache 2.0 lisansı altında sunuluyor. Herkes depoyu indirip inceleyebiliyor.

Stacks Project, cebirsel geometri tanımlarını, teoremlerini ve kanıtlarını içeren açık kaynaklı bir başvuru kitabı. Proje 2005’te başladı. Kaynaktaki her maddeye, tanımlar ve teoremler arasındaki bağımlılıkların izlenmesini sağlayan benzersiz bir etiket veriliyor.

Axiom Math bu etiketleri Lean koduyla da ilişkilendirdi. Böylece araştırmacılar kaynak maddeleri bunlara karşılık gelen biçimsel önermelerle yan yana inceleyebiliyor.

Biçimselleştirme, insanların okuyabildiği matematiksel önerme ve kanıtları bilgisayarların işleyebileceği bir dile aktarma süreci. Lean çekirdeği, girilen biçimsel önerme için kanıtın mantıksal olarak geçerli olup olmadığını denetliyor.

Bu denetim, biçimsel önermenin kaynak metindeki anlamı doğru yansıttığını garanti etmiyor. Kaynak metinle kodun aynı anlama gelip gelmediğini belirlemek için ayrıca karşılaştırma yapılması gerekiyor.

Açık deponun kapsamı, biçimselleştirilebilen Stacks Project etiketleriyle sınırlı. Örnekler, alıştırmalar ve bazı açıklamalar tamamlanmamış işler arasında yer alıyor. Dolayısıyla yaklaşık 7.500 sayfanın tamamı koda aktarılmış değil.

Kodun inceleme durumu ikiye ayrılıyor. ‘StacksCore’, insanların kaynak metinle karşılaştırarak incelediği bölümleri; ‘StacksFrontier’ ise AI ajanlarının yazdığı ve henüz insan incelemesinden geçmemiş bölümleri kapsıyor.

Axiom Math’in biçimselleştirme üst verileri, genel inceleme durumunu şirketin kendi değerlendirmesi olarak gösteriyor. Bu nedenle AI tarafından yazılan kodun makineyle denetlenmiş olması ile insanların kodu kaynak metne göre incelemiş olması birbirinden ayrı değerlendirilmeli.

Axiom Math, biçimselleştirme sırasında kaynak metindeki onlarca önermenin ek varsayımlara ihtiyaç duyabileceğini veya belirli koşullarda geçerli olmayabileceğini tespit ettiğini açıkladı. Bu, şirketin aktarımı; özgün projenin doğruladığı bir hata listesiyle aynı şey değil.

Özgün projenin yöneticileri 21 Ekim’de, AI tarafından yazılan yorumların veya çekme isteklerinin şimdilik gönderilmemesini duyurdu. Axiom Math, biçimselleştirme sonuçlarını özgün projeden ayrı kendi deposunda tutuyor.

5 Kasım’da açık depoya, derleme hatalarını düzeltmek amacıyla iki dosyayı değiştiren bir gönderim eklendi. Bir gönderimin eklenmiş olması, düzeltilmiş sürümün başarıyla derlendiğini göstermiyor.

AI’ın matematik sorularına yanıt vermenin ötesine geçerek çözümleri biçimsel olarak doğrulamasını ele alan araştırma eğilimi, Google DeepMind’in matematik alanındaki iş birliği ve biçimsel kanıt sistemleriyle ilgili TokenPost haberinde de aktarılmıştı. Bu çalışma, AI tarafından yazılan matematik kodunun ölçeğini ve insan incelemesine duyulan ihtiyacı birlikte ortaya koyuyor.

Axiom Math, cebirsel geometrinin uygulama alanları arasında eliptik eğriler ve dijital kriptografiyi saydı. Ancak şirket, bu biçimselleştirme çalışmasının belirli bir blokzincire veya kripto varlığa uygulandığını duyurmadı. Matematik kaynağı Stacks Project, Bitcoin tabanlı Stacks (STX) ağından ayrı bir proje.

Açık depo, örneklerin ve alıştırmaların biçimselleştirilmesini ve AI tarafından yazılan bölümlerin insanlarca incelenmesini katkı gerektiren işler arasında gösteriyor.