OpenAI’den matematik dünyasını sarsan hamle: 10 yıllık 10 problem çözüldü

OpenAI, henüz genel kullanıma sunulmayan yeni nesil modeli Astra ile matematik dünyasında dikkat çeken bir başarıya imza attığını açıkladı. Şirket, modelin matematik ve teorik bilgisayar bilimi alanlarında en az 10 yıldır açık olan 10 problem için yeni sonuçlar ürettiğini duyurdu. Çalışmaların tamamı 249 sayfalık bir makale ve bilgisayar tarafından kontrol edilebilen Lean 4 kanıtlarıyla birlikte yayımlandı.

OpenAI’nin paylaştığı sonuçlar; yüksek boyutlu geometri, kodlama teorisi, grup teorisi, kuantum karmaşıklığı, kafes kriptografisi ve kombinatorik gibi farklı alanlara uzanıyor. Şirketin açıklamasına göre Astra’nın ürettiği sonuçlar arasında uzun yıllardır çözülemeyen bazı önemli soruların çözümü ve bazı problemlerde bilinen sınırların geliştirilmesi bulunuyor.

YILLARDIR AÇIK KALAN PROBLEMLERDE YENİ SONUÇLAR

Astra’nın dikkat çeken çalışmalarından biri, sofic olmayan grupların varlığını ortaya koyan açık bir yapı oluşturması oldu. Bu soru, Mikhail Gromov’un sofic gruplar kavramını ortaya koymasından bu yana uzun yıllardır matematikçilerin üzerinde çalıştığı problemler arasında yer alıyordu. 

Model ayrıca Connes'in rijitlik varsayımını çürüten bir sonuç ortaya koyarken, Paul Erdős’ün problem kataloğundaki bazı sorulara da çözüm getirdi. Yüksek boyutlu küre paketleme konusunda ise 1978’den bu yana genel üst sınırdaki ilk önemli ilerlemelerden biri elde edildiği bildirildi. 

Burada önemli bir ayrım bulunuyor: OpenAI’nin açıkladığı 10 sonucun tamamı aynı anlamda “çözülmüş problem” niteliğinde değil. Bazıları açık bir varsayımı çözerken bazıları bilinen sınırları geliştiriyor. Bu nedenle çalışmanın etkisi, tek bir matematiksel keşiften ziyade farklı alanlarda elde edilen yeni sonuçların toplamı olarak değerlendiriliyor.

LEAN 4 KANITLARIYLA BİLGİSAYARDA KONTROL EDİLEBİLİYOR

OpenAI’nin duyurusunu önceki yapay zeka destekli matematik iddialarından ayıran en önemli noktalardan biri, sonuçlara ilişkin Lean 4 kanıtlarının da yayımlanması oldu. Lean, matematiksel ispatların bilgisayar tarafından biçimsel olarak kontrol edilmesine imkan veren bir doğrulama sistemi.

Şirket, 10 sonucun her biri için makine tarafından kontrol edilebilen kanıt dosyalarını kamuoyuna açtı. Böylece araştırmacılar, Astra’nın ürettiği matematiksel argümanların biçimsel olarak doğrulanıp doğrulanamadığını bağımsız şekilde kontrol edebiliyor. 

Ancak Lean tarafından doğrulanmış olması, çalışmanın otomatik olarak akademik hakem değerlendirmesinden geçtiği anlamına gelmiyor. Bir kanıtın biçimsel olarak tutarlı olması, kullanılan matematiksel ifadenin ilgili problemi doğru şekilde temsil edip etmediği veya sonucun bilimsel öneminin ne olduğu gibi soruları tek başına yanıtlamıyor. 

10 MATEMATİKSEL SONUCUN MALİYETİ NE KADAR?

OpenAI, bu çalışmaların ortaya çıkarılması için gereken toplam token miktarının Sol API fiyatları üzerinden yaklaşık 2 bin dolara karşılık geleceğini açıkladı. Ancak bu rakamın Astra’nın geliştirilmesi veya eğitilmesinin toplam maliyeti olmadığı özellikle belirtilmeli. Söz konusu hesaplama yalnızca sonuçların bulunması sırasında kullanılan hesaplama miktarının farklı bir API fiyatlandırması üzerinden yapılan karşılığı. 

Ayrıca Astra henüz kamuya açık bir model değil. Dolayısıyla kullanıcıların bugün Astra’yı çalıştırarak aynı sonuçları üretmesi mümkün değil. OpenAI, modelin uzun soluklu araştırma görevlerini yerine getirebilecek yeni nesil bir sistem olarak geliştirildiğini belirtiyor.

Bu gelişme, yapay zekanın yalnızca mevcut bilgileri özetleyen bir araç olmaktan çıkıp yeni matematiksel sonuçların ortaya çıkarılmasında kullanılabileceğine dair dikkat çekici bir örnek oluşturuyor. Bununla birlikte elde edilen sonuçların akademik topluluk tarafından daha kapsamlı biçimde incelenmesi, Astra’nın matematiksel araştırmalardaki gerçek kapasitesinin anlaşılması açısından önem taşıyor.