OpenAI 719 matematik makalesini birden yayınladı: Neyi kanıtladı, neyi henüz kimse kontrol etmedi?

Ne oldu?

OpenAI 6 Ekim’de, henüz yayınlanmamış bir iç modelinin ürettiği matematik sonuçlarını openai/math adlı herkese açık bir GitHub deposunda paylaştı. İlk sürümde 722 makale vardı. Ertesi gün üçü geri çekildi, bugün katalogda 372 sonuç ailesine ayrılmış 719 makale var. Bir “aile”, ana sonucu, ona dayanan yan sonuçları ve aynı şeyin farklı kanıtlarını bir araya topluyor. Yani 719 makale, 719 ayrı buluş demek değil.

Yöntem de açıklanmış: Model yaklaşık 4.000 açık probleme sokulmuş, her sonuç için ortalama ChatGPT Pro’da üç saatlik düşünmeye denk bir hesaplama harcanmış. Çıkan sonuçlar ailelere toplanıp belli bir önem eşiğini geçenler yayınlanmış. Riemann zeta fonksiyonu ve Hodge sanısıyla ilgili birkaç çalışma bu sabit yöntemin dışında kalmış, birinin yazımı da okunabilirlik için insan eliyle düzenlenmiş.

Two Minute Papers videosu, bu yayının “matematik yapmak” fikrini nasıl değiştirdiğini anlatıyor. Biz ayrıntıları deponun kendisinden kontrol ettik.

Listede neler var?

Depodaki özetlere göre öne çıkan birkaç başlık:

• Unique Games sanısı. Bilgisayar biliminde, bazı problemleri yaklaşık olarak bile çözmenin ne kadar zor olduğunu belirleyen ünlü bir varsayım. Doğruysa, Max-Cut gibi problemlerde bilinen en iyi yaklaşık algoritmaların aslında aşılamaz olduğu anlamına geliyor. Depo bunu kanıtladığını söylüyor.
• Matris çarpımı. İki n×n matrisi çarpmanın maliyetini belirleyen üs için bilinen en iyi sınır yaklaşık 2,371’di. Makale bunu 2,25’e (9/4) indirdiğini iddia ediyor. Bu teorik bir sınır; yarın ekran kartlarının hızlanacağı anlamına gelmiyor.
• Riemann zeta fonksiyonu. Ünlü Riemann hipotezi değil, daha zayıf bir hâli: Fonksiyonun gerçel kısmı 7/8’den büyük bölgede hiç sıfırı olmadığı.
• π sayısı. π’nin kesirlerle ne kadar iyi yaklaşılabildiğini ölçen “irrasyonellik üssünün” tam olarak 2 olduğu.

Bu dört başlığın hepsinde depo bir Lean kanıtına bağlantı veriyor. Ama listedeki her sonuç için bu geçerli değil.

Yüzde 42 kontrol edilmiş, yüzde 58 bekliyor

Lean, kanıtı kod gibi yazıp her adımını bilgisayara kontrol ettiren bir dil. Nasıl çalıştığını yapay zekâ ve matematik yazımızda anlatmıştık. OpenAI’ın kendi sayısına göre ana sonuçların 300 / 719’u, yani yaklaşık yüzde 42’si Lean ile biçimselleştirilmiş. Geri kalan yüzde 58 için şimdilik elde yalnızca makalenin kendisi var.

Lean kanıtlarını kontrol etmek için depo, Lean ekibinin Comparator aracını öneriyor. Comparator, güvendiğin bir “problem tanımı” dosyasıyla modelin “çözüm” dosyasını karşılaştırıyor. Teoremin ifadesinin birebir aynı olduğuna, kanıtın yalnızca izin verilen aksiyomları kullandığına bakıyor ve her şeyi Lean çekirdeğinde yeniden çalıştırıyor. Yazılımcı gözüyle: Testi modelin yazdığı kopyaya değil, senin elindeki asıl teste karşı koşturmak gibi. Yine de bir sınırı var: Problem tanımı yanlış yazıldıysa, doğru ama yanlış soruya ait bir kanıt onaylanır.

Bunun neden önemli olduğu ilk gün görüldü. 7 Ekim’de OpenAI, Lean kanıtı olmayan bir makalede işaret hatası bulduğunu ve buna dayanan iki makaleyle birlikte üç makaleyi geri çektiğini duyurdu. 14 makale daha düzeltildi. Eski sürümler silinmiyor, geri çekilen makaleler bir açıklama notuyla duruyor. Kısacası depo, bir yazılım projesi gibi sürüm geçmişiyle yönetiliyor.

Matematikçiler ne diyor?

OpenAI, yayını Princeton’daki Institute for Advanced Study’de toplanan bağımsız bir danışma grubuna (AGMAI) danışarak hazırladığını söylüyor. Grup aynı gün yaptığı açıklamada, danışmanlık rolünün sonuçların değerine ya da elde ediliş biçimine onay anlamına gelmediğini yazdı. Ona göre bu yayın işin sonu değil, başı: Sonuçları anlamak ve matematiğe katmak hâlâ insanların işi. Grup ayrıca matematikçilerin, yapay zekâya vitrin olsun diye seçilmiş problemler yerine kendi sorularını sorabilmesi gerektiğini vurguluyor.

Tepkiler karışık. Bazı matematikçiler sonuçların büyüklüğünü tarihî buluyor. Bazıları ise makalelerin okunmasının zor olduğunu ve bu kadar sonucu bir anda yayınlamanın, insanların o problemler üzerinde çalışma sürecini elinden aldığını söylüyor. Navier-Stokes yazımızdaki “kimin başarısı?” tartışması, şimdi yüzlerce problem ölçeğinde soruluyor. Sonrasını, aynı depoda yayınlanan üstel zaman hipotezi iddiasında anlattık.

Düşün

• Lean kontrolü olmayan bir sonucu, kontrol edilene kadar “kanıtlanmış” saymalı mıyız?
• Yapay zekânın yazdığı kodda sen hangisine daha çok güveniyorsun: kodu okumana mı, otomatik testlere mi?

Kendi cümlelerimizle yazılmış bir özettir, çeviri değildir. Tüm kaynaklar yukarıda.