Terence Tao’nun Gözünden Kanıt Denetleyiciler ve Yapay Zeka Matematik Copilot’ları

 (scientificamerican.com)
1 puan yazan GN⁺ 2024-06-13 | 1 yorum | WhatsApp'ta paylaş
  • Matematiksel kanıtlar daha sıkı biçimde formelleştikçe, Lean gibi araçlar insanların kanıtlarını doğruluyor ve büyük ölçekli iş birliklerinin güven temelini değiştiriyor
  • mathlib gibi standart kütüphaneler biriktikçe, lisans düzeyi teoremlerden yeni alanlara kadar formelleştirme için giriş bariyeri düşüyor
  • PFR varsayımının formelleştirilmesinde 20’den fazla katılımcı küçük kanıt adımlarını paylaştı; Terence Tao ise satır satır incelemeden çok genel yönü yönetmeye odaklandı
  • Yapay zeka, matematiği hemen “çözmekten” ziyade formelleştirme, doğrulama ve tekrarlı işleri destekleyen bir kanıt copilot’u rolüne daha yakın
  • Matematik araştırması; insanın yön belirlemesi, ayrıntılı formelleştirme, yapay zeka eğitimi ve yapay zeka kanıtlarının yorumlanması gibi daha açık ve iş bölümlü görevlere dönüşebilir

Formelleştirmenin matematik iş birliğini değiştirmesi

  • Geleneksel matematik araştırması küçük ölçekli iş birliklerine yakındı; Tao genellikle yaklaşık 5 kişinin iş birliği ölçeğinde üst sınıra yakın olduğunu düşünüyor
  • Otomatik kanıt denetleyicisi (proof checker) olduğunda, birbirini tanımayan yüzlerce kişiyle bile iş birliği yapılabilir
    • Katılımcılar kodu yükler, Lean compiler doğrular
    • Güven yalnızca kişisel ilişkilere dayanmaz; formel doğrulama sonuçlarıyla teyit edilebilir
  • Polynomial Freiman-Ruzsa(PFR) varsayımının yakın tarihli sonucunu formelleştirirken 20’den fazla kişi katıldı
    • Kanıt çok sayıda küçük adıma bölündü
    • Her katılımcı bir adımın kanıtını üstlendi
    • Tao, tüm katkıları satır satır kontrol etmek yerine genel ilerleme yönünü yönetti

Her matematikçinin programcı olması gerekmez

  • Formelleştirme projelerinde rol paylaşımı mümkündür
    • Bazı kişiler matematiksel yöne odaklanır
    • Bazıları küçük matematik parçalarını formel kanıtlara dönüştürme işinde uzmanlaşır
  • Peter Scholze gibi bilgisayara aşina olmayan matematikçiler de Lean projelerine katılabilir
  • Büyük matematik görevleri küçük parçalara ayrıldığında, tüm teoriyi anlamadan belirli alt görevlere katkı sağlanabilir

Lean, mathlib ve aramanın sağladığı pratiklik

  • Formel matematiğin pratik hale gelmesinin büyük nedenlerinden biri standart matematik kütüphanelerinin gelişmesidir
  • Lean’de mathlib adlı büyük ölçekli bir proje var
    • Kalkülüs ve topoloji gibi lisans matematiğinin temel teoremleri tek tek kütüphaneye giriyor
    • Amaç, kütüphaneyi lisansüstü düzeye kadar taşımak
    • Bu gerçekleştiğinde yeni matematik alanlarını formelleştirmek kolaylaşacak
  • Kanıt oluşturmak için daha önce doğru olduğu doğrulanmış teoremleri bulmak gerektiğinden, daha akıllı arama motorları da önem kazanıyor
  • PFR projesinin tamamı formelleştirildikten sonra doğrulama derlemesi yalnızca yaklaşık 30 dakika sürüyor
    • Darboğaz, hesaplama gücünden çok kullanılabilirlik, kullanıcı dostu olma ve insanların araçlara uyum sağlamasında
  • Lean şu anda en aktif topluluğa sahip formel dil olarak değerlendiriliyor
    • Tek yazarlı projeler için başka diller daha iyi olabilir
    • Lean’i öğrenmek kolay; kütüphanesi ve topluluğu iyi
    • İleride başka alternatiflerle yer değiştirebilir, ancak şu anda baskın formel dil konumunda

