Yapay zekânın neredeyse her hafta yeni bir matematik sorunu çözdüğü hissi veriyor. Geçen ay yalnızca OpenAI, bu alanın en zor problemlerinden bazılarını çözdüğünü iddia eden 719 makale yayınladı. Hatta bilgisayar kontrolleri bile hata yapabilir. Yıllarca AI içeriği çöpü yaşadıktan sonra, matematiğin de etkilenen sonraki alan olup olmayacağı sorusu akla geliyor.
AxiomMath, hızı yavaşlatmak yerine daha sağlam bir temel oluşturarak bu kaderden kaçabilir. 1,6 milyar dolar değerindeki bu start-up, AI ajentlerinin yazılım yazmak ve nihayetinde bilimsel araştırmalar yapmak için güvenebileceği doğrulanmış bir temel katmanı inşa etmeyi hedefliyor.
Çarşambaları Kazanın Hafta XXX, şirket, insanlık tarafından yazılan en büyük matematiksel başarılarından biri olan Stacks Projesi'ni resmen doğruladığını duyurdu. Matematikçiler, Stacks'a genellikle çok yüksek puan verir. Columbia Üniversitesi matematikçisi Peter Woit, projeyi “karşılaştırılabilecek neredeyse hiçbir şey yok” olarak nitelendirmiş ve projeyi, 20. yüzyılda matematiği temelden yeniden kurmak amacıyla yazılan ünlü Bourbaki serisine benzetmişti.
Woit'in Kolombiyalı meslektaşı Johan de Jong, 2005 yılında Stacks Projesini bir açık kaynak referansı olarak başlattı. Bundan beri matematikçiler, üniversite düzeyi cebirden cebir, geometri ve sayılar teorisi alanlarındaki en önde gelen fikirlere kadar katkıda bulunmaya devam etmektedir.
Şirketin AI temsilci grubu, yaklaşık 7.654 sayfa olan bu veritabanını, bilgisayar tarafından kontrol edilebilir yaklaşık 16 milyon satır kodla çevirdi.
Formel matematiğin amacı, temel yapısının güvenilirliğini sağlamaktır. Matematikçiler, kanıtları Lean adlı bir programlama diliyle kodlara dönüştürür ve bu kodları bir proof assistant adlı programla satır satır kontrol ettirir. Kanıt başarıyla geçerse, matematikçiler bunun mantıksal olarak doğru olduğuna güvenebilirler.
Mühendisler de çip tasarımının uygunluğunu doğrulamak için aynı fikri, yani formel doğrulama yöntemini kullanır; Fransız araştırmacılar ise bunu aile yardım hesaplama yazılımında bir güvenlik açığı keşfetmek için kullanmışlardır.
Stacks Projesi gibi bir kaynak için teoremleri tek tek kontrol etmek işin bir parçasıdır. Stacks'teki teoremler ve tanımlar birbirine bağlıdır ve her biri öncekilerin üzerine kuruludur. Bir ağaç yapısı gibi, Stacks'taki birçok sonuç daha önceki sonuçlara kadar izlenebilir.
Bu bağımlılık, Axiom'un bu projenin mümkün olup olmadığını başlangıçta emin olamamasına neden oldu. Takım, yaklaşık 16 milyon satır Lean kodu içinde her bağlantının tamamen korunmasını sağlamalıydı.
Axiom CEO Carina Hong, TechCrunch'a şunu söyledi: "Boyut ve ince detay, gerçek dünyada genellikle uyumlu değildir. [Stacks], matematiksel temeli oluşturan bir dizi matematiksel sonuçtur. [Teoremler] birbirleriyle tutarlı olmasını, çelişkiler gibi görünmesini istersiniz. Ayrıca bu tanımlar arasında çatışma olmamasını da istersiniz."
25 yaşındaki CEO, Stanford Üniversitesi matematik doktora programından ayrıldı ve 2025 Mart ayında şirketi kurdu. Bu yıl Mart'ta, Axiom, Menlo Ventures'in öncülük ettiği sermaye artırma turundan 200 milyon dolar topladı.
Hong, "Vibe coding'in Stacks'in estetiğini koruyup korumayacağını o zamanlar emin değildik."
Bu projeyi tamamlamak için takım, ajanlara esnek bir yapı tanımladı ve onları paralel olarak çalıştırdı. Axiom teknik ekibi üyesi Ashvin Swaminathan, “Stacks için bir hiyerarşi oluşturduk… ancak bu, her ajanın tam olarak ne yapması gerektiğini tamamen belirleyen bir hiyerarşi değil. Ajanlar kendi kendilerine görevleri bulur ve paralel olarak işlenebilecek şeyleri tanımlar.”
Axiom, kendi modellerini matematikte yetenekli hale getirmek için eğitti. Hong, bu yaklaşımın diğer çoğu doğrulama temelli girişim tarafından benimsenmediğini söyledi. Başlangıçta, ekip, bu ajanların insan benzeri yargı kriterleri geliştirmesini sağlamak için dahili bir Lean uzmanına güvendi. Zamanla, Hong'a göre, bu ajanlar bu yargı yeteneğini kendi kendilerine öğrendi.
Bu başarı, formel matematikteki en büyük boşluklardan birini doldurdu. Swaminathan, “Zaten formelleştirilmiş matematik içeriklerine baktığınızda, dev bir kara delik olduğunu görürsünüz. Ve bu kara delik, cebirsel geometriyi kapsıyor.”
Swaminathan, şimdiye kadar Lean ile cebirsel geometriye dair yeni çalışmalarını kontrol etmek isteyen araştırmacıların neredeyse hiç hazır temele sahip olmadığını söyledi. "Şimdi bunlara sahipler."
Axiom, doğrulanmış her sonucun bir yapı taşı olduğunu ve gelecekteki kanıtların matematiği baştan başlamadan, zaten denetlenmiş olan üzerine kurulabileceğini düşünür. UCLA matematikçisi ve Fields Ödülü sahibi Terence Tao, bunu daha özlü bir şekilde şöyle özetler: "Ne kadar çok formel kanıta sahip olursanız, o kadar çok formel kanıt oluşturabilirsiniz."
Axiom'un hedef kitlesi sadece matematikçilerden oluşmuyor. Geliştiriciler uzun süredir kodlarının hatalar ve güvenlik açıkları içermemesini sağlamak için çaba harcıyor. AI temsilcilerinin yazılım yazma oranı arttıkça bu sorun daha da büyüyecek.
Axiom bahis, geleceğin yazılımları, Stacks gibi kanıtlanmış temeller üzerine kurulmalıdır.
Swaminathan, "Matematiğin, bunları oluşturmayı başlattığınız alan olduğunu ve bunun taşınabilir bir beceri olduğunu düşünüyoruz. Ajentler, kodumuzu okuyabilir, anlayabilir ve üzerine yeni altyapılar inşa edebilir. Lean ile yaptığımız formelleştirme, artık ajentlerin inşa edebileceği temel taban haline gelmiştir."
Axiom'un Stacks'i oluşturma şekli—paralel çalışmak, kendi görevlerini seçmek—Hong'un gelecekteki birçok AI işinin böyle olacağını beklediği şekildir. O, AI ajantlarının çöp içerik üretmemesi için iyi yapılandırılmış ve tekrar kullanılabilir bir bilgi tabanına ihtiyaç duyacağını düşünmektedir.
Hong, "Bir [ajansın] sürekli olarak yeniden kullanılabilir bir veritabanına sahip olmasını istersiniz ki, bu veritabanı üzerinde ilerleyebilsin ve öne çıksın. Eğer baştan kötü mühendislik seçimleriyle çöp doldurursanız, o zaman bu sınırı genişletmek çok zorlaşır."
Hong, bu yönteme büyük bir güvene sahip ve açıkça meydan okudu. "Bu ölçekteki formel çalışmayı yapmak için tüm programlama şirketlerine açıkça meydan okuyorum," dedi.