OpenAI bir yapay zekânın Navier–Stokes'u çözdüğünü açıkladı. Kanıt Lean dilinde yazıldı
OpenAI, yedi Bin Yıl Ödülü probleminden birine yapay zeka tarafından üretildiğini söylediği bir çözüm yayımladı — ve bunu bir bilgisayarın satır satır denetleyebileceği biçimsel bir kanıtla birlikte sundu.
Suyun bir boruda nasıl aktığını, havanın bir kanat üzerinde nasıl hareket ettiğini, dumanın bir sigaradan nasıl kıvrılarak yükseldiğini anlatan denklemlere Navier–Stokes denir. Bunlar, matematikçilerin alanın en zor açık soruları saydığı yedi Bin Yıl Ödülü probleminden biri. OpenAI şimdi bu probleme yapay zeka tarafından üretildiğini söylediği bir çözüm yayımladı.
Ortada bir yazı var, bir de daha alışılmadık bir şey: Lean dilinde yazılmış biçimsel bir kanıt. Lean, bir argümanın her adımının yazılım tarafından denetlenebilecek şekilde yazıldığı bir dil — okuyup başını sallamak değil, gerçekten doğrulamak. Bir adım yanlışsa, denetleyici kabul etmez. Üzerinde durulması gereken kısım tam olarak bu.
Büyük bir kanıtın dünyaya giriş şekli genelde yavaş ve insana bağlıdır. Biri bir el yazması paylaşır, dünyada bunu okuyacak yetkinlikte bir avuç uzman vardır, alanın hemfikir olması aylar hatta yıllar alır. Lean'de yazılmış bir kanıt bu sürecin şeklini değiştirir: makine tarafından denetlenebilir sürümü, dosyaya sahip herkes çalıştırabilir — ya derlenir ya derlenmez. Güven artık kağıtta kimin adının yazdığına bağlı değil.
Asıl hikaye manşetten çok bu aslında. "Yapay zeka artık zeki" değil — bu iddiayı yıllardır duyuyoruz, genelde laboratuvar dışında kimsenin tekrarlayamadığı bir benchmark puanına bağlı olarak. Bu sefer iddia, kendi denetim izini de yanında getiriyor.
Çalıştırabildiğin bir kanıt, güvenmek zorunda kaldığın bir kanıttan bambaşka bir şeydir.
"Çözüldü" kelimesine dikkatli yaklaşmalıyız. OpenAI bir çözüm paylaşıyor; matematik camiası henüz görüşünü bildirmedi ve bunun ne kadar süreceğine dair hiçbir fikrimiz yok. Söyleyebileceğimiz şey şu: duyurunun formatı, doğrulama tartışmasını uzun ve kapalı kapılar ardında değil, kısa ve herkesin gözü önünde yapıyor.
Şu anda ne okuyacağına karar veren herkes — biçimsel, makine tarafından denetlenen matematik, zor sonuçların yayımlanma biçimi haline gelirse, bu beceri birkaç yıl içinde nişten merkeze taşınır ve bugün Lean öğrenenler yarın bu dosyaları okuyacak kişiler olur. İşi "bana güvenin, kontrol ettim" demek olan herkes de bunun içinde: kontrolün yazılıma devredilebildiği an, uzman sözünün değeri düşer. Ve en sıradan haliyle, uçağa binen, duş alan ya da bir vantilatörün önünde duran herkes de — Navier–Stokes hareket eden akışkanın matematiğidir ve hiçbir zaman tam olarak anlaşılamadı.
OpenAI bir yazı ve bir Lean kanıtı yayımladı. Şimdi ne olacağı, matematikçilerin bu dosyayı çalıştırıp yazıyı okumasına bağlı — ve buna dair bir takvim verilmedi. İlk güvenilir bağımsız doğrulamayı ya da ilk ciddi itirazı izleyin. Bunlardan biri ortaya çıkana kadar bu, olağanüstü iyi belgelerle desteklenmiş yayımlanmış bir iddia — kesinleşmiş bir sonuç değil.
Bu problem üzerine bir asırlık çalışma, ancak birkaç düzine kişinin hakemlik yapabileceği parlak makaleler üretti. Bu seferki, bir dizüstü bilgisayarın denetleyebileceği bir dosyayla geliyor. Bu normalleşirse, matematikteki darboğaz doğrulama olmaktan çıkar — hayal gücü olur. Ki bu, tam olarak makinelerin yapamayacağını varsaydığımız kısımdı.
Kaynaklar: OpenAI Blog, "On the Navier–Stokes Millennium Prize Problem" (openai.com/index/navier-stokes-solution)
Doğrulama teyit edilirse, bir makine insanlığın bir asırdır uğraştığı problemi ilk kez çözmüş olacak — üstelik söze güvenmekle değil, satır satır yeniden kontrol edilebilen biçimsel bir kanıtla.
THE TELL’in yapay zekâ haber merkezi tarafından yazıldı. nasıl çalışıyoruz · düzeltmeler