Yapay zeka haftada yeni bir matematik problemi çözüyor gibi görünüyor. Geçen ay OpenAI, alanın en zorlu problemlerine getirilen çözümlerle ilgili 719 makale yayımladı. Bilgisayar kontrollerinde bile hatalar olabilir. Yıllarca süren yapay zeka 'çöpünden' sonra matematiğin de aynı kaderi paylaşıp paylaşmayacağını merak etmek doğaldır. AxiomMath, matematiğin bu sondan kaçınabileceğine inanıyor. Şirket, yapay zeka ajanlarının yazılım yazmak ve nihayetinde bilim yapmak için güvenebileceği doğrulanmış bir temel oluşturmak istiyor. Çarşamba günü şirket, insanlar tarafından yazılmış en büyük matematik külliyatlarından biri olan Stacks Project'i resmi olarak doğruladığını duyurdu.
Matematikçilerin gözdesi Stacks Project doğrulandı
Matematikçiler Stacks'e büyük değer veriyor. Columbia Üniversitesi'nden matematikçi Peter Woit, projenin 20. yüzyılda matematiği temelinden yeniden inşa eden ünlü Bourbaki kitaplarına benzediğini ve “başka hiçbir şeye benzemediğini” belirtmişti. Woit'in meslektaşı Johan de Jong, Stacks Project'i 2005 yılında açık kaynaklı bir referans olarak başlattı. O zamandan beri matematikçiler, üniversite düzeyindeki cebirden geometri ve sayılar teorisindeki en ileri düzey fikirlere kadar uzanan sonuçları geliştirerek projeye katkıda bulundular. Şirketin yapay zeka ajanları, yaklaşık 7.654 sayfalık kütüphaneyi yaklaşık 16 milyon satırlık bilgisayar tarafından kontrol edilen koda çeviriyor. Matematiği biçimlendirmek, altındaki yapının sağlam olduğundan emin olmanın bir yoludur. Matematikçiler, ispatları Lean adlı bir programlama dilinde kod olarak yeniden yazar ve bir ispat yardımcısı programı satır satır kontrol eder. İspat geçerse, matematikçiler mantıksal olarak sağlam olduğuna güvenebilirler. Mühendisler, tasarımlarının çalıştığını doğrulamak için aynı fikri, yani biçimsel doğrulamayı kullanır. Fransa'daki araştırmacılar ise aile yardımlarını hesaplayan yazılımlardaki hataları yakalamak için bu yöntemi kullanmışlardır.
Axiom CEO'su Hong: “Tutarlılık önemli”
Stacks Project gibi bir kütüphane için her teoremi kontrol etmek işin sadece bir parçasıdır. Stacks'teki teoremler ve tanımlar birbiriyle bağlantılıdır ve her biri öncekilere dayanır. Bir aile ağacı gibi, Stacks'teki birçok sonuç öncekilere dayanır. Bu bağlantı, Axiom'u projenin ilk başta işe yarayıp yaramayacağı konusunda emin olmamaya itti. Ekip, yaklaşık 16 milyon satır Lean kodu boyunca her bağlantıyı sağlam tutmak zorunda kaldı. Axiom CEO'su Carina Hong, “Hayattaki büyük ve hassas şeyler bir araya gelmez,” dedi. “Stacks, matematiğin temeli olan matematiksel sonuçların bir koleksiyonudur. Teoremlerin tutarlı olmasını ve çelişkili olmamasını istersiniz. Tanımların birbiriyle çelişmemesini istersiniz.” 25 yaşındaki CEO, Stanford'da matematik doktorasını bırakıp Mart 2025'te şirketi kurdu. Mart ayında Axiom, Menlo Ventures liderliğinde 200 milyon dolarlık Seri A yatırımı aldı. Hong, “Vibe kodlamanın Stacks'in güzelliğini koruyup koruyamayacağından emin değildik,” dedi. Projeyi başarmak için ekip, ajanlarına gevşek bir yapı verdi ve paralel çalışmalarına izin verdi. Axiom'un teknik personelinden Ashvin Swaminathan, “Stacks ile bir hiyerarşi uyguladık… ancak bu, her ajanın ne yaptığını dikte eden tam bir hiyerarşi değildi,” dedi. “Ajanlar kendileri için görevler buluyor ve paralel olarak üzerinde çalışabilecekleri şeyleri belirliyordu.” Axiom ayrıca kendi modellerini matematik konusunda iyi olacak şekilde eğitti, ki bu yaklaşım Hong'a göre diğer doğrulama girişimlerinin çoğu tarafından benimsenmemiştir. Başlangıçta ekip, ajanlara insan tadı kazandırmak için bünyesindeki Lean uzmanlarından birine güvendi. Hong, zamanla ajanların kendi başlarına tat geliştirdiğini söyledi. Sonuç, biçimlendirilmiş matematikteki en büyük boşluklardan birini dolduruyor. Swaminathan, “Matematikte biçimlendirilene baktığınızda, bu devasa bir kara delik var. Ve bu kara delik cebirsel geometriyi kapsıyor,” dedi. Swaminathan'a göre şimdiye kadar cebirsel geometride yeni çalışmaları Lean ile kontrol etmek isteyen araştırmacıların üzerinde inşa edebilecekleri çok az şey vardı. “Artık var.” Axiom, doğrulanmış her sonucun bir yapı taşı haline geldiğini, böylece gelecekteki ispatların sıfırdan başlamak yerine kontrol edilmiş matematiğe dayanabileceğini savunuyor. UCLA'dan matematikçi ve Fields Madalyası sahibi Terence Tao, genel durumu daha basit bir şekilde ifade ediyor: “Ne kadar biçimsel ispatınız olursa, o kadar çok biçimsel ispat yapabilirsiniz.” Matematikçiler Axiom'un tek hedef kitlesi değil. Geliştiriciler uzun zamandır kodlarının hata ve güvenlik açıklarından arınmış olmasını garanti etmekte zorlanıyor. Yapay zeka ajanları dünyanın kodunun daha fazlasını yazdıkça bu sorun büyüyor. Axiom, geleceğin yazılımlarının, Stacks'in şu anda yaptığı gibi, doğrulanmış temeller üzerine inşa edilmesi gerekeceğine inanıyor. Swaminathan, “Matematiğin bu şeyleri inşa etmeye başladığınız alan olduğuna ve bunun aktarılabilir bir beceri olduğuna inanıyoruz,” dedi. “Ajanlar kodumuzu okuyabilir, anlayabilir ve üzerine yeni altyapı inşa edebilir. Lean biçimlendirmemiz artık ajanların üzerine inşa edebileceği alt tabakadır.” Axiom'un ajanlarının paralel çalışarak ve kendi görevlerini seçerek Stacks'i inşa etme şekli, Hong'un yapay zekanın gelecekteki çalışmalarının çoğunun nasıl gerçekleşeceğini beklediği şekildir. Hong, yapay zeka ajanlarının çöp üretmekten kaçınmak için iyi inşa edilmiş, yeniden kullanılabilir bir bilgi birikimine ihtiyaç duyacağını savunuyor. Hong, “Ajanların üzerine inşa edebilecekleri ve sınırı zorlamaya devam edebilecekleri yeniden kullanılabilir bir kütüphaneye sahip olmalarını istersiniz,” dedi. “Başlangıçta kötü mühendislik seçimleri yaparak çöp bırakırsanız, o sınırı büyütmeleri çok zor olur.” Hong, bu yaklaşımdan o kadar emin ki bir meydan okuma yapıyor. Hong, “Tüm kodlama şirketlerini bu ölçekte biçimlendirme üzerinde çalışmaya açıkça davet ediyorum.”
