Terence Tao’nun Proof Checker’lar ve yapay zeka programları hakkındaki görüşleri

Yapay zeka matematikçilerin 'ortak pilotu' olacak

Matematiğin değişimi

• Matematik geleneksel olarak yalnız yapılan bir alandı.
• Son dönemde matematiğin büyük bir kısmı, bilgisayarlarla doğrulanabilecek şekilde katı biçimde ayrı bileşenlere ayrılabiliyor.
• UCLA’den Terence Tao, bu yöntemlerin matematikte yeni işbirliği olanakları açtığına inanıyor.

Otomatik ispat denetleyicilerinin yükselişi

• Otomatik ispat denetleyicileri sayesinde matematikçiler yüzlerce kişiyle işbirliği yapabilir hale geldi.
• Örneğin Tao, Polynomial Freiman-Ruzsa (PFR) varsayımını 20’den fazla kişiyle birlikte çalışarak ispatladı.
• Süreç, her kişinin ispatın küçük bir adımına katkı sunması ve genel yönün merkezi olarak yönetilmesi şeklinde ilerliyor.

Matematiğin biçimselleştirilmesi

• Herkesin programcı olması gerekmiyor; roller, matematiksel yöne odaklananlar ile biçimsel ispatları oluşturanlar arasında paylaşılabilir.
• Standart matematik kütüphanelerinin gelişmesiyle biçimsel matematik pratik hale geliyor.
• Lean adlı proje, temel matematik teoremlerini içeren geniş bir kütüphaneye sahip.

Yapay zeka ve matematiğin geleceği

• Yapay zekanın matematikçiler için yardımcı bir rol üstlenme ihtimali var.
• Yapay zeka, ispatları biçimselleştirme, makale yazma ve gönderme gibi işlerde yardımcı olabilir.
• İnsanların fikir üretip yapay zekanın bunları biçimsel hale getirdiği bir işbirliği modeli mümkün olabilir.

Matematiğin yeni biçimi

• Yapay zekayla işbirliği içinde matematiğin yeni bir biçiminin ortaya çıkma ihtimali var.
• Matematikçiler rollerini proje yöneticileri gibi paylaşabilir, yapay zeka da ispatlara yardımcı olabilir.
• Matematik ders kitapları biçimselleştirilerek daha etkileşimli öğrenme araçları oluşturulabilir.

Yapay zekanın sınırları ve potansiyeli

• Yapay zeka, matematiğin büyük problemlerini çözmeye yardımcı olabilir; ancak insan sezgisi ve kavrayışı hâlâ önemli.
• Yapay zekanın sunduğu ispatları analiz edip anlayan yeni bir matematikçi türüne ihtiyaç duyulabilir.
• Yapay zeka matematiğin yeni alanlarını keşfedebilir ve insanların anlamakta zorlandığı kısımlarda yardımcı olabilir.

GN⁺ görüşü

• Yapay zekanın rolü: Yapay zeka, matematikçilerin daha büyük problemleri çözmesine yardımcı olabilecek önemli bir araç olabilir.
• İşbirliğinin önemi: Yapay zeka ile insanların işbirliği, matematikte yeni olanakların kapısını açabilir.
• Biçimselleştirmenin gerekliliği: Matematiğin biçimselleştirilmesi, daha fazla bilginin açık hale gelmesini ve işbirliğinin hızlanmasını sağlayabilir.
• Geleceğin matematikçileri: Yapay zekayla birlikte ispatları analiz edip anlayan yeni bir matematikçi türüne ihtiyaç duyulabilir.
• Teknolojik ilerleme: Yapay zeka ile matematiğin birleşimi, teknolojik gelişmelere paralel olarak daha fazla olasılık yaratabilir.

[GN⁺]

Hacker News görüşü

• Edsger Dijkstra'nın yazısı: Yazılım üretim biçimini hicveden 1975 tarihli bir yazıdan söz ediliyor; ana içeriği fikri mülkiyet eleştirisi.

• LLM'lerin yetenekleri: Şu anda yardımcı rolündeler, ancak ileride daha yüksek düzeyde içgörü sunma potansiyelleri var. Örneğin, nükleer bomba ile kompost yığını arasındaki ilişkiyi anlamak gibi, insanların gözden kaçırdığı noktaları yakalayabilirler.

• Röportaj özeti:

  • Proje yöneticisi matematikçi: Yapay zeka ve ispat yardımcı araçları, matematiksel içgörü üretmede devrim niteliğinde olabilir.
  • Örtük bilgi: Sezgi ve başarısızlık bilgisi makalelere dahil edilmediği için, matematikçiler arasındaki iletişim önemlidir.
  • Matematiğin biçimselleştirilmesi: İspat yardımcı araçlarının anlayışı desteklemek için matematiği daha fazla biçimselleştirmesi gerekir.

• Bilgisayar tarafından doğrulanan ispatlar: Yapay zeka, satranç motorları gibi, ispat doğrulamada faydalı olabilir. Çok sayıda teorem ve yardımcı lemmayı ele almak zor olsa da, yapay zeka bunu iyileştirebilir.

• Yazılım tarihi ve matematik: Geçmişteki yazılım projeleri ile günümüzün modüler yazılım mühendisliği karşılaştırılıyor; matematiğin de benzer bir yoldan gidebileceği görüşü dile getiriliyor.

• Terence Tao'nun konuşması: Matematik araştırmalarında Lean'in nasıl kullanılacağına dair daha ayrıntılı açıklama yapan bir konuşma öneriliyor.

• GPT-4 ile matematiksel ispat: GPT-4'ün yeni bir yardımcı lemmayı ispat etmeyi başardığı bir örnek sunuluyor. Bunun matematik araştırmalarında faydalı olabileceği belirtiliyor.

• Kariyerinin başındaki matematikçiler ve Lean: Kariyerinin başındaki matematikçilerin sezgilerine güvenip makale yazmalarının daha iyi olabileceği görüşü aktarılıyor.

• Başarısızlıktan öğrenmek: Başkalarının başarısızlıklarından öğrenmenin çok verimli olduğu görüşü dile getiriliyor.