Claude, Gödel'in stenografi defterlerini çözümledi ve yüzlerce bilinmeyen teoremi ortaya çıkardı

Ne oldu

Kurt Gödel'in yayımlanmamış defterlerini çözme çabası, projeye öncülük eden araştırmacı yapay zekâ modeli Claude ile çalışmaya başladıktan sonra ani bir sıçrama yaşadı. The Guardian'ın haberine göre model, mantıkçunun 1940'ların başında yazdığı 1.009 sayfalık notların kapsamlı bir analizini birkaç gün içinde üretti ve Gödel'in kimsenin farkında olduğundan çok daha fazlasını kanıtlamış olduğunu ortaya koydu.

Söz konusu malzeme, "çalışma defterleri" olarak bilinen 16 ciltlik bir külliyat; büyük bölümü, Gödel'in kullandığı döneminde bile eskimiş olan Alman stenografisi Gabelsberger ile yazılmıştı. 2017'den bu yana Fin mantıkçı Jan von Plato, Helsinki Üniversitesi'nde bu defterleri çözme projesine 2,5 milyon euro'luk bir Avrupa Araştırma Konseyi hibesiyle öncülük ediyor. İlerleyiş buzul gibi yavaştı: insan okuması haftada kabaca bir sayfa, yılda yaklaşık 50 sayfa ilerleyebiliyordu.

Dönüm noktası Ağustos ayında, Fransa'da yapay zekâ ve teorem kanıtlama üzerine düzenlenen bir konferansta geldi; bilgisayar bilimcileri von Plato'ya Claude'yi denemesini önerdi. Von Plato, modele çalışma defterlerinin transkripsiyonlarını, Gödel hakkında yazdığı altı kitabı ve diğer ikincil literatürü verdi. The Guardian'ın aktardığına göre sonuç, günler içinde üretilen 650 sayfalık bir açıklamaydı — hâlâ sayfa sayfa kontrol edilmesi gerekiyordu, ama von Plato bunu insan kapasitesini aşan bir görev olarak nitelendirdi; çünkü hiçbir okuyucu bin sayfalık yoğun mantığı aynı anda zihninde tutamaz.

Seçim aksiyomu sorusu

En çarpıcı bulgu seçim aksiyomuna ilişkin. 1966'da Paul Cohen, seçim aksiyomu ile süreklilik hipotezinin standart küme kuramından bağımsız olduğunu göstererek Fields Madalyası'nı kazandı. Gödel buna yanıt olarak bu bağımsızlık sonucunu 1940'larda kendisinin de kanıtladığını öne sürdü; ancak meslektaşları üzerinde ısrar ettiğinde kanıtı yeniden oluşturamadı.

Von Plato'nun Claude'ya sorduğu ilk soru, çalışma defterlerinde böyle bir kanıtın bulunup bulunmadığıydı. Yanıt, onun ifadesiyle "evet, neredeyse" idi: Gödel'in bir tanımı yanlıştı, oysa doğru versiyonu iki yıl önce ifade etmişti ve von Plato'ya göre birkaç ay daha çalışsaydı sonuca ulaşacaktı. Yeniden oluşturulan argüman, matematiksel kanıtları mekanik olarak doğrulayan bir proof assistant olan Coq'tan geçirildi ve kabul edildi. Von Plato, Gödel'in bu çalışmayı yayımlamış olsaydı 1940 Fields Madalyası'nı kazanacağını söylüyor.

Makine tarafından kontrol edilen 663 teorem

Von Plato ayrıca Claude'dan, Gödel'in çalışma defterlerinde kanıtı, kanıt taslağı ya da fikir tohumu bulunan her teoremi çıkarmasını istedi. Model 663 teorem buldu. Coq'ta kontrol edilenlerden yaklaşık 400'ü ifade edildiği şekliyle doğrulandı; kabaca 200'ü onarıldı — ifadeleri keskinleştirildi ya da ek varsayımlar eklendi — ve yaklaşık 50'si yanlış çıktı. The Guardian'ın da belirttiği gibi, Gödel bazen kendi hatalarını defterin kenarına "falsch!" ya da "schlecht!" gibi notlarla kendisi işaretliyordu.

Tekil sonuçların ötesinde von Plato, çalışma defterlerinde 1970'ler ve 80'lerde keşfedilen bulguların onlarca öncülünü ve bugüne dek ele alınmamış 14 mantık teması bulunduğunu söylüyor. Gödel'in hâlâ büyük ölçüde incelenmemiş fizik ve kozmoloji defterleri, listesindeki sıradaki hedef.

Bir uyarı notu

Herkes tarih kitaplarını yeniden yazmaya henüz hazır değil. Notre Dame Üniversitesi'nde mantık profesörü olan Joel David Hamkins, The Guardian'a Claude'un seçim aksiyomu kanıtına dair yeniden oluşturmasını görmediğini söyledi. Bu doğrulanırsa "dikkat çekici ve tarihsel açıdan ilginç" olur, dedi; ancak Claude'un katkısını Gödel'inkinden ayıklamak tarihçilerin işi. Hamkins'e göre Cohen'in kanıtını andıran defter pasajları Gödel'in bu yolda olduğunu gösteriyor — ama yayımlanmamış çalışma itibar kazandırmıyor.

Neden önemli

Bu öykü, yapay zekânın akademi dünyasında gerçekten yararlı olduğu noktaya somut bir tanıklık: hacmi işlemek ve insan kapasitesini aşan malzeme arasında bağlantılar kurmak. İnsan ilerlemesinin haftada sayfa ile ölçüldüğü bir külliyat, günler içinde, dünyada okuyabilen yalnızca birkaç kişinin bulunduğu bir stenografiyle sindirildi. En az bunun kadar önemli olan doğrulama örüntüsü — dil modeli yeniden oluşturmalar ve çıkarımlar önerirken bağımsız bir proof assistant bunları kontrol etti; bu da ham model çıktısını matematikte riskli kılan güvenilirlik sorunlarını hafifletiyor. Yöntem genellenebilirse, diğer çözülememiş ya da az incelenmiş bilimsel arşivler yakında yeniden okunabilir hâle gelebilir ve matematik tarihindeki bazı köklü öncelik sorularının yeniden gözden geçirilmesi gerekebilir.