Bu neden önemli?
Yapay zekânın ürettiği bir kanıta nasıl güveneceğiz? Cevap, yazılımcıların iyi bildiği bir fikirde: derleyicinin kontrol ettiği kod. Bu gelişme, bilimin nasıl yapıldığını ve kimin neyle anıldığını da değiştiriyor.
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.
- 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.
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.
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. Bu yüzden Clay Enstitüsü’nün ödül koşullarını karşılamıyor.
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?
Bu yazıdaki araçlar Araç Kutusu'nda: Lean