Axiom Math, Matematik Alanına Yapay Zekâ Kaynaklı İçerikleri Sınırlandırmayı Hedefliyor.

Yapay zekânın her hafta yeni bir matematik problemi çözüyormuş gibi görünmesi alışıldık bir hal aldı. Geçen ay yalnızca OpenAI, alanın en zor problemlerinin çözümlerini iddia eden 719 makale yayınladı. Bilgisayar kontrolleri bile hata yapabiliyor. Yıllardır süren yapay zekâ üretileri sonrasında, matematikin sıradaki hedef olabileceği şüphesiz akla geliyor.

AxiomMath, matematigin bu kaderi atlatabileceğine inanıyor; bunu yavaşlayarak değil, daha sağlam bir temele oturarak başarmaya çalışarak. 1,6 milyar dolar değerlemeli startup, yapay zekâ ajanlarının yazılım yazmak için güvenebileceği ve nihayetinde bilim yapabileceği doğrulanmış bir temel inşa etmek istiyor.

Woit’un Columbia’daki meslektaşı Johan de Jong, 2005 yılında Stacks Project’i açık kaynaklı bir referans olarak başlattı. Matematisyenler o günden beri bu projeye katkıda bulunuyor; lisans düzeyinde cebirden, cebir, geometri ve sayı teorisinde alanın en gelişmiş fikirlerine kadar sonuçlar inşa ediyorlar.

Şirketin yapay zekâ ajanları filosu, kütüphanenin yaklaşık 7.654 sayfasını bilgisayar tarafından kontrol edilen yaklaşık 16 milyon satır koda çeviriyor.

Matematiksel formalizasyon, altındaki yapının sağlam olduğunu güvence altına alma yöntemidir. Matematisyenler ispatı Lean denilen bir programlama dilinde kod olarak yeniden yazar ve proof assistant denilen bir program kodu satır satır kontrol eder. İspat geçerliyse, matematisyenler onun mantıksal olarak sağlam olduğuna güvenebilir.

Mühendisler aynı fikri, formal verification (formal doğrulama) olarak bilinen yaklaşımı, çip tasarımlarının doğru çalıştığını teyit etmek için kullanırken; Fransa’daki araştırmacılar bu yöntemi aile yardımlarını hesaplayan yazılımdaki hataları yakalamak için kullandı.

Açık kaynaklı yapay zekâ patlama yapıyor. Hugging Face kimin kazandığını açıklıyor. | Equity Podcast

Stacks Project gibi bir kütüphanede her teoremi kontrol etmek işin yalnızca bir parçasıdır. Stacks’taki teoremler ve tanımlar birbirine bağlıdır ve her biri kendinden öncekilerin üzerine inşa edilir. Bir aile ağacı gibi, Stacks’taki birçok sonuç kendinden öncekilere dayanır.

Bu birbirine bağlılık, AxiomMath’in projenin başta çalışıp çalışmayacağı konusunda belirsizliğe düşmesine yol açtı. Ekibin, yaklaşık 16 milyon satır Lean kodu boyunca her bağlantının bütünlüğünü koruması gerekiyordu.

“Hayatta hem büyük hem de narin şeyler bir araya gelmez,” Axiom CEO’si Carina Hong TechCrunch’a söyledi. “Stacks, matematiğin temeli olan matematiksel sonuçlardan oluşan bir koleksiyondur. Teoremlerin tutarlı ve paradoksal olmayan, tanımların birbirleriyle çışmamasını istersiniz.”

25 yaşındaki CEO, Stanford’daki matematik doktora programından ayrıldı ve şirketi Mart 2025’te kurdu. Mart ayında Axiom, Menlo Ventures önderliğinde 200 milyon dolarlık Seri A fon topladı.

“Vibe coding’in (ruh kodlaması) Stacks’ın güzelliğini koruyabileceğinden emin değildik,” Hong söyledi.

Projeyi başarıyla hayata geçirmek için ekip, ajanlarına gevşek bir yapı verdi ve paralel çalışmaları için serbest bıraktı. “Stacks ile bir hiyerarşi dayattık… [ancak] bu, her bir ajanın ne yaptığını dikte eden kapsamlı bir hiyerarşi değildi,” Axiom’un teknik ekibinden Ashvin Swaminathan söyledi. “Ajanlar kendi görevlerini buluyor ve paralel çalışabilecekleri konuları tespit ediyordu.”

Axiom aynı zamanda kendi modellerini matematikte başarılı olacak şekilde eğitti; bu yaklaşımın Hong’a göre diğer doğrulama girişimlerinin çoğunun benimsemediği bir yaklaşım olduğunu belirtti. İlk başlarda ekip, ajanlara insan zevkini öğretmesi için kendi ev içi Lean uzmanlarından birine güvendi. Zamanla, Hong’a göre ajanlar zevkini kendi kendine edinmeye başladı.

Sonuç, formalize edilmiş matematikteki en büyük açıklardan birini dolduruyor. “Matematikte neyin formalize edildiğine baktığınızda, kocaman bir kara delik görürsünüz. Bu kara delik cebirsel geometriyi kapsıyor,” Swaminathan söyledi.

Şimdiye kadar cebirsel geometrideki yeni çalışmaları Lean ile kontrol etmek isteyen araştırmacılar, dayanacak pek bir şey bulamıyordu; Swaminathan söyledi. “Evet, artık bulabilirler.”

Axiom, her doğrulanmış sonucun bir yapı taşı haline geldiğini, böylece gelecekteki kanıtlar sıfırdan başlamak yerine kontrol edilmiş matematiğe dayanabileceğini savunuyor. UCLA matematikçisi ve Fields Madalyası sahibi Terence Tao, genel durumu daha basit ifade etti: “Ne kadar çok formalize edilmiş kanıtınız varsa, o kadar çok formalize edilmiş kanıt yapabilirsiniz.”

Matematikçiler, Axiom’un hedeflediği tek kitle değil. Geliştiriciler uzun süredir kodlarının hâli hazırda hatalardan ve güvenlik açıklarından arındırıldığından emin olmaya çalışıyor. Bu sorun, dünyadaki kodların giderek daha fazlasını yapay zekâ ajanlarının yazmasıyla birlikte büyüyor.

Axiom, geleceğin yazılımlarının, Stacks’in şu an yaptığı gibi, doğrulanmış temeller üzerine kurulu olması gerektiğine dair bir iddiada bulunuyor.

“Matematik, bu şeyleri inşa etmeye başladığınız alan ve bunun aktarılabilir bir beceri olduğuna inanıyoruz” diyen Swaminathan, “Ajanlar kodumuzu okuyabilir, anlayabilir ve üzerine yeni altyapı kurabilir. Lean ile biçimlendirme çalışmalarımız, ajanların inşa edebileceği tabakaya dönüştü.”

Axiom’un ajanlarının Stacks’i inşa ederken paralel çalışması ve kendi görevlerini seçmesi, Hong’un yapay zekânın geleceğindeki çalışmaların büyük kısmının böyle gerçekleşeceğine inandığı yaklaşım. Yapay zekâ ajanlarının, ‘slop’ denilen kalitesiz çıktıları üretmemek için iyi inşa edilmiş, yeniden kullanılabilir bir bilgi birikimine ihtiyaçları olacağını savunuyor.

Hong, bu yaklaşım konusunda yeterince emin olduğu için bir meydan okuma yayımlıyor: “Tüm kodlama şirketlerini, bu ölçekte biçimlendirme çalışmalarına odaklanmaya açıkça meydan okuyorum.”