Formelleştirme maliyeti hâlâ yüksek

  • Tao, bir projeyi formelleştirebileceğini ancak şu anda bunun kendi zamanından bir ay alabileceğini düşünüyor
  • Henüz tüm sonuçları rutin olarak formelleştirme aşamasında değiliz
    • Lean öğrenmeye yardımcı olduğu durumlar
    • Sonucun doğruluğuna yönelik ilginin yüksek olduğu durumlar
    • Formelleştirmenin gerçekten değer kattığı projeler seçilmeli
  • Teknoloji geliştikçe formelleştirme maliyeti azalabilir
    • Şu anda geleneksel yöntemden 10 kat daha uzun sürebilir
    • Gelecekte yaklaşık 2 kata, hatta 1 katın altına kadar düşme olasılığı var

Yapay zeka matematikçinin copilot’u olabilir

  • Tao, gelecekte matematikçinin kanıtı doğrudan yazmak yerine GPT benzeri sistemlere açıklama yaptığı, yapay zekanın da süreç içinde Lean formelleştirmesini denediği bir yöntemi hayal ediyor
    • Doğrulama başarılı olursa LaTeX makalesi ve Lean kanıtı birlikte sunulabilir
    • Kullanıcı isterse dergiye gönderime kadar yardımcı olan bir asistana dönüşebilir
  • Şu anda en hızlı formelleştirme yolu hâlâ önce insanın kanıt fikrini ve taslağını oluşturmasıdır
  • Uzun vadede, insan tüm kanıtı bilmeden küçük parçaları formelleştirip, yapay zeka ve insanın birlikte bunları bağlayarak büyük bir teoremi kanıtladığı projeler de mümkün olabilir
    • Tao, böyle bir yöntemin mümkün hale gelmesi için birkaç yıl gerektiğini düşünüyor
    • Mevcut teknoloji hâlâ yetersiz ve formelleştirme de hâlâ zahmetli bir iş

“Matematik çözülecek” öngörüsüne mesafe

  • Tony Wu ve Christian Szegedy, 2–3 yıl içinde makinelerin insanlardan daha iyi kanıt bulması anlamında matematiğin “çözüleceğini” söylemişti
  • Tao, 3 yıl içinde yapay zekanın matematikçiler için yararlı hale gelebileceğini ve belirgin ilerleme yaşanabileceğini kabul ediyor; ancak matematiğin çözüleceğini düşünmüyor
  • Yapay zeka, kanıttaki bir adım doğru gibi göründüğünde ama insan bunu hemen göremediğinde yardım istenen bir copilot olabilir
  • Yapay zeka bugün insanların yaptığı düzeyde matematik yapabilse bile, insan matematikçiler daha yüksek düzeyde matematiğe geçebilir
  • Yapay zeka sayesinde tek seferde yüzlerce ya da binlerce teoremi kanıtlayan yöntemler de mümkün hale gelebilir
    • İnsan matematikçi, yapay zekanın ne yapacağını yönlendiren rolü üstlenir
    • Tao, bu değişim için 2–3 yıllık zaman çizelgesi öngörüsünü biraz agresif buluyor

Kanıtı anlama ve yapay zeka üretimi kanıtlar

  • Matematiksel kanıt yalnızca doğruluğu teyit eden bir prosedür değil, neden doğru olduğunu anlama sürecidir de
  • Yakın gelecekte yapay zeka muhtemelen önce sıkıcı ve önemsiz işleri otomatikleştirecek; insan ise yön belirlemeyi sürdürecek
  • Yapay zeka anlaşılması zor ve çirkin bir kanıt ortaya koyarsa, insan bu kanıtı yeniden analiz edebilir
    • Örneğin 10 varsayımla sonuca ulaşılan bir kanıtta, varsayımlardan biri çıkarıldığında da geçerli olup olmadığı kontrol edilebilir
  • Yapay zeka üretimi kanıtlardan içgörü çıkaran yeni bir matematikçi türü ortaya çıkabilir
    • İlk yapay zeka kanıtlarında içgörü yokmuş gibi görünebilir
    • İnsanlar bu kanıtları daha anlaşılır hale getirip yapısını ortaya çıkarabilir

