OpenAI, henüz kamuya açılmayan yeni model ailesi Astra’nın matematik ve teorik bilgisayar biliminin farklı alanlarında uzun süredir çözüm bekleyen 10 problem için yeni sonuçlar ürettiğini duyurdu.
Forbes yazarı Jon Markman’ın aktardığına göre sonuçlar; grup teorisi, yüksek boyutlu geometri, kodlama teorisi, kuantum karmaşıklığı, kafes tabanlı kriptografi ve ekstremal kombinatorik gibi farklı çalışma alanlarını kapsıyor.
OpenAI, 1 Ağustos’ta yayımladığı 249 sayfalık makale derlemesinde ele alınan problemlerin her birinin en az 10 yıldır açık olduğunu, bazılarında ise onlarca yıldır ilerleme sağlanamadığını belirtti.
Sofik olmayan gruplardan küre paketlemeye
Astra’nın ürettiği sonuçlar arasında, matematikçilerin uzun yıllardır üzerinde çalıştığı “sofik olmayan grupların” varlığına ilişkin açık bir yapı oluşturulması yer aldı. Sofik gruplar, grup teorisinde karmaşık yapıların sonlu ve daha anlaşılır yapılar aracılığıyla yaklaşık olarak temsil edilmesine dayanıyor. Sofik olmayan bir grubun açık biçimde inşa edilmesi ise alanın uzun süredir yanıt aranan temel problemlerinden biri olarak kabul ediliyor.
Modelin ayrıca von Neumann cebirleri teorisindeki Connes katılık varsayımına karşı bir sonuç ürettiği bildirildi.
Astra’nın çalışmaları arasında yüksek boyutlarda küre paketleme yoğunluğunun üst sınırını geliştiren yeni bir sonuç da bulunuyor. Küre paketleme problemi, belirli bir alana birbiriyle çakışmayan eş büyüklükteki kürelerin mümkün olan en yoğun biçimde nasıl yerleştirilebileceğini araştırıyor. Forbes’a göre model, bu alanda 1978’den beri kullanılan genel üst sınırın geliştirilmesini sağladı.
Açıklanan sonuçlardan üçünün, Macar matematikçi Paul Erdős’ün geride bıraktığı açık problemler kataloğundan geldiği belirtildi. Diğer çalışmaların ikili ve küresel kodlar, kuantum hesaplama ve kafes tabanlı kriptografi gibi alanlara uzandığı aktarıldı.
Mayısta 80 yıllık varsayımı çürütmüştü
Astra ailesinin matematik alanındaki çalışmaları ilk kez ağustosta gündeme gelmedi. Aynı model ailesinin bir üyesi, mayıs ayında ayrık geometrinin yaklaşık 80 yıldır açık olan “birim uzaklık” problemine ilişkin yaygın bir varsayımı çürüten karşı örnek üretmişti.
Paul Erdős tarafından 1946’da ortaya atılan problem, bir düzlem üzerine yerleştirilen belirli sayıdaki nokta arasında tam olarak bir birim uzaklık bulunan kaç çift oluşturulabileceğini inceliyordu. Matematikçiler uzun süre kare ızgaraya dayanan yapıların en iyi sonucu verdiğini düşünüyordu.
OpenAI modeli ise bu yapıların en iyi seçenek olmadığını gösteren ve daha fazla birim uzaklık çifti oluşturan sonsuz bir örnek ailesi üretti.
Forbes’un haberine göre Fields Madalyası sahibi matematikçi Tim Gowers, kanıtı tereddüt etmeden önde gelen bir matematik dergisinde yayımlanmak üzere önerebileceğini söyledi. Aralarında Gowers ile Noga Alon’un da bulunduğu dokuz matematikçi daha sonra modelin ortaya koyduğu kanıtı insanlar tarafından daha kolay takip edilebilecek biçimde açıklayan ayrı bir çalışma yayımladı.
Erdős problemleri kataloğunu yöneten matematikçi Thomas Bloom ise ağustosta açıklanan 10 yeni sonucu “büyük haber” olarak nitelendirerek bunların birim uzaklık problemindeki önceki çalışmadan daha önemli olduğunu belirtti.
OpenAI araştırmacısı Noam Brown, sonuçların önemine karşın Astra’nın henüz matematiğin en büyük problemleri arasında gösterilen “Milenyum Problemleri”nden herhangi birini çözemediğini ifade etti.
Kanıtlar bilgisayar tarafından kontrol edilebiliyor
Astra’nın ürettiği sonuçları önceki yapay zeka başarı iddialarından ayıran en önemli unsur, çözümlerin makine tarafından denetlenebilen kanıtlarla birlikte yayımlanması oldu.
OpenAI, her sonuç için Lean adlı kanıt denetleme sisteminde hazırlanmış bir sertifika oluşturdu. Sertifika dosyaları açık lisansla GitHub üzerinden erişime açıldı.
Lean, bir matematiksel kanıtın bütün adımlarını tek tek kontrol ediyor. Bir çıkarımın daha önce tanımlanan kurallardan ve önermelerden mantıksal olarak türememesi halinde sistem kanıtı kabul etmiyor. Böylece sonuçların değerlendirilmesi yalnızca OpenAI’ın açıklamasına veya bir dil modelinin ikna edici görünen anlatımına dayanmıyor.
Dosyaları indiren bağımsız araştırmacılar, Lean denetleyicisini çalıştırarak sunulan biçimsel kanıtların geçerli olup olmadığını kontrol edebiliyor.
Geleneksel yöntemde önemli bir matematiksel kanıtın hakem değerlendirmesinden geçmesi aylar, bazı durumlarda yıllar sürebiliyor. Lean sertifikaları ise biçimsel hale getirilmiş kanıtın mantıksal tutarlılığının kısa sürede denetlenmesine olanak tanıyor.
Bununla birlikte Lean’in kanıtı kabul etmesi, çalışmanın matematiksel öneminin, özgünlüğünün veya mevcut literatürle ilişkisinin bütünüyle değerlendirildiği anlamına gelmiyor. Bu konular için alan uzmanlarının incelemesine ihtiyaç devam ediyor.
“2 bin dolar” hesabı neyi kapsıyor?
OpenAI, 10 problemin çözümünde kullanılan toplam token miktarının Sol API fiyatları üzerinden yaklaşık 2 bin dolara karşılık geldiğini açıkladı.
Ancak Forbes’un da dikkat çektiği üzere bu rakam, Astra’nın geliştirilme ve eğitilme maliyetini göstermiyor. Hesaplamaya modelin geliştirilmesi için kullanılan altyapı, araştırmacıların çalışmaları ve problemler belirlenmeden önce yapılan yatırımlar dahil değil.
Ayrıca OpenAI’ın yayımlamak üzere seçmediği problemler üzerinde kaç deneme yaptığı ve başarısız girişimlerin toplam maliyeti bilinmiyor. Bu nedenle 2 bin dolar, 10 keşfin bütün araştırma maliyeti yerine başarılı çalışmalarda kullanılan tokenların tahmini API karşılığı olarak değerlendiriliyor.
Şirket çalışanlarının makalelerin hazırlanmasına ve matematiksel argümanların biçimsel kanıtlara dönüştürülmesine yardımcı olduğu da belirtiliyor. OpenAI, yeni matematiksel içeriğin Astra tarafından üretildiğini savunuyor.
Model bağımsız araştırmacıların kullanımına açık değil
Astra henüz kamuya veya bağımsız araştırmacılara sunulmadı. Bu nedenle OpenAI dışındaki uzmanlar aynı problemleri modele yeniden vererek sonuçları baştan üretme olanağına sahip değil.
Yayımlanan Lean sertifikaları mevcut kanıtların biçimsel doğruluğunun denetlenmesini sağlasa da modelin çalışma süreci bağımsız biçimde tekrarlanamıyor. Dolayısıyla sonuçlar kontrol edilebiliyor ancak Astra’nın aynı koşullarda aynı sonuçlara ulaşıp ulaşmayacağı henüz sınanamıyor.
Yapay zeka alanındaki çalışmalara eleştirel yaklaşımıyla tanınan Gary Marcus, açıklanan sonuçları etkileyici bulduğunu ancak OpenAI’ın duyurusunun kapsamının abartılmış olabileceğini söyledi. Bazı uzmanlar da 10 problemden birkaçının son derece önemli sonuçlar olarak kabul edilebileceğini, diğerlerinin ise uzun süredir kimsenin yoğun biçimde çalışmadığı ve mevcut yöntemlerle ulaşılabilecek problemler çıkabileceğini belirtiyor.
Yapay zeka çıktılarında doğrulama sorunu
Forbes, Astra’nın çalışmalarının öneminin yalnızca matematik problemlerini çözebilmesinden kaynaklanmadığına dikkat çekiyor. Yapay zeka sistemlerinin şirketlerde ve kritik sektörlerde kullanılmasının önündeki temel engellerden biri, ürettikleri sonuçların güvenilirliğinin geniş ölçekte kontrol edilememesi.
Bir uzman, yapay zekanın hazırladığı tek bir metni inceleyebilir ancak aynı yöntemle on binlerce çıktıyı kontrol etmek mümkün olmayabilir. İnsan denetiminin ölçeklenemediği alanlarda, otomatik doğrulama sistemleri yapay zekanın kullanımını daha güvenli hale getirebilir.
Çip tasarımı, donanım doğrulama, kriptografi ve güvenlik açısından kritik yazılımlar, üretilen sonuçların matematiksel veya otomatik yöntemlerle kontrol edilebildiği alanlar arasında yer alıyor.
Astra’nın Lean sertifikalarıyla birlikte yayımlanan matematiksel sonuçları, yapay zekanın yalnızca zor problemlere yanıt üretmekle kalmayıp ürettiği yanıtı bilgisayar tarafından denetlenebilir biçime dönüştürebildiğini gösteren dikkat çekici bir örnek oluşturuyor.
