Axiom Math, matematikte AI slop'a karşı Stacks Project'i doğruladı

Axiom'un ajanları yaklaşık 7.654 sayfayı, Lean dilinde yazılmış yaklaşık 16 milyon satır bilgisayar denetimli koda çevirdi. Bir kanıt Lean'e aktarılıyor, bir kanıt asistanı kodu satır satır denetliyor; test geçilirse kanıtın mantıksal olarak sağlam olduğuna güvenilebiliyor. Zorluk, Stacks'teki teorem ve tanımların birbirine bağlı olmasıydı: tüm bağlantıların korunması gerekiyordu. CEO Carina Hong, büyük ve hassas şeylerin genellikle bir arada olmadığını söyledi.

Paralel çalışan ajanlar

Ekip ajanlara gevşek bir hiyerarşi verip paralel çalışmalarına izin verdi. Teknik ekipten Ashvin Swaminathan'a göre ajanlar kendi görevlerini kendileri buldu. Axiom ayrıca matematikte iyi olacak kendi modellerini de eğitiyor; Hong'a göre doğrulama alanındaki çoğu girişim bunu yapmıyor.

Sonuç, biçimselleştirilmiş matematikteki en büyük boşluklardan birini, cebirsel geometriyi dolduruyor. Swaminathan, Lean ile yeni çalışmaları denetlemek isteyen araştırmacıların artık dayanabilecekleri bir tabana sahip olduğunu belirtiyor.

Neden önemli

Axiom'a göre doğrulanmış her sonuç sonraki kanıtlar için yapı taşı oluyor. Terence Tao'nun sözleriyle, ne kadar çok biçimselleştirilmiş kanıt varsa, o kadar çoğunu üretmek mümkün. Hedef kitle yalnızca matematikçiler değil: yazılımcılar da kodlarının hatasız ve güvenlik açıksız olduğunu garanti etmekte zorlanıyor ve AI daha fazla kod yazdıkça sorun büyüyor.

Hong, ajanların “slop” üretmemesi için yeniden kullanılabilir bir bilgi birikimine ihtiyaç duyacağını savunuyor ve kodlama şirketlerine bu ölçekte biçimselleştirme yapmaları için meydan okuyor. Axiom Mart 2025'te kuruldu ve bu yıl Mart'ta Menlo Ventures liderliğinde 200 milyon dolarlık Seri A yatırımı aldı.