Çözülmemiş problemler ve yapay zekanın sınırları

  • Açık varsayımları kanıtlamak için önce onları daha küçük parçalara ayırmak gerekir
  • Bir problemi daha kolay bir probleme dönüştürmektense daha zor bir probleme dönüştürmek çok daha kolaydır
  • Tao, yapay zekanın bu parçalama işinde insandan daha iyi olduğuna dair bir yetenek henüz göstermediğini düşünüyor
  • Yapay zekanın farklı alanlar arasında olası bağlantılar önermesi ilginç bir kullanım alanı
    • Şu an başarı oranı düşük
    • 10 öneriden yalnızca 1’i ilginç, 9’u işe yaramaz olabilir
    • Tao, gelecekte bu kısmın değişebileceğini düşünüyor

Matematik bilgisinin veri sorunu

  • Matematik yapay zekası eğitiminin sorunlarından biri yeterli verinin olmaması
  • Çevrim içi makaleler eğitimde kullanılabilir, ancak birçok matematiksel sezgi makalelerde yer almaz
    • Matematikçiler arasındaki konuşmalar
    • Dersler
    • Öğrencilere danışmanlık yapma biçimleri
    • Başarısız denemeler ve düzeltme süreçleri
  • Yayımlanmış kanıtlar sıkıştırılmış sonuçlardır ve insanlar yalnızca başarı örneklerini yayımlama eğilimindedir
  • Gerçekten değerli veri, bir şeyin denendiği ancak iyi gitmediği ve bunun nasıl düzeltildiğini içeren süreçtir
  • Gelecekte araştırma denemeleri ve başarısızlık süreçleri kaydedilip yapay zeka eğitimi veya başka araştırmacıların aynı başarısızlıkları tekrar etmesini önlemek için kullanılabilir
    • Tao, 2040’ın gelişmiş yapay zeka Lean’i gibi bir sistemi kullanmak için araştırma sürecinin kaydedilmesine onay verilen bir durumu örnek gösteriyor

Daha açık matematiğe doğru değişim

  • Matematik bilgisinin büyük kısmı tek tek matematikçilerin zihninde hapsolmuş durumda; yalnızca çok küçük bir kısmı açık biçimde geride kalıyor
  • Formelleştirme arttıkça örtük bilgi daha çok açık bilgiye dönüşür
  • Formelleştirilmiş ders kitapları etkileşimli ders kitaplarına yol açabilir
    • Üst düzey kanıt açıklamalarından başlar
    • Anlaşılmayan adımlar daha ayrıntılı biçimde açılabilir
    • İstenirse aksiyom düzeyine kadar inilebilir
  • Bu yöntem, bir alandaki matematikçinin başka bir alana katkıda bulunmasını kolaylaştırabilir
    • Büyük bir görevin alt görevleri net biçimde belirlenebilir
    • Bütününü anlamadan gerekli parçaya katılım sağlanabilir

İlgili okumalar

1 yorum

 
GN⁺ 2024-06-13
Hacker News yorumları

  • https://archive.is/Idouw

  • project manager mathematicians ifadesi, Edsger Dijkstra’nın 1975’te yazdığı hiciv metni “A letter to my old friend Jonathan”ı [1] ve devam yazısını [2] akla getiriyor
    Yazı, yazılım geliştirme biçiminin matematiğe uygulanması halinde bunun ne kadar gülünç olacağını gösterip eleştiriyordu; ama bir açıdan ileri görüşlüymüş
    Asıl mesele, fikri mülkiyet haklarının, özellikle de matematiksel hakikate uygulanmasındaki saçmalığı eleştirmekti; neyse ki bugünkü mekanizasyon eğiliminde bu kısmın büyük bir endişe olmadığı görülüyor
    [1]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD04xx/E...
    [2]: https://www.cs.utexas.edu/users/EWD/transcriptions/EWD05xx/E...

    • LLM’ler de matematik yapabilir. Biçimselleştirme yoksa bu makale şu anki en üst seviyeye yakın görünüyor: https://arxiv.org/abs/2301.13867
    • Bu karşılaştırma pek mantıklı gelmiyor. Yazılımın %99,999’u en ileri teknoloji değil, yönetilebilir mühendislik uygulamasıdır

  • İçgörülü bir yazı, ancak eksik kalan noktanın LLM’lerin giderek insanüstü biçimde soyutlama yapması olduğunu düşünüyorum
    Tao, “bir problemi daha zor hale getirmek kolaydır ama daha basit hale getirmek zordur; yapay zekanın bu konuda insanlardan daha iyi olduğunu gösterdiğini hiç görmedik” diyor; ancak LLM’lerin çalışma biçimi çok daha yüksek düzeyde içgörüleri mümkün kılabilir
    Şimdilik daha çok yardımcı, doğruluk kontrolcüsü ve sıkıcı işleri yapan bir araç gibiler; ama yakında içgörü öneren varlıklar olacaklar. LLM’ler şimdiden gömme uzayları ve bilgiyi sıkıştırıyor, bizim göremediğimiz içgörülere sahipler
    Hinton’ın nükleer bomba ile kompost yığını arasındaki ilişkiyi örnek verdiği bölüm: https://www.youtube.com/watch?v=Gg-w_n9NJIE&t=4613s

    • LLM’lerin en büyük sorunu, internetteki sayısız insan yazısının yalnızca bir regresyon modeli olmaları
      İnsanların yazma biçimini taklit etmek üzere eğitilmiş makinelerden ibaretler ve insandan daha zeki bir şeyi taklit etmek için gereken eğitim verisine sahip değiller
      Makine öğreniminin insan zekasını aşacağından şüphem yok; ancak darboğaz, dünya genelindeki tüm yazılara regresyon yapmak yerine, insan müdahalesi olmadan kendi çıktılarıyla kendini eğitmesini sağlamanın yolunu bulmak
      Ramanujan düzenli eğitim almadan ve yalnızca birkaç matematik kitabı görerek parlak matematiksel keşifler yaptı; bu, bir makine öğrenimi modelinin eğitim verisi açısından neredeyse hiçbir şey sayılmayacak bir miktar
    • Hinton’ın örneği bana pek etkileyici gelmiyor. Hobi olarak bahçecilik yaptığım için “nükleer silahlarla kompost yığınlarının ortak noktası nedir?” sorusuna hemen kritik kütle cevabı aklıma geldi
      Bunu kelimelere dökmem yaklaşık 10 saniye sürdü, ama gerekli bilgiyi biliyorsanız cevap barizdi
      Hinton bunun analojik düşünmeyi gösterdiğini söylüyor; ancak bahçecilik yazıları ve kompost yığınlarının fiziğiyle ilgili anlatılar internette çok fazla ve ChatGPT’nin eğitim sırasında bunları zaten görmüş olması gayet olası
      Bu yüzden bu örnek, LLM’nin eğitim metinlerinde cevabı fiilen daha önce görmüş olma ihtimalini kontrol etmeyen bir vaka gibi görünüyor
      Videonun devamında Ilya’nın “varlık kanıtı var. İnsan beyni bir sinir ağıdır” dediği bölüm (https://youtu.be/Gg-w_n9NJIE?t=4966) de ilginç. İnsan beyninin de bir sinir ağı olduğu görüşüne genel olarak katılıyorum; ancak gerçek nöronların 8 bit çalışmadığı, hücre türleri, DNA ve hormonların kimyasal ortamı gibi şeylerin farklı olduğu yönünde pek çok karşı argüman da var; bu yüzden burada felsefi bir ayrım noktası olduğunu düşünüyorum
    • Yapay zeka tabanlı bir sistem matematik kanıtı yazma uzmanı haline geldiğinde, bir tane daha elde etmenin maliyeti dosyayı kopyalayıp başka bir cloud instance üzerinde çalıştırmaktan ibaret olur
      Bu birkaç dakika ile birkaç saat arasında yapılabilir
      Buna karşılık bir insan uzman daha elde etmek için matematiği meslek olarak sevecek birinin ortaya çıkması, onlarca yıllık eğitim ve ileri uzmanlaşmadan geçmesi gerekir; üstelik o kişinin sonuna kadar devam edeceğinin ve bilginin en ön safını ileri taşıyacak seviyeye ulaşacağının garantisi de yoktur
      O zamanı beklerken paralel çalışan trilyonlarca yapay zeka uzmanı oluşturulabilir
      İnsan beyninin yeni bilgiyi soğurma bant genişliği düşüktür; makineler ise bir ömürlük bilgiyi saniyeler içinde kopyalayabilir, binlerce sohbeti paralel yürütebilir ve beynin bir kısmını serileştirip başka bir yapay zekaya gönderebilir. Programlanabilir maddeye kadar ulaşıldığında computronium’u üstel biçimde üretmek ve birkaç saniyede binlerce yıllık araştırma yapmak gibi bir omega noktası da mümkün hale gelir
    • “Yardımcı, doğruluk kontrolcüsü ve sıkıcı işleri yapan araç” üçlüsünde doğruluk kontrolcüsü diğerlerinden farklı bir karaktere sahip

  • Matematikten hiç anlamıyorum ama yazılım tarihini hatırlatıyor. Eskiden RollerCoaster Tycoon gibi şaşırtıcı projeler neredeyse tek bir kişinin eseri olurdu.
    Sonra yazılım mühendisliği, röportajda anlatılana benzer şekilde modülerleşti; bugünse benim gibi insanların geçimini sağlamak için React üretip durduğu dev bir montaj hattına dönüştü ve kişi başına üretkenlik ya da gereken beceri neredeyse 0’a yaklaşmış gibi görünüyor.
    Bir alan altın çağındayken bir dâhi kafasında yüz şeyi tutup en iyi işi çıkarıyor; bu bir montaj hattıyla değiştirildiğinde de o alan artık gerçekten değerli bir şey üretemez hale geliyor izlenimi veriyor.

    • Bu sezgi, insanın özündeki gücü, yani bizim yalnızca bireyler olmadığımızı, birlikte çalışarak tek bir bireyden daha büyük işler yapabildiğimizi inkâr ediyor.
      Yazılım mühendisliği harika işler yapmayı bırakmadı; bence tam tersine.
    • Daha içine çeken işler istiyorsan maaşını düşürüp bir startup’a gidebilirsin. Orada aynı derecede tembel ve dağınık insanların daha “otoriter görünen” dillerle daha da berbat kod yazmış olması muhtemel.
      Şaka bir yana, bir gün kritik bir bug’ı düzeltmen gerektiğinde beceri ortaya çıkar. Bir ürünün ya da hizmetin istikrarlı ve kârlı hale gelmesi, ilk geliştiricilerin ayrıldığı ya da kimsenin büyük işler başaramayacağı anlamına gelmez.
    • Bu değerlendirme haksız. RollerCoaster Tycoon gibi eski projelerde kişi başına üretkenlik etkileyici ama ortaya çıkan bütün sonuç modern oyunlarla karşılaştırıldığında sönük kalıyor.
      Bu alanın artık gerçekten değerli bir şey üretmediğini söylemek çok yanlış.
      100 kişinin 100 yılda yaptığı bir katedralle, bir kişinin bir ayda yaptığı kulübeyi karşılaştırmak gibi. Kulübe de ayakta durur ve barınacak yer sağlar ama katedral değildir.
    • Yazılımın uzmanlaşması ve sanayileşmesinin uç düzeyde modülerleşme ve parçalanma doğurduğunu düşünüyorum.
      Web geliştirme tarafında, yalnızca Python’a bakmaya çalışsanız bile çarkın her küçük dişlisi için o kadar çok framework ve teknoloji var ki takip etmek gerçekten zor.
    • Genel olarak katılıyorum. “Benim React uygulamam da bana zor ve meydan okuyucu geliyor” tepkisine takılıp kalmak asıl noktayı kaçırıyor.
      Beceri çoğunlukla log-normal dağılım izler; bu yüzden istisnai insanlar zaten azdır. Erken aşamadaki küçük alanlarda destek altyapısı eksik olduğundan yalnızca aşırı yetenekli kişiler ayakta kalır ve zirve yetenek yoğunluğu gerçekçi olmayacak kadar yüksek olabilir.
      En yeni 47 framework’ü zorla birbirine bağlayıp yapılacaklar listesi uygulaması basmak ile anlamlı bir etki yaratmak temelde farklı şeylerdir.
      Maliyet-fayda açısından bakınca, büyük işlere uzun vadeli yatırım yapmak yerine ucuza çok kod püskürtme tarafında güçlü bir yerel optimum vardır; alan olgunlaştıkça bu noktaya ulaşmak için gereken beceri eşiği düşer.
      Zirve yetenekleri eğitmeye odaklanan kuruluş sayısı da fazla değildir. Bu yüzden alan büyüdükçe ortalama becerinin kendi hâline bırakıldığında düşmesini açıklamak kolaydır; dağılımı yanlış ele almak sonradan düzeltmesi pahalı bir soruna dönüşebilir.

  • Bilgisayar tarafından doğrulanan ispatlar, yapay zekanın oldukça yakın vadede yararlı olabileceği bir alan. Ancak tam teşekküllü bir LLM’den çok, satranç motorlarındaki sinir ağlarına daha yakın olabilir.
    Her şeyi elle ispatlamak sıkıcı ve zaman alıcı olduğu için zaten çok sayıda solver kullanılıyor; ancak taktikler ya da solver’lar, üzerlerine çok fazla teorem ve yardımcı teorem atıldığında zorlanıyor.
    İlgili yardımcı teoremleri örüntü eşleştirmeyle bulan bir arama makinesi olarak sinir ağı buna iyi uyuyor.
    Tümevarım ve yüksek mertebeden birleştirme de aslında kod sentezidir; mümkün olan tüm sözdizimi ağaçlarını körlemesine yinelemek çok verimsizdir.
    Solver zaten backtracking yaptığı için yapay zeka %95 işe yaramaz yardımcı teorem önerse bile sorun değil; elle aramaya kıyasla dramatik biçimde daha iyi olabilir.
    Yine de bilgisayar tarafından doğrulanan ispatların iletişim açısından mutlaka iyi olup olmadığından emin değilim. İnsanların okuduğu ispatlar yalnızca uzunluk nedeniyle değil, başka birçok nedenle de yüksek seviyelidir ve ayrıntıları atlar.

    • Matematikçi değilim ama ispat denetleyicilerinin nasıl çalıştığına bakınca, büyük gelecek atılımları olmadan pratikleşmelerinin zor olduğunu düşünüyorum. Şu anda kesinlikle değil.
      Temel sorun, ispatta kullanılan matematiksel nesnelerin biçimsel tanımlarıyla bağlantılı olmak zorunda olması.
      Ama insanlar ispat yazarken ya da okurken böyle düşünmez. Genellikle ne yaptıklarına dair “ahlaki” düzeyde, yüksek seviyeli ve biçimsel olmayan bir sezgileri vardır; gerekli oldukça biçimsel ayrıntıları doldururlar.
      Bilgisayar kodunda dilin biçimsel semantiği zihinsel modele çok daha yakındır, bu yüzden bir ölçüde işler; ama matematikte hedef genellikle farklıdır.
    • Otomatik teorem ispatlama zaten uzun zamandır var olan bir kavram.
      Isabelle’in sledgehammer stratejisi, E, Z3, SPASS, Vampire gibi otomatik teorem ispatlayıcıları birleştirerek hedefi ispatlamaya ya da çürütmeye çalışır.
      Teoride iyi görünür ama pratikte rastgele görünen 12 yardımcı teoremin uygulandığı yeniden kurulmuş ispatlar çıkar; bu ispatlar okunamaz ve çok kırılgandır.
      Yapay zekanın bu sorunu sihirli biçimde çözecek gibi görünmüyor.
    • Doğru. Ancak örnek verimliliği konusunda büyük ilerleme gerekiyor.
      Mevcut sinir ağlarının örnek verimliliği son derece düşük ve biçimsel matematik veri kümeleri Python kodu gibi veri kümelerinden çok daha küçük.

  • Terence Tao birkaç ay önce bu konuda mükemmel bir konuşma yaptı ve Lean kullanımını daha ayrıntılı ele aldı: https://www.youtube.com/watch?v=AayZuuDDKP0

  • Görev başındaki bir matematikçinin, araştırma sırasında GPT-4o’ya muhtemelen yeni bazı yardımcı önermeleri kanıtlattığı söyleniyor
    “Partnerim matematikçi; geçen hafta ilk kez ChatGPT’yi kullanarak araştırma amaçlı birkaç yardımcı önermeyi kanıtlamayı denedi. Bu teoremlerin doğru olduğundan zaten şüpheleniyordu ve kabaca bir yaklaşımı da vardı, ama o tür önermelerin uzmanı değildi. Modelden doğru ve işe yarar bir kanıt aldığı ilk sefer buydu
    İlk yardımcı önerme, bir işbirlikçinin küçük e değerleri için yaptığı hesaplarda bulduğu bir şeydi. ChatGPT, Möbius fonksiyonunu denemesini söyleyene kadar kanıtı bulamadı
    https://chatgpt.com/share/9ee33e31-7cec-4847-92e4-eebb48d4ff...
    İkincisi biraz daha standart görünüyor ve Mathematica da yapabilirdi gibi. Ama Mathematica temiz bir çıkarım vermediği için yine de faydalı
    https://chatgpt.com/share/7335f11d-f7c0-4093-a761-1090a21579...”

    • Ben Goertzel yakın tarihli bir röportajda, kendisinin ve meslektaşının ortaya attığı yeni bir matematik fikri üzerine GPT-4 ile doktora düzeyinde bir tartışma yaptığını söyledi
      Bu şeyler akıl yürütmede ve ağır konularda ürkütücü derecede iyi hale geliyor
      Makine öğrenmesi alanı, LLM’lerin büyük ölçüde Sistem 1 düşüncesini tamamlayacak Sistem 2 yetenekleri eklemeye odaklanmayı sürdürürse işler sertleşecek gibi
    • İkinci kanıtın bir kitapta ya da e-kitapta bir yerlerde bulunma olasılığı oldukça yüksek görünüyor. Aklıma generatingfunctionology geldi
      Etkileyici olan hafıza; yeni bir akıl yürütme değil
    • Alıntının kaynağını merak ediyorum. İlki, yakın zamanda arkadaşım Beren’le konuştuğumuz şeye benzediği için ilginç
      Biz bunu |τ|! katsayılı bölme toplamı olarak değil, sıralı bölmelerin toplamı olarak düşünmüştük; ama ikisi elbette aynı şey
      Döngüsel olarak sıralı bölmelerde, yani |τ|! yerine (|τ|-1)! katsayısı kullanınca (-1)^e değil 0 çıkıyor
      Beren’in kombinatorik kanıtı, özel bir eleman seçip, o eleman tek başınaysa onu bir sonraki parçayla birleştiren, tek başına değilse kendi parçasına ayıran bir yöntemle çift uzunluklu ve tek uzunluklu döngüsel sıralı bölmeler arasında bir bijeksiyon kuruyor
      Doğrusal sıralama durumunda da benzer biçimde son elemandan başlayarak uygulanıyor; ancak son elemanın son parçada tek başına olduğu bölmeler eşleşmediği için yinelemeli olarak bir sonraki elemana geçiliyor
      Sonunda her şey eşleşiyor ve yalnızca tüm elemanların ayrı ayrı ve özgün sırada olduğu bölme kalıyor. Özgün kümenin boyutunun tek-çiftliğine göre işaretli toplam, ilk önermeye götürüyor
    • İkinci kanıt gerçekten çok pürüzsüz. Neden doğru olduğuna dair cebirsel kanıt dışında kombinatorik bir kanıt var mı merak ediyorum
    • İlk örnekte ChatGPT düpedüz anlamsız bir çıktı üretmiş. 6. adımdaki τ ≤ τ üzerindeki toplama bakınca τ’nun toplamın bağlı değişkeni mi yoksa serbest değişkeni mi olduğu belirsiz
      “τ ≤ τ” üzerindeki toplamda kaç terim olduğunu da bilmiyorum; bunun 3. maddenin sol ya da sağ taraflarından birini kurup sonra diğer tarafı sonuçlandırmakla nasıl bağlandığı da oturmuyor
      Aslında ChatGPT, bölme kafesinin Möbius fonksiyonunu hatırlayıp kanıtsız biçimde tekrarlamış, sonrasında da dışarıdan makul görünen saçmalıklar üretmiş
      O Möbius fonksiyonunu kurmak zaten esas nokta; soru neredeyse o fonksiyonun bu biçimde olduğunu kanıtlamayı istemekle aynı
      Üstelik ChatGPT’nin verdiği genel formül de biraz yanlış; yalnızca mevcut kanıt için önemli olan |σ| = 1 durumunda doğru
      Bu olgu, Möbius fonksiyonu aygıtının tamamını açıkça kullanmadan da N(t,e)’yi t eşdeğerlik sınıfına ayıran bölmelerin sayısı olarak alıp N(t,e+1)=N(t-1,e)+tN(t,e) yineleme bağıntısıyla temel tümevarım yaparak hemen görülebilir

  • Bu röportajda üç şey öne çıkıyor
    Birincisi, Tao matematiksel içgörünün de toplumun diğer çıktıları gibi “üretildiği” bir gelecek tasavvur ederek project manager mathematiciansdan söz ediyor. Matematiğin henüz bu kadar sanayileşememiş olmasının nedenini araç eksikliğinde görüyor; yapay zeka ve kanıt yardımcılarının bu noktada devrimsel olabileceğini düşünüyor. Bununla birlikte insan etkileşimi ve yönlendirmesi hâlâ gerekli
    İkincisi, makalelerde yer almayan çok fazla örtük bilgi var. Sezgi ya da başarısızlık bilgisi gibi şeyler önemli; en iyi matematikçiler bile aynı hataları tekrarlamamak için birbirleriyle konuşmak zorunda
    Üçüncüsü, matematiğin zaten yeterince biçimselleştirilmiş olduğunu düşünmek kolay, ama makalelerde çok fazla ortak bilgi varsayılıyor. Kanıtları, kanıt yardımcılarının anlayabileceği şekilde biçimselleştirmek, daha fazla kişinin gerçekte ne olup bittiğini anlamasına yardımcı oluyor
    Tao’nun Polymath projesi konuşmasında gösterdiği gibi, onun her zaman matematik araştırması için yeni yöntemler arayan biri olduğu ortaya çıkıyor

  • Şimdilik bu, Tao ya da Scholze gibi Fields madalyalıların kanıta 10 kat zaman ayırabilecekleri durumda mümkün olan bir proje olabilir
    Yakın zamanda en üst düzey matematik bölümlerinden bir doktora sonrası araştırmacıyla konuştum; çevresinde gerçek çalışmalarda lean4 kullanan kimsenin olmadığını söyledi
    Kariyerinin başındaki bir araştırmacı için sezgisine güvenip makale yayımlamak muhtemelen daha iyi olur

    • Matematik profesörüyüm ve Lean kullanan ya da ona katkı veren pek çok kişi tanıyorum. Hepsi Fields madalyalı değil
      Bu konuyu doğru görmek için birkaç kişinin izlenimi yeterli değil
    • Matematiğin içinde de alana göre büyük farklılıklar olacaktır. Matematiksel mantık ya da cebir zaten biçimsel üslubu güçlü alanlar olduğu için kanıtları Lean’e aktarmanın yükü görece daha küçük
      Buna karşılık düşük boyutlu topoloji gibi daha sezgisel üsluba sahip alanlarda kanıt denetleyicisi kullananların daha az olacağını tahmin ediyorum
      Burada sezgisel demek daha az titiz demek değil. Belirli bir homotopi denkliğine dair görsel bir kanıtı Lean’in anlayabileceği hale getirmek, eşitsizlikler listesinden çok daha zor
      Bu arada geometri/topoloji tarafındayım; henüz bu tür araçları kullanan birini görmedim ya da duymadım
    • Tao’nun bir kanıta 10 kat zaman harcaması, yine de ortalama bir doktora sonrası araştırmacıdan 5 kat daha az zaman harcaması anlamına gelebilir. İnanılmaz derecede hızlı ve üretken biri
    • lean4 hem bir programlama dili hem de bir teorem kanıtlayıcıdır
      https://lean-lang.org/
      https://github.com/leanprover/lean4

  • “Yapay zeka anlaşılması imkânsız ve çirkin bir kanıt sunarsa, bunu alıp analiz edebiliriz. Bu kanıt tek bir sonuca ulaşmak için 10 varsayım kullanıyorsa, varsayımlardan birini silsek kanıt hâlâ çalışır mı? Bu tür bir bilim, henüz çok fazla yapay zeka üretimi kanıt olmadığı için mevcut değil; ama yapay zeka üretimi matematiği alıp daha anlaşılır hâle getiren yeni bir matematikçi türü ortaya çıkacak” kısmı, kodun açık API tasarımı hakkındaki düşüncelerimle tamamen aynı
    Geleneksel olarak yalnızca deneyimli geliştiricilerin üstlendiği rol artık büyük ölçüde basitleşip herkes için erişilebilir hâle gelebilir