OpenAI’ın Astra’sı 10 Açık Matematik Probleminde İlerleme Sağladı: Maliyet Yaklaşık 2.000 Dolar

Astra hangi problemlere odaklandı?

Astra’nın ele aldığı başlıklar, matematiğin yanı sıra teorik bilgisayar biliminin farklı dallarını kapsıyor: yüksek boyutlu geometri, kodlama teorisi, aritmetik devre karmaşıklığı, grup teorisi, operatör cebirleri, kuantum karmaşıklığı, kafes kriptografisi ve ekstremal kombinatorik .

OpenAI’nin sıraladığı 10 sonuç şöyle:

1. Yüksek boyutlu küre paketleme: Küre paketleme yoğunluğu için Cohn–Elkies eşiğine kadar ulaşan yeni üst sınırlar .
2. İkili ve küresel kodlar: Belirli bir minimum mesafeye göre mümkün olan en büyük kod boyutu için üstel ölçekte iyileştirilmiş sınırlar .
3. Sofik olmayan gruplar: Grup teorisinin uzun süredir açık sorularından biri olan sofik olmayan grupların varlığını ortaya koyan açık bir inşa .
4. Connes’in rijitlik varsayımı: Von Neumann cebirleriyle ilgili uzun süredir kabul gören bir varsayımın çürütülmesi .
5. Aritmetik devre karmaşıklığı: Permanent hesaplamasına ilişkin yeni alt sınırlar; bunlar arasında n⁴/log n mertebesinde bir aritmetik-formül alt sınırı da bulunuyor .
6. Kuantum paralel tekrar: Genel iki oyunculu kuantum oyunları için üstel paralel tekrar teoremi .
7. En yakın vektör problemi: Kuantum sonrası kriptografinin temellerinden biri olan problemin yaklaşık çözümünün polinomik faktör açısından zor olduğuna dair sonuç .
8. Ehrhart’ın hacim varsayımı: Ağırlık merkezinin, içindeki tek kafes noktası olduğu bir dışbükey cismin alabileceği maksimum hacim .
9. Çok renkli Ramsey sayıları: Erdős’ün 183 numaralı problemini çözen, süper üstel bir alt sınır .
10. Ekstremal sayı varsayımları: Kompaktlık ve dejenerasyon varsayımlarına ilişkin sonuçlar; Erdős’ün 146 ve 180 numaralı problemlerinin çözümü .

“Lean ile doğrulama” neden önemli?

OpenAI, Astra modelini ya da kullanılan üretim sürecinin tamamını yayımlamadı. Bunun yerine, Apache 2.0 lisansı altında Lean 4 ispat sertifikalarını GitHub’da erişime sundu. Depodaki “sorry” sayısının sıfır olduğu bildirildi; bu da biçimsel hâle getirilen 10 ispatın her adımının Lean tarafından doğrulandığı anlamına geliyor .

Lean gibi biçimsel ispat sistemleri, matematiksel bir argümandaki her adımın makinenin anlayabileceği şekilde açıkça yazılmasını gerektirir. Böylece tartışma, “Yapay zekânın açıklaması doğru mu?” sorusundan, “Yayımlanan biçimsel ispat gerçekten bu sonucu mu kanıtlıyor?” sorusuna taşınır. Ancak bu yöntem, ispatın nasıl keşfedildiğini veya modelin hangi yönlendirmelerle çalıştırıldığını tek başına açıklamaz.

Matematik dünyasının tepkisi: Etkileyici ama temkinli

Noam Brown gibi bazı araştırmacılar duyuruyu bilimsel akıl yürütme açısından önemli bir adım olarak değerlendirdi . Buna karşın, eleştiriler de birkaç başlıkta yoğunlaştı.

Bunlar Milenyum Problemleri değil

Gözlemciler, söz konusu 10 problemin Clay Matematik Enstitüsü’nün Milenyum Ödülü Problemleri arasında yer almadığına dikkat çekti. P ile NP arasındaki ilişki veya Riemann hipotezi gibi kamuoyunda çok daha bilinen soruların çözülmemiş olması, duyurunun “matematik çözüldü” şeklinde yorumlanmasını sınırlıyor .

Yine de bu durum problemlerin önemsiz olduğu anlamına gelmiyor. Örneğin sofik olmayan grupların açık biçimde inşa edilmesi sorusu, Mikhail Gromov’un sofik kavramını 1999’da ortaya koymasından bu yana açık durumdaydı .

Bağımsız hakem değerlendirmesi yok

Sonuçlar, bir matematik dergisinde veya konferans bildiri kitabında hakem değerlendirmesinden geçmeden doğrudan OpenAI tarafından duyuruldu . Eleştirmenler, yapay zekânın keşfiyle insanların sonucu çerçevelemesi arasındaki sınırın belirsiz kaldığını savunuyor. OpenAI’nin de yapay zekâ ve matematikte yazarlık tartışmalarına değinerek Leiden Bildirgesi’ne atıfta bulunması bu gerilimi gösteriyor .

Matematikteki başarı başka alanlara taşınabilir mi?

Bilişsel bilimci Gary Marcus, biçimsel matematikteki başarının “özel bir durum” olabileceğini ve bunun daha geniş bilimsel akıl yürütmeye otomatik olarak genellenemeyeceğini savundu . Matematikte sonuçlar sembolik araçlarla görece ucuza ve kesin biçimde kontrol edilebiliyor. Bilimsel araştırmaların çoğunda ise gerçek dünya verileri, belirsizlik ve tekrarlanabilirlik sorunları aynı şekilde kolayca yönetilemiyor.

Astra’nın üretim süreci tekrarlanamıyor

Model henüz yayımlanmadığı ve kullanılan özgül yönlendirme yöntemi ayrıntılı biçimde açıklanmadığı için, bağımsız araştırmacıların aynı üretim sürecini baştan sona tekrarlaması mümkün değil . Lean sertifikaları ispatların kontrol edilmesini sağlasa da Astra’nın bu sonuçlara hangi adımlarla ulaştığı sorusu açık kalıyor.

Duyurunun zamanlaması tartışılıyor

Astra, OpenAI’nin bir sonraki büyük model ailesi olarak konumlandırılıyor. Bu nedenle bazı eleştirmenler, araştırmanın bilimsel değerlendirmeden önce ve model tanıtım süreciyle aynı dönemde duyurulmasının pazarlama etkisini artırmaya yönelik olabileceğini öne sürdü .

Sonuç: Büyük bir iddia, fakat nihai hüküm için erken

OpenAI’nin yayımladığı kanıtlar, sıradan bir kurumsal tanıtım açıklamasından daha ayrıntılı ve incelenebilir bir tablo sunuyor . Eğer uzmanların incelemesinden sonra ispatların geçerli olduğu doğrulanırsa, bazı sonuçlar onlarca yıldır açık kalan soruları kapatabilir. Sofik olmayan bir grubun ilk açık inşası iddiası, 25 yılı aşkın süredir bekleyen bir soruya yanıt vermesi açısından özellikle dikkat çekiyor .

Ancak şu aşamada Astra’nın matematikte “insanüstü” veya genel anlamda bilimsel araştırmacı olduğunu söylemek için yeterli kanıt yok. Asıl sınav, biçimsel olarak doğrulanabilen bu sonuçların bağımsız uzman incelemesinden geçmesi ve benzer bir akıl yürütme kapasitesinin matematiğin dışındaki, doğrulanması daha zor bilimsel alanlarda da gösterilebilmesi olacak.