Axiom Math, Stacks Project'i Lean ile doğruladı

Axiom Math, matematiğin en kapsamlı insan yapımı derlemelerinden biri olan Stacks Project'i resmen doğruladığını duyurdu. Üstelik çalışmayı şirketin yapay zeka ajanları yürüttü. Ajanlar, kütüphanenin yaklaşık 7.654 sayfasını yaklaşık 16 milyon satırlık koda çevirdi. Böylece projedeki sonuçlar makine tarafından satır satır denetlenmiş oldu.

Yapay zeka çıktılarının kalitesi son dönemde sık tartışılıyor. Örneğin OpenAI yalnızca geçen ay, matematiğin en zor problemlerine çözüm iddiası taşıyan 719 metin yayımladı. Ancak bilgisayar kontrolleri bile bazen hata yapabiliyor. Bu nedenle 1,6 milyar dolar değerindeki girişim, hızı kesmek yerine daha sağlam bir zemin kurmayı seçti.

Axiom Math Stacks Project'i Nasıl Doğruladı?

Stacks Project'i Columbia'dan matematikçi Johan de Jong, 2005'te açık kaynaklı bir referans olarak başlattı. O günden beri birçok matematikçi projeye katkı veriyor. Kütüphane, üniversite düzeyindeki cebirden cebir, geometri ve sayı teorisinin en ileri fikirlerine kadar uzanıyor. Nitekim Columbia'dan Peter Woit, projeyi 20. yüzyılda matematiği temelden yeniden kuran Bourbaki kitaplarına benzetiyor ve gerçekten benzeri olmadığını söylüyor.

Doğrulama süreci şöyle işliyor. Matematikçiler ispatı Lean adlı bir programlama diliyle koda döker. Ardından ispat asistanı denen bir program kodu satır satır kontrol eder. Denetimden geçen ispat, mantıksal olarak sağlam kabul edilir. Mühendisler de aynı fikri, yani biçimsel doğrulamayı, çip tasarımlarının çalıştığını teyit etmek için kullanıyor. Fransa'daki araştırmacılar ise aile yardımlarını hesaplayan bir yazılımdaki hataları bu yöntemle yakaladı.

Stacks için tek tek teorem denetlemek işin yalnızca bir kısmı. Çünkü teoremler ve tanımlar birbirine bağlı, her biri öncekilerin üzerine kuruluyor. Bu yapı bir aile ağacına benziyor. Dolayısıyla ekip, yaklaşık 16 milyon satırlık Lean kodunda tüm bağlantıları korumak zorundaydı. Axiom CEO'su Carina Hong, başta işin yürüyeceğinden emin olmadıklarını söylüyor. Ona göre büyük ve hassas şeyler pek bir arada bulunmaz; teoremlerin tutarlı, tanımların da birbiriyle çelişmeyen yapıda olması gerekir.

Ekip, ajanlara gevşek bir hiyerarşi verdi ve hepsini paralel çalıştırdı. Teknik ekipten Ashvin Swaminathan'a göre ajanlar kendi görevlerini buldu ve aynı anda yürütülebilecek işleri belirledi. Axiom Math ayrıca matematikte başarılı olsun diye kendi modellerini eğitti. Hong'a göre diğer doğrulama girişimlerinin çoğu bu yolu izlemedi. Başlangıçta ajanlara insani bir estetik anlayışı öğretme işini şirketin Lean uzmanlarından biri üstlendi. Hong, ajanların zamanla bunu kendi kendine edindiğini belirtiyor.

Cebirsel Geometrideki Boşluk Kapandı

Swaminathan, biçimselleştirilmiş matematikte dev bir kara delik bulunduğunu anlatıyor. Bu boşluk cebirsel geometriyi de kapsıyordu. Bu nedenle Lean ile yeni cebirsel geometri çalışmalarını denetlemek isteyen araştırmacıların dayanabileceği çok az şey vardı. Swaminathan'a göre artık böyle bir zemin var.

Axiom, doğrulanan her sonucun bir yapı taşına dönüştüğünü savunuyor. Böylece gelecekteki ispatlar sıfırdan başlamak yerine denetlenmiş matematiğe yaslanabilir. UCLA'dan Fields Madalyası sahibi matematikçi Terence Tao da genel mantığı şöyle özetlemişti: elinizde ne kadar çok biçimsel ispat varsa, o kadar çok yenisini üretebilirsiniz.

Yazılım Dünyası İçin Ne Anlama Geliyor?

Axiom Math'in hedef kitlesi yalnızca matematikçiler değil. Geliştiriciler uzun süredir kodlarının hatasız ve güvenlik açıklarından arınmış olduğunu garanti etmekte zorlanıyor. Yapay zeka ajanları dünyadaki kodun daha büyük bölümünü yazdıkça bu sorun büyüyor. Şirket, geleceğin yazılımının tıpkı Stacks gibi doğrulanmış temellere oturması gerektiğini düşünüyor.

Swaminathan'a göre matematik, bu tür altyapıların kurulmaya başlanacağı alan ve edinilen beceri başka alanlara aktarılabiliyor. Ajanlar Axiom'un kodunu okuyup anlayabilir ve üzerine yeni altyapılar inşa edebilir. Lean ile oluşturulan bu biçimsel yapı, ajanların üzerine basacağı zemin işlevi görüyor.

Hong, Stacks'in inşa biçimini, yani paralel çalışmayı ve görevi ajanın kendisinin seçmesini, yapay zekanın gelecekteki işlerinin örneği olarak görüyor. Ona göre ajanların düşük kaliteli çıktı üretmemesi için iyi kurulmuş, yeniden kullanılabilir bir bilgi birikimi gerekir. Çünkü başta kötü mühendislik kararları alınırsa sınırları genişletmek zorlaşır.

Hong, tüm kodlama şirketlerine bu ölçekte biçimselleştirme üzerine çalışmaları için açık bir meydan okuma yaptı. Stanford'daki matematik doktorasını bırakıp şirketi Mart 2025'te kuran 25 yaşındaki CEO'nun girişimi, Mart ayında Menlo Ventures liderliğinde 200 milyon dolarlık A serisi yatırım almıştı.