Yapay zekâ matematiğin açık problemlerini çözmeye başladı: Lean kanıtı neden önemli?

Bir yazda neler oldu?

Bir yıl önce yapay zekâ modelleri matematik olimpiyatı sorularında başarılıydı. Ama olimpiyat soruları, cevabı bilinen bulmacalardır. Bu yaz iş değişti: Kimsenin çözemediği açık problemler düşmeye başladı.

• Jacobian sanısı (Temmuz). 1939’dan beri açık duran bu soru, Smale’in 21. yüzyılın zor problemleri listesindeydi. Kabaca şunu söylüyordu: Bir polinom fonksiyon her noktada yerel olarak “geri alınabilir” görünüyorsa, bütünüyle de geri alınabilir olmalı. Anthropic’te çalışan matematikçi Levent Alpöge, üç boyutta bunun yanlış olduğunu gösteren somut bir örnek paylaştı. Bulurken Claude Fable 5’ten yardım aldığını söyledi. İki boyutlu durum hâlâ açık. Anthropic’in Ağustos’taki Riemann zeta sonucunu ayrı bir yazıda anlattık.
• OpenAI’ın on sonucu (Ağustos). OpenAI, henüz yayınlanmamış bir modelinin matematik ve teorik bilgisayar biliminde on açık probleme sonuç ürettiğini açıkladı. Bunlardan biri, yüksek boyutta küre yerleştirme üzerine 1978’den beri kıpırdamayan bir sınırın iyileştirilmesi. Şirket, kanıtları Lean sertifikalarıyla birlikte herkese açık bir depoda paylaştı.

Lean: Kanıtı derleyiciye kontrol ettirmek

Bir matematikçinin yazdığı kanıtı başka matematikçiler aylarca okuyup kontrol eder. Yapay zekâ günde yüzlerce kanıt denemesi üretebiliyorsa, bu yöntem yetişemez.

Lean burada devreye giriyor. Lean hem bir programlama dili hem de bir kanıt denetleyicisi. Kanıtı onun diline çevirdiğinde, her adımın bir öncekinden kurallara uygun şekilde çıkıp çıkmadığını bilgisayar kontrol ediyor. Derlenirse kanıt geçerli, derlenmezse bir yerde hata var.

Yazılımcı gözüyle düşün: Yapay zekânın yazdığı kodu gözle okumak yerine tip denetleyiciye ve testlere güveniyorsun. Lean, bunun matematikteki karşılığı. Bu yüzden yapay zekâ + Lean birleşimi, “model uydurmuş olabilir mi?” sorusuna güçlü bir cevap veriyor. Ekim’de OpenAI yüzlerce sonucu birden yayınladı; bunların ne kadarının Lean ile kontrol edildiğini OpenAI’ın matematik arşivi yazısında anlattık.

Tek bir kural var: Lean yalnızca yazdığın ifadeyi kontrol eder. Problemi Lean’e yanlış çevirdiysen, doğru ama yanlış soruya ait bir kanıt elde edersin. Kontrol etmenin bulmaktan neden çok daha kolay olabildiği ise bilgisayar biliminin en ünlü açık sorusu: P vs NP yazımız.

Navier-Stokes ve “kimin başarısı?” tartışması

Eylül’de iş gerginleşti. Navier-Stokes denklemleri, sıvıların ve gazların nasıl aktığını anlatıyor. Hava tahmininden uçak kanadı tasarımına kadar her yerde kullanılıyor. Denklemlerin bir noktada “patlayıp” patlamayacağı sorusu, bir milyon dolar ödüllü Milenyum Problemleri’nden biri.

8 Eylül’de OpenAI, bir modelinin denklemlerin bir çeşidinde patlamanın olabileceğini gösterdiğini ve kanıtın Lean ile doğrulandığını açıkladı. Kanıt, dışarıdan bir kuvvet eklenen (“forced”) versiyonla ilgili. Clay’in resmî problem tanımı bu versiyona da izin veriyor. Ama matematikçilerin asıl merak ettiği, sıvının hiçbir dış etki olmadan da patlayıp patlamadığı. Ayrıntılar Navier-Stokes yazımızda.

OpenAI’ın duyurusundan yaklaşık 12 saat önce NYU’dan Tristan Buckmaster ve Levent Alpöge, bir yıldır üzerinde çalıştıkları ve yakından ilişkili Euler denklemleriyle ilgili makalelerini yayınladı. Buckmaster, OpenAI’ın kendi yöntemlerini öğrendikten sonra aynı yolu izlediğini ve yayın sırası konusunda baskı kurduğunu söylüyor. OpenAI ise onların istemlerini ya da kanıtlarını kullanmadığını söylüyor, ama yöntemin benzer olduğunu kabul ediyor.

Kimin haklı olduğunu biz bilemeyiz. Ama tartışmanın sorduğu soru önemli: Bir fikir dolaşmaya başladığında binlerce ajanla ondan önce sonuca koşmak mümkünse, araştırmacılar fikirlerini paylaşmaktan çekinir mi?

Terence Tao ne diyor?

Yaşayan en ünlü matematikçilerden Terence Tao, Temmuz’daki Uluslararası Matematikçiler Kongresi’nde bu dönemi “matematiğin değerleri ve pratiklerinde bir temel krizi” olarak tanımladı. Ona göre asıl soru, matematik araştırmasının amacının ne olduğu. Tao’nun önerdiği ölçüt de dikkat çekici: Hiçbir insanın düzgünce anlatamadığı bir kanıt, resmî olarak doğrulanmış olsa bile eksik sayılmalı.

Düşün

• Bir kanıtın doğru olduğunu bilmek mi daha önemli, neden doğru olduğunu anlamak mı?
• Yapay zekânın yazdığı kodu kontrol etmek için sen hangi “Lean”leri kullanıyorsun: testler, tipler, linter’lar?

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