Axiom Math, Stacks Project'ı yapay zekâ ajanlarıyla biçimsel olarak doğruladı

Axiom Math, insanların yazdığı en büyük matematik külliyatlarından biri olan Stacks Project'ı biçimsel olarak doğruladığını duyurdu. 1,6 milyar dolar değerlemeye ulaşan girişim, kütüphaneyi yapay zekâ ajanlarıyla yaklaşık 16 milyon satırlık bilgisayarca denetlenebilir koda dönüştürdü.

Şirketin açıklamasına göre Stacks Project, yaklaşık 7.654 sayfadan oluşuyor. Axiom'un ajanları bu metni, matematikçilerin ispatları yazarken kullandığı Lean programlama diline çevirdi. Lean kodunu satır satır kontrol eden ispat asistanı, ispat geçerse sonucun mantıksal olarak sağlam olduğunu gösteriyor.

Stacks Project nedir, neden önemli?

Stacks Project'ı 2005'te Columbia Üniversitesi matematikçisi Johan de Jong açık kaynak bir referans olarak başlattı. O tarihten bu yana matematikçiler projeye katkı verdi; kütüphane üniversite düzeyindeki cebirden cebir, geometri ve sayılar teorisindeki en ileri konulara kadar uzanıyor.

Columbia'dan Peter Woit, projeyi 20. yüzyılda matematiği temellerinden yeniden kuran ünlü Bourbaki kitaplarına benzeterek "karşılaştırılabilecek başka bir şey yok" demişti. Kütüphanedeki teorem ve tanımlar birbirine bağlı olduğundan, her birini ayrı ayrı kontrol etmek yeterli olmuyor; tüm bağlantıların korunması gerekiyor.

Biçimsel doğrulama ne işe yarıyor?

Biçimsel doğrulama, bir ispatın altındaki yapının sağlam olduğundan emin olma yöntemi. Matematikçi ispatı Lean'de kod olarak yeniden yazıyor, ispat asistanı da kodu satır satır denetliyor. Aynı yaklaşımı mühendisler çip tasarımlarını doğrulamak için kullanıyor; Fransa'daki araştırmacılar da aile yardımlarını hesaplayan yazılımlardaki hataları yakalamak için bu yönteme başvurdu.

Axiom CEO'su Carina Hong, projenin ilk aşamada kesin sonuç vereceğinden emin olmadıklarını söyledi. Hong, TechCrunch'a yaptığı açıklamada "Hayatta büyük olan şeylerle hassas olan şeyler pek bir araya gelmez" dedi ve ekledi: "[Stacks] matematiğin temeli olan bir sonuçlar bütünü. Teoremlerin tutarlı olmasını, çelişkili olmamasını istiyorsunuz. Tanımların birbiriyle kavga etmemesini istiyorsunuz."

Yapay zekâ ajanları nasıl çalıştırıldı?

Hong, 2025'in mart ayında Stanford matematik doktora programını bırakarak şirketi kurdu. Aynı ay Axiom, Menlo Ventures liderliğinde 200 milyon dolarlık Series A yatırımı aldı.

Şirket, projeyi yürütmek için ajanlara gevşek bir yapı verip onları paralel çalıştırdı. Axiom'un teknik kadrosundan Ashvin Swaminathan, "Stacks'te bir hiyerarşi dayattık ... [ama] her bir ajanın ne yaptığını dikte eden tam bir hiyerarşi değildi bu" dedi. Swaminathan'a göre ajanlar kendilerine görev buldu ve paralel yürütebilecekleri işleri belirledi.

Axiom ayrıca kendi modellerini matematikte iyi olacak şekilde eğitti. Hong, çoğu doğrulama girişiminin bu yolu izlemediğini söyledi. Ekip başlangıçta ajanlara insani bir zevk anlayışını Lean uzmanlarından öğretti; Hong'a göre zamanla ajanlar bu anlayışı kendi başlarına geliştirdi.

Neden önemli?

Swaminathan, biçimselleştirilmiş matematikte cebirsel geometriyi kapsayan büyük bir boşluk olduğunu belirtti. Ona göre bu alanda yeni çalışmalarını Lean ile kontrol etmek isteyen araştırmacıların üzerine inşa edebileceği çok az şey vardı; artık var.

Axiom, doğrulanan her sonucun bir yapı taşı haline geldiğini, böylece gelecekteki ispatların sıfırdan başlamak yerine denetlenmiş matematiğe dayanabileceğini savunuyor. Şirketin hedef kitlesi yalnızca matematikçiler değil. Yazılımcılar kodlarının hata ve güvenlik açıklarından arınmış olduğunu uzun süredir garanti edemiyor; yapay zekâ ajanları dünyanın kodunun giderek daha fazlasını yazdıkça bu sorun büyüyor.

Axiom, teknoloji devlerinin ajanlarına güvenilir bir temel sunmak için matematiği başlangıç noktası olarak görüyor. Swaminathan, "Ajanlar bizim kodumuzu okuyabilir, anlayabilir ve üzerine yeni altyapı kurabilir" dedi.

Hong, yapay zekâ ajanlarının niteliksiz çıktı üretmemesi için yeniden kullanılabilir, sağlam bir bilgi kütüphanesine ihtiyaç duyacağını savunuyor. Hong, kodlama şirketlerine açık bir çağrı da yaptı: "Bu ölçekte biçimselleştirme üzerinde çalışmaları için tüm kodlama şirketlerine açıkça meydan okuyorum."