OpenAI'nin 372 sonuçluk matematik dökümünde Unique Games Conjecture'ın bir AI kanıtı da var

Ne oldu

6 Ekim'de OpenAI, bir yapay zekâ modelinin ürettiği 372 matematiksel sonucu yayımladı ve liste, teorik bilgisayar biliminin en önemli açık problemlerinden biri olan Unique Games Conjecture'ın (UGC) bir kanıtını da içeriyor. Scott Aaronson'ın Shtetl-Optimized blogunda "The Mathocalypse" başlığıyla ele aldığı yayına göre, bu set, Timothy Gowers ve Edward Witten gibi seçkin matematikçilerden oluşan bir danışma grubunun önerisiyle bir araya getirildi. Aaronson'ın değerlendirmesine göre bu, matematiğin tarihindeki en büyük tek günlerden biri.

Ama bir pürüz var. Aaronson, UGC sonucu için bir Lean kanıt sertifikasının bulunduğunu, 372 makalenin bir kısmında da bulunduğunu ama kalanında olmadığını, yine de bu kanıtların şimdiye dek esas olarak hiçbir insan tarafından anlaşılmadığını yazıyor. Bu işleri okuma, doğrulama ve açıklama yarışı henüz yeni başladı.

UGC kanıtı ne içeriyor

Subhash Khot tarafından ortaya atılan UGC, geniş bir optimizasyon problemi ailesinin, standart bir araç olan yarıtanımlı programlama gevşetmesinin zaten sağladığından yalnızca biraz daha iyi bir yaklaşım istense bile NP-hard olarak kaldığını ima ediyor. Aaronson'ın eşi, karmaşıklık kuramcısı Dana Moshkovitz, kariyerinin neredeyse tamamını bu kanıtı elde etmeye adamış bir durumda; Aaronson, dokuz yaşlarındaki çocuklarının bir robotun onu "pişirdiğini" duyurduğunu anlatıyor.

Aaronson aracılığıyla aktarılan Moshkovitz'in kanıtla ilgili ilk okuması açık sözlü. Makale, yapay zekâ desteği olmadan okunamayacak kadar belirsiz yazılmış ve merkezi bir noise gadget için tamlık ve sağlamlık iddialarını, belgeye dağılmış ifadeleri birleştirerek bir yapay zekâ asistanı yardımıyla toplamak zorunda kalmış. Kanıt, Aaronson'ın aktardığı tanımla, bir noise testine sahip garip yeni bir özyinelemeli kod ortaya koyuyor; ne uzun kod ne de kısa kod, ama "yabancı" bir şey. Ayrıca yayının, UGC'yi tamamen atlayarak varsayımın amiral gemisi uygulamaları olan Max Cut ve tüm kısıt doyurulabilirliği problemleri için doğrudan optimal NP-hardness-of-approximation kanıtları içerdiğine de dikkat çekiyor.

Aaronson, onun durumundaki araştırmacılara iki teselli işaret ediyor: varsayım doğru çıkıyor (birçok meslektaşı bundan şüphe ediyordu) ve net biçimde tanımlanmış problemler üzerinde çalışan herkes artık aynı botada.

Geri kalan ganimet

Aaronson'a göre diğer sonuçların her biri, kendi alanında sıradan bir yıla damga vurma potansiyelindeydi. Sıraladığı öne çıkanlar arasında şunlar var: olasılıksal ve deterministik logspace'i çökerten L = BPL; 1960'lardan beri süren bir engeli kırarak tam sayı çarpımı ve Fourier dönüşümünü O(n log n) zamanının altında, yaklaşık O(n log^0.9999999999999 n) ile yapmak; Aaronson'ın 2007'de Greg Kuperberg ile birlikte ortaya koyduğu Unitary Synthesis Problem'in, çoğu araştırmacının beklediğinin tersine olumlu bir çözümü; 1999'dan beri açık olan paritenin QAC0'da olmadığının kanıtı; toplam Boole fonksiyonları için rastgele ve kuantum sorgu karmaşıklığı arasında yaklaşık dördüncü kuvvet ayrımı; 2D gapped Hamiltonian'lar için bir alan yasası; yeni bir yoldan rasyonel bir üsse ulaşmasıyla dikkat çeken O(n^2.25)'lik matris çarpımı; permanent'ın determinantal karmaşıklığı için Ω(n^3) alt sınırı; mükemmel eşleşmeleri yaklaşık olarak saymak için rastgele zamanlı polinom bir algoritma; ve hesaplanabilirlik kuramının tartışmasız en büyük açık problemi olan rasyoneller üzerinde polinom denklemlerini çözmenin hesaplanamaz olduğunun kanıtı. Ayrıca Riemann hipotezi, Hodge Conjecture ve Birch–Swinnerton-Dyer Conjecture yönünde kısmi ilerleme rapor edildiği bildiriliyor.

Eksik olanlar da anlamlı: P versus NP yok, P = BPP yok ve NEXP'in P/poly'dan ayrımı da yok; Aaronson bunun denemekten kaçınıldığı için olmadığını söylüyor.

Bir makine kanıtını yayımlamanın iki yolu

OpenAI'nin yayınından bir gece önce Virginia Williams ve Josh Alman, 3SUM'ı O(n^1.9992) zamanında ve tüm çiftler arası en kısa yolları O(n^2.9995) zamanında çözen bir arXiv ön baskısı yayımladı; bu, o problemler hakkında yaklaşık yarım yüzyıldır geçerli olan varsayımları çürüttü. Aaronson'a göre kritik fikir bir Anthropic modelinden geldi, ama Anthropic yayını farklı biçimde yönetti ve iki araştırmacıya, karşılığında tazminat ödeyerek özetlenmiş bir sürümü yazıp duyurma fırsatı tanıdı.

Aaronson, ortaya çıkan iki model arasındaki ödünleşimi çiziyor. Ham kanıtları alenen döken OpenAI yaklaşımı, bunları sindirmek ve açıklamak için rekabetçi ve büyük ölçüde minnettarlık görmeyen bir insan koşuşturması başlatıyor. Anthropic yaklaşımı ise özel bir şirketi, hangi matematikçilerin yapay zekâ keşiflerinin elçileri olacağını seçme konumuna sokuyor. 372 sonucun arkasındaki sistemin, milyonlarca dolarlık işlem gücü yakan binlerce ajandan oluşan özel bir sürü olmadığının bildirildiğini de ekliyor.

Neden önemli

Lean sertifikaları geçerli kalırsa, matematik, makinelerin hiçbir insanın henüz kavramadığı, biçimsel olarak doğrulanmış sonuçlar üretebildiği bir eşiği aşmış olacak. Darboğaz kanıtlamaktan okumaya kayıyor ve insan katkısı, Moshkovitz'in kendisinin çizdiği gelecekte olduğu gibi, problem seçimi, vizyon ve yorumlamaya doğru kayıyor. Yapay zekâ kanıtlarının literatüre nasıl gireceği ve bunları sindirene kredinin kime verileceği, şu an canlı kurumsal sorular; normu belirleme yarışında birbirinden çok farklı iki kurumsal model zaten rekabet ediyor.