Terence Tao'nun hoşuna gitti! ChatGPT otomatik olarak büyük bir buluş olduğunu kanıtlıyor ve AI 10 yıl içinde matematik dünyasına hakim olacak

**Kaynak:**Xinzhiyuan

**Kılavuz:**Pek çok kişi bunu kabul etmek istemese de, yapay zekanın on yıl içinde insan matematikçileri geçmesi çok muhtemeldir.

Birkaç gün önce Caltech ve MIT araştırmacılarının matematik teoremlerini kanıtlamak için ChatGPT'yi kullanan bir makalesi patladı ve matematik çevresinde büyük ilgi gördü.

Nvidia'nın baş bilim adamı Jim Fan, AI matematiği Copilot'un geldiğini ve yeni teoremleri keşfeden bir sonraki kişinin tam otomatik bir AI matematikçisi olacağını söyleyerek heyecanla iletti!

New York Times ayrıca yakın zamanda matematikçilerin hazır olduğunu ve yapay zekanın on yıl içinde en iyi insan matematikçileri yakalayacağını, hatta geride bırakacağını söyleyen bir makale yayınladı.

Ve Tao Zhexuan'ın kendisi bu makaleyi yeniden yayınladı.

Siobhan Roberts, bu yıl Machine Assisted Proofs tarafından düzenlenen IPAM çalıştayına katıldı ve ardından kendi deneyimlerine ve röportajlarına dayanarak yapay zeka ve matematik üzerine bu makaleyi yazdı.

**Yapay zeka da matematik dünyasını alt üst etmeye geliyor! **

Bugün, matematikçiler en son devrim niteliğindeki güç olan AI ile yüzleşmek zorunda.

2019'da, eski bir Google çalışanı olan ve şu anda bir Bay Area girişiminde çalışan bilgisayar bilimcisi Christian Szegedy, bilgisayar sistemlerinin on yıl içinde en iyi insan matematikçilerin problem çözme yetenekleriyle eşleşeceğini veya onları aşacağını tahmin etti. Geçen yıl hedef tarihini 2026 olarak revize etti.

Carnegie Mellon Üniversitesi mantıkçısı Jeremy Avigad (mavili) Örgün Matematik Yaz Okulu'ndaki öğrencilerle birlikte

2018 Fields Madalyası sahibi ve Princeton'daki Institute for Advanced Study'de matematikçi olan Akshay Venkatesh, şu anda AI kullanmakla ilgilenmiyor, ancak AI ile ilgili konuları tartışmaya çok hevesli.

Geçen yıl bir röportajda Venkatesh, "Öğrencilerimin bu alanın çok değişeceğini fark etmelerini istiyorum" dedi.

Ve son zamanlarda tavrı şuydu: "Yapay zekanın insanın anlayışına yardımcı olmak için kasıtlı, hatta kasıtlı kullanımına hiçbir itirazım yok. Ancak onu kullanma şeklimiz konusunda dikkatli ve dikkatli olmamız gerektiğine kesinlikle inanıyorum."

Bu yılın Şubat ayında, UCLA'daki Teorik ve Uygulamalı Matematik Enstitüsü "Makine Destekli İspatlar" konulu bir çalıştay düzenledi.

Seminerin ana organizatörü, 2006'da Fields Madalyası kazanan ve UCLA'da çalışan bir matematikçi olan Tao Terence'dir.

Matematiksel kanıtlara yardımcı olmak için AI kullanımının aslında dikkate değer bir fenomen olduğuna dikkat çekti.

Matematikçiler, ister matematiksel estetiğin yapay zeka tarafından yok edilmesi, ister matematikçilerin kendilerine yönelik bir tehdit olsun, yapay zekanın potansiyel tehdidi konusunda ancak son yıllarda endişelenmeye başladılar.

Ve seçkin topluluk üyeleri bu sorunları masaya yatırıyor ve "tabuyu nasıl yıkacaklarını" keşfetmeye başlıyor.

Yaz okulunun organizatörleri, soldan sağa: Avigad, Patrick Massot ve Heather Macbeth

Öklid geometrisi ilkellerinden bilgisayar koduna

Binlerce yıldır matematikçiler mantık ve muhakemedeki en son gelişmelere uyum sağladılar. Ama yapay zeka için hazırlar mı?

17. yüzyıl Yunan matematikçisi Öklid'in Los Angeles'taki Getty Müzesi'ndeki portresi: paçavralar içinde ve geometri üzerine incelemesini elinde tutuyor, Elements

2000 yılı aşkın bir süredir Öklid'in metni, matematiksel argüman ve muhakeme için bir paradigma olmuştur.

Carnegie Mellon Üniversitesi mantıkçısı Jeremy Avigad, Öklid'in zamanının matematiğini üzerine inşa etmek için neredeyse şiirsel bir "tanım" ile başladığını söylüyor - her biri birbirini izleyen temel kavramları, tanımları ve önceki teoremleri kullanarak. şeyleri kanıtlamak gibi bir yol.

Bazıları Öklid'in bazı "bariz" adımlarının çok açık olmadığından şikayet etti, ancak Dr. Avigad sistemin çalıştığını söyledi.

Ancak 20. yüzyıldan sonra, matematikçiler artık matematiği bu sezgisel geometrik temele dayandırmaya istekli değillerdi.

Bunun yerine kesin sembolik temsiller ve mekanik kurallar içeren biçimsel sistemler geliştirdiler.

Sonunda, böyle bir sistem altında, matematik bilgisayar koduna çevrilebilir.

1976'da dört renk teoremi, kaba kuvvet hesaplamaları yardımıyla ispatlanan ilk büyük teorem oldu.

Dört renk teoremi: Dört renk, bir haritayı iki bitişik bölge aynı renge sahip olmayacak şekilde doldurmak için yeterlidir.

Şikayet Eden Yapay Zeka: Üzgünüm, teoreminizi anlayamıyorum

Proof Assistant veya Interactive Theorem Prover adında böyle bir matematik aracı var.

Matematikçiler adım adım kanıtları koda dönüştürür ve ardından akıl yürütmenin doğru olup olmadığını kontrol etmek için yazılım programları kullanır.

Doğrulama süreci, başkaları tarafından kullanılabilen dinamik bir belirtim referans kitaplığında toplanır.

Hoskinson Resmi Matematik Merkezi'nin müdürü Dr.

Açık kaynaklı bir prova asistan sistemi olan Lean, geçtiğimiz günlerde bir kez daha ilgi gördü.

Yalın, şu anki Amazon bilgisayar bilimcisi Leonardo de Moura tarafından Microsoft'tayken geliştirildi.

Yalın, mantıktan ilham alan sembolik bir yapay zeka olan eski tarz yapay zeka GOFAI tarafından desteklenen otomatik akıl yürütmeyi kullanır.

Şimdiye kadar Lean, bir küreyi içten dışa çeviren ilginç bir teoremin yanı sıra şemaları matematiksel küre boyunca birleştiren bir anahtar teoremi doğruladı.

Bununla birlikte, ispat asistanının da eksiklikleri vardır: genellikle matematikçi tarafından girilen tanımları, aksiyomları veya muhakeme adımlarını anlamadığından şikayet eder, bu nedenle "ispat şikayetçisi" olarak da adlandırılır.

Fordham Üniversitesi'nden bir matematikçi olan Heather Macbeth, bu şikayetlerin araştırmayı külfetli hale getireceğini, ancak satır satır geri bildirim sağlayan işlevsellik türünün aynı zamanda sistemi öğretim için yararlı hale getireceğini söylüyor.

Bu bahar, Dr. Macbeth "iki dilli" bir kurs tasarladı, tahtadaki her sorunu ders notlarındaki Yalın koda çevirdi ve öğrencilerin çözümleri Yalın ve doğal dilde sunmaları gerekiyor.

Macbeth, "Onlara güven verdi," dedi, çünkü kanıtın ne zaman tamamlandığı ve yoldaki her adımın doğru mu yanlış mı olduğu konusunda anında geri bildirim alacaklardı.

Johns Hopkins Üniversitesi'nden matematikçi Emily Riehl, bir atölye çalışmasına katıldıktan sonra bir deneme yaptı.

Johns Hopkins Üniversitesi'nde matematikçi olan Emily Riehl, deneysel bir ispat asistanı kullanıyor.

Daha önce yayınlanan makalelerinde teoremleri ispatlamak için bir ispat yardımcısı uygulaması kullandı.

Kullandıktan sonra şok oldu. "Artık ispat sürecini her zamankinden çok daha derin anlıyorum. Düşüncem o kadar net ki, onu en aptal bilgisayara bile açıklayabilirim."

Matematiksel Örgünleştirme Yaz Okulu'nda öğrencilerin katıldığı bir grup projesi

**Şiddetli akıl yürütme - bu "matematiksel" değildir **

Bilgisayar bilimcilerin bazı matematik problemlerini çözmek için sıklıkla kullandıkları başka bir araca "şiddetli akıl yürütme" adı verilir, ancak matematik topluluğu genellikle bu yöntemle alay eder.

Bununla birlikte, AI bilim adamları, matematikçilerin fikirlerini pek umursamıyor gibi görünüyor ve matematiğin "dağlık alanlarını" yakalamak için kendi tanıdık yöntemlerini kullanmaya devam ediyor.

Carnegie Mellon Üniversitesi'nde bilgisayar bilimcisi olan Heule, 2016 yılında "Boole Pisagor üçlü problemini" çözmek için 200T "SAT çözücü" dosyası kullandı.

"Nature" dergisi yazıda şunları söyledi: 200T'nin ispatı tarihteki en büyük ispat işlemidir.Bu araçları problem çözmek için kullanmak gerçekten matematik midir?

Ancak, sorunun kendisinin çözülmesiyle ilgili makalenin yazarı olan bilgisayar bilimcisi Heule'ye göre, "bu yaklaşım, insan yeteneklerinin kapsamı dışındaki sorunları çözmek için gereklidir."

Benzer şekilde, bir satranç oyununda (AlphaZero) insanları yendikten sonra, DeepMind protein katlanmasını (AlphaFold) çözmek için makine öğrenimi algoritmaları tasarladı.

DeepMind, bu sonuçlara ulaşma yolunun, matematiği ilerletmek için insan sezgisini yönlendirmek için yapay zekayı kullanmak olduğunu savunan bir makale yayınladı.

Şu anda Körfez Bölgesi'nde bir iş kuran eski bir Google bilgisayar bilimcisi olan Yuhuai Wu, işinin yönünün matematik problemlerini çözmek için makine öğrenimini kullanmak olduğunu söyledi.

Şu anki projesi Minerva, matematiksel modelleri çözmek için ince ayarlanmış büyük bir dil modelidir.

Gelecekte, projenin genel araştırma görevlisi olarak "matematik problemlerini bağımsız olarak çözebilen" bir "otomatik matematikçiye" dönüşeceğini umuyor.

Matematik bir turnusol kağıdıdır

Öte yandan, AI teknolojisi ile derinlemesine temas halinde olan birçok matematikçi, AI'nın matematiksel araştırmalarda ciddiye alınmadığına dair endişelerini de dile getirdi.

Yapay zeka teknolojisinin, matematikçilerin istedikleri yanıtları "bulmalarına" genellikle "doğrudan" yardımcı olabileceğine inanıyorlar.

Matematikçiler veya yapay zeka uzmanları, yapay zekanın bu yanıtı nasıl bulduğuna dair hiçbir fikre sahip olmasa da.

DeepMind ile çalışmış bir matematikçi olan Geordie Williamson, bir zamanlar DeepMind ile çalışma deneyimini paylaştı.

DeepMind ile yaptığı iş birliği sürecinde, DeepMind tarafından keşfedilen bir sinir ağı, kendisinin çok önemli olduğunu düşündüğü veri değerini tahmin edebilmektedir ve bu son derece doğrudur.

Yapay zekanın bunu nasıl yaptığını anlamak için gerçekten çok uğraşıyor çünkü bu bir teoremin temeli olabilir.

Ama sonunda yapay zekanın mantığını hala anlayamadı ve DeepMind'daki insanlar da bunu yapamadı.

Öklid gibi, sinir ağları bir şekilde gerçeği bulur, ancak mantıksal nedenleri kavramak zordur.

Öte yandan, matematikçinin bakış açısından çıkarım, matematiğin özüdür, ancak makine öğrenimindeki yapbozun eksik bir parçasıdır.

Teknoloji dünyasında, çoğu zaman bir soruna çözüm sağlayacak bir kara kutu olsaydı, teknoloji dünyası son derece memnun olurdu.

AI böyle bir kara kutu.

Ancak matematikçiler bu durumdan memnun değiller.

Matematikçiye göre, sinir ağlarının nasıl çalıştığını anlamaya çalışmak büyüleyici matematiksel soruları gündeme getiriyor.

Ve bu problemleri çözmek, matematikçilerin "dünyaya anlamlı katkılar yapmalarını" sağlayacaktır.

Yapay zeka matematiksel teoremleri kanıtlayabilirse

Dünya yapay zeka tarafından üretilen hipotezlerle dolup taşsaydı ne yapardık?

Netizenler buna ruh işkencesi gönderdi ve ilk adım olarak AI sisteminin yeni hipotezi/formülü hakkında şüphelerim var çünkü DeepMind bunu zaten düğüm teorisinde yaptı.

Topluluğun, yapay zekanın ürettiği yeni varsayımlar seline nasıl tepki vereceğini merak ediyorum. Bir yapay zeka tarafından yaratılan mantıksal bir argümanı kontrol etmek başka bir şey, milyonlarca "ah, bu doğru olabilir" önerisine boğulmak başka bir şey. Mevcut inceleme ve yayın sistemlerimizin buna hazır olduğunu düşünmüyorum.

Bu, insanların matematiğe olan güvenini nasıl etkiler?

Makinelerin yakın zamanda matematik yapamayacağı iddia edildi, ancak makine öğrenimi modelleri ve hesaplama gücünün biyoloji alanını değiştirdiği gibi, araştırmanın yapılma şeklini değiştirdiği görülebilir.

Bazı netizenler, AlphaDev'den beri bu sorunu düşündüğümü, ancak aynı programın sıralama algoritmaları oluşturabileceğini ve ayrıca matematik teoremlerini kanıtlamak için otomatik kanıt denetleyicileri kullanabileceğini söyledi. Asıl soru, önemsiz bir keşfi değil, önemli bir şeyi kanıtlamak için kullanılıp kullanılamayacağıdır.

Bununla birlikte, bazı netizenler, GPT benzeri araçların değerli gerçekleri gerçekten keşfedip keşfedemeyeceği konusunda hala şüpheci.

Bazı netizenler ayrıca insanlarla yapay zeka arasında matematiği anlama ve dikkat etme konusunda bir fark olabileceğine dikkat çekti.Yapay zeka neyin doğru olduğunu kanıtlarken, insanlar her zaman neden doğru olduğuna odaklanır.

Referanslar: