10 bin ajan, 88 saat: OpenAI'ın Navier-Stokes iddiası tam olarak neyi çözdü?

Problem ne soruyor?

Navier-Stokes denklemleri, suyun, havanın, kanın nasıl aktığını anlatıyor. Uçak tasarımından hava tahminine kadar her yerde kullanılıyor. Ama denklemlerle ilgili temel bir soru 90 yıldır açık: Pürüzsüz başlayan bir akış, sonlu bir sürede patlayabilir mi? Yani bir noktadaki hız, belli bir anda sonsuza gidebilir mi?

Gerçek bir sıvıda bu olmaz, çünkü bir noktada artık molekülleri tek tek hesaba katman gerekir. Soru, denklemlerin bunu izin verip vermediği. Clay Matematik Enstitüsü 2000’de bunu, her biri bir milyon dolar ödüllü yedi Milenyum Problemi’nden biri yaptı.

Önemli bir ayrıntı: Resmî problem tanımı dört seçenek veriyor. İkisi “akış hep pürüzsüz kalır” demeyi, ikisi (C ve D) “patlama olabilir” demeyi gerektiriyor. Ve C ile D’de sıvıya dışarıdan pürüzsüz bir kuvvet uygulamak serbest.

OpenAI ne yaptı?

OpenAI’ın 8 Eylül’de yayınladığı açıklamaya göre süreç şöyle işledi:

• 1 Eylül’de, Anthropic’te çalışan matematikçi Levent Alpöge ile NYU’dan Tristan Buckmaster’ın büyük bir problemi çözmeye yaklaştığı söylentisini duydular.
• GPT-6 Astra’dan “belirgin şekilde daha yetenekli” bir iç modeli tüm açık Milenyum Problemleri’ne yönelttiler.
• Ajanları gruplara böldüler. Bir kısmına “bunu kanıtla”, bir kısmına “bunu çürüt” dediler. Navier-Stokes’u çözen grupta aynı anda yaklaşık 10 bin ajan çalıştı. Ajanlar internetin önbelleğe alınmış bir kopyasını okuyabiliyor, kod çalıştırabiliyor ve birbirine mesaj atabiliyordu.
• Ajanlar önce daha kolay bir akrabası olan Euler denklemlerinde sonuç buldu. Ekip bu sonucu Navier-Stokes’a odaklanan ajanlara verdi.
• Yaklaşık 88 saat sonra sonuç geldi: Spagetti gibi uzayarak içe doğru dönen bir girdap. Merkezi küçülürken hızı sonsuza gidiyor, toplam enerjisi ise sınırlı kalıyor.
• GPT-6 Astra kanıtı 17 saatte Lean’e çevirdi. Yalnızca bu problem için ajanlar 2,7 milyon mesaj attı ve yaklaşık 130 milyar token çıktı üretti.

Lean, kanıtın her adımını bilgisayara kontrol ettiren bir dil. Önceki yazımızda anlattığımız gibi, yapay zekânın ürettiği yüzlerce sayfalık bir kanıta güvenmenin en sağlam yolu bu. Lean dosyaları GitHub’da herkese açık.

Ne doğrulandı, ne doğrulanmadı?

• Lean kanıtı herkesin derleyebileceği şekilde yayında. Ama Lean, yalnızca yazılan ifadeyi kontrol eder. İfadenin Clay’in tanımıyla birebir örtüştüğünü yine uzmanların okuması gerekiyor.
• Hakemli bir dergide yayın yok. Clay’in kurallarına göre ödül süreci ancak saygın bir dergide yayından sonra, en az iki yıllık incelemeyle başlayabiliyor.
• Clay’in açıklaması temkinli: Problemin “görünüşe göre” çözüldüğünü yazdı, kimsenin adını anmadı ve sürecin bilerek acelesiz yürüyeceğini söyledi.
• OpenAI ödülü talep etmeyeceğini açıkladı.

“Yanlış problemi mi çözdü?”

Matematikçilerin itirazı kanıtın doğruluğundan çok, neyi gösterdiğiyle ilgili. Scientific American’ın konuştuğu uzmanlara göre OpenAI’ın sonucu Clay’in resmî tanımını karşılıyor, ama dışarıdan özenle seçilmiş bir kuvvet kullanıyor. Çoğu araştırmacının asıl merak ettiği ise sıvının hiçbir dış etki olmadan, kendi kendine patlayıp patlamadığı.

Dış kuvvet kullanan bu yol yeni de değil. İspanyol matematikçiler Diego Córdoba ve Luis Martínez-Zoroa yıllardır kâğıt kalemle bu yöntemi geliştiriyordu. Buckmaster ve Alpöge de onların programını yapay zekâ yardımıyla ileri taşımıştı. Buckmaster, modelin ilk ürettiği kanıtın hayatında okuduğu “en berbat” kanıt olduğunu yazdı.

Eylül ortasında Peter Constantin, Mihaela Ignatova ve Vlad Vicol bir makale yayınladı. Makaleye göre OpenAI’ınkine benzeyen yapılarda kuvvet, patlama noktasının yakınında ortadan kaldırılamıyor. Yani bu yöntemle kuvvetsiz problem çözülemez. Bu makale de henüz hakem incelemesinden geçmedi.

Ne öğreniyoruz?

Yapay zekâ, açıkça tanımlanmış bir hedefi aramakta artık çok güçlü. 10 bin ajan, problem tanımındaki her boşluğu bulup kullanabiliyor. Yazılımda da aynısı geçerli: Bir ajana “testler geçsin” dersen, testleri geçiren ama işi yapmayan bir kod da yazabilir. Sonucun değeri, hedefi ne kadar doğru tanımladığına bağlı.

Düşün

• Bir problemin resmî tanımını karşılamak ile gerçekten sorulan soruyu cevaplamak arasındaki farkı kendi işinde nerede gördün?
• Bir kanıtı ya da kodu bilgisayar doğruladıysa, bir insanın onu anlaması hâlâ gerekli mi?

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