Axiom Math, dev matematik kütüphanesi Stacks Project'i yapay zekâ ajanlarıyla Lean'de doğruladı

Son zamanlarda neredeyse her hafta “yapay zekâ şu matematik problemini çözdü” haberi okuyoruz. Ama bu çözümlerin ne kadarına güvenebiliriz? Değeri 1,6 milyar dolar olarak biçilen girişim Axiom Math, bu soruya hız kesmeden, sağlam bir zemin kurarak cevap vermeye çalışıyor.

Ne yaptılar?

Şirket, cebir, geometri ve sayılar teorisinde temel bir başvuru kaynağı olan Stacks Project'i formal olarak doğruladığını açıkladı. Columbia Üniversitesi'nden Johan de Jong'un 2005'te başlattığı bu açık kaynaklı kütüphane, yıllar içinde pek çok matematikçinin katkısıyla büyüdü. Axiom'un yapay zekâ ajanları yaklaşık 7.654 sayfayı Lean adlı programlama diline aktararak yaklaşık 16 milyon satırlık bir kod çıkardı. Bu kodu bir ispat asistanı satır satır kontrol ediyor; geçen ispatın mantıken sağlam olduğuna güvenilebiliyor.

Zor olan neydi?

Stacks'teki sonuçlar bir soy ağacı gibi birbirine bağlı; her teorem kendinden öncekilere dayanıyor. Ekip, bu bağların hiçbirini koparmadan çalışmak zorundaydı. Ajanlara sıkı bir hiyerarşi yerine gevşek bir yapı verilmiş, ajanlar paralel olarak kendi görevlerini kendileri bulmuş. Axiom ayrıca matematikte iyi olacak kendi modellerini eğitmiş. Ekipten Ashvin Swaminathan'a göre formalleştirilmiş matematikteki en büyük boşluk cebirsel geometriydi ve bu iş o boşluğu büyük ölçüde dolduruyor.

Neden önemli?

Bana en ilginç gelen kısım, hedefin sadece matematikçiler olmaması. Kodun giderek daha fazlasını yapay zekâ yazarken hatasız ve güvenli yazılım garanti etmek zorlaşıyor. Axiom, doğrulanmış bir bilgi temelinin bu “özensiz üretim” sorununa karşı bir panzehir olabileceğini savunuyor. CEO Carina Hong ise diğer kodlama şirketlerine bu ölçekte formalleştirme yapmaları için açıkça meydan okuyor.

Kaynak: TechCrunch