DeepMind'in yapay zekası, Uluslararası Matematik Olimpiyatı sorularını gümüş madalya düzeyinde çözdü

(deepmind.google)

3 puan yazan GN⁺ 2024-07-26 | 3 yorum | WhatsApp'ta paylaş

Zor matematiksel akıl yürütmenin başlıca sınavlarından biri olan IMO 2024'te Google DeepMind'in AlphaProof ve AlphaGeometry 2 sistemleri 6 sorudan 4'ünü çözerek bir yapay zekanın ilk kez gümüş madalya bandında bir sonuca ulaşmasını sağladı
Toplam 42 puan üzerinden 28 puan aldı; çözdüğü soruların tamamı tam puan sayıldı ve 2024 altın madalya barajı olan 29 puanın yalnızca 1 puan gerisinde kaldı
Değerlendirme IMO puanlama kurallarına göre matematikçiler tarafından yapıldı; cebir ve sayı teorisi sorularını AlphaProof, geometriyi ise AlphaGeometry 2 üstlenerek farklı akıl yürütme biçimlerini birleştirdi
Sorular önce elle biçimsel matematik diline çevrildi; öğrenciler yarışmada 4,5 saatlik iki oturumda çözüm üretirken sistem bir soruyu birkaç dakikada, diğerlerini ise en fazla 3 günde tamamladı
Bu sonuç, matematik yapay zekasının basit hesaplamanın ötesine geçerek ispat arama ve doğrulamaya yaklaştığını gösteriyor; ancak biçimselleştirilmiş girdi ve uzun çözüm süresi hâlâ önemli kısıtlar olarak duruyor

IMO 2024'te elde edilen gümüş madalya düzeyindeki sonuç

Google DeepMind, matematiksel akıl yürütme sistemi AlphaProof ile geometri problem çözme sisteminin geliştirilmiş sürümü AlphaGeometry 2'yi tanıttı
İki sistem, 2024 Uluslararası Matematik Olimpiyatı'ndaki 6 sorudan 4'ünü çözdü
- AlphaProof: 2 cebir sorusu, 1 sayı teorisi sorusu çözdü
- AlphaGeometry 2: 1 geometri sorusunu ispatladı
- 2 kombinatorik sorusu çözülemedi
Her soru 7 puan değerinde ve toplam puan 42
- Sistem, çözdüğü 4 sorunun tamamında tam puan alarak 28 puan elde etti
- Bu, 2024 IMO gümüş madalya bandının üst kısmına karşılık geliyor
- 2024 altın madalya barajı 29 puandı ve resmi yarışmada 609 katılımcıdan 58'i altın madalya bandına ulaştı
Bu, bir yapay zeka sisteminin IMO'da gümüş madalyalı düzeyine denk gelen bir sonuç aldığı ilk örnek oldu

Değerlendirme yöntemi ve çözüm koşulları

Sorular için IMO organizatörlerinin sağladığı yarışma problemleri kullanıldı
Yanıtlar, IMO'nun puan verme kurallarına göre değerlendirildi
- Değerlendiriciler, IMO altın madalyalısı ve Fields Madalyası sahibi Prof Sir Timothy Gowers ile iki kez IMO altın madalyası kazanmış ve IMO 2024 Problem Selection Committee başkanı olan Dr Joseph Myers'tı
Sistemin soruları anlayabilmesi için tüm sorular önce elle biçimsel matematik diline çevrildi
Resmi yarışmada öğrenciler çözümlerini 4,5 saatlik iki oturum boyunca teslim ediyor
- Yapay zeka sistemi bir soruyu birkaç dakika içinde çözerken diğer sorular için en fazla 3 gün harcadı
AlphaProof'un çözdüğü sorular arasında, IMO 2024'te yalnızca 5 katılımcının çözebildiği en zor soru da vardı

AlphaProof: Lean tabanlı biçimsel akıl yürütme

AlphaProof, matematiksel önermeleri Lean biçimsel dilinde ispatlamayı öğrenen bir sistem
Ön eğitimli bir dil modeli ile AlphaZero pekiştirmeli öğrenme algoritmasını birleştiriyor
- AlphaZero, satranç, shogi ve Go'yu kendi kendine öğrenmek için kullanılan algoritma
Biçimsel dil kullanıldığında, matematiksel akıl yürütme içeren ispatların doğruluk doğrulaması yapılabiliyor
Daha önce insan eliyle yazılmış biçimsel ispat verisi çok az olduğundan, makine öğrenmesinde biçimsel dil kullanımı sınırlıydı
Doğal dil tabanlı yaklaşımlar çok daha fazla veri kullanabiliyor, ancak ikna edici görünen fakat yanlış ara akıl yürütme adımları ya da çözümler üretebiliyor
DeepMind, Gemini modelini ince ayar yaparak doğal dil problemlerini otomatik olarak biçimsel önermelere çevirecek hale getirdi ve farklı zorluk seviyelerinde bir biçimsel problem kütüphanesi oluşturdu
AlphaProof, bir problem verildiğinde önce çözüm adayları üretiyor, ardından Lean içinde olası ispat adımlarını arayarak bunları ispatlıyor ya da çürütüyor
- Bulunan ve doğrulanan ispatlar, AlphaProof'un dil modelini güçlendirmek için kullanılıyor
- Bu yinelemeli süreç, daha zor problemleri çözme yeteneğini artırmak için kullanılıyor
IMO hazırlık sürecinde sistem, haftalar boyunca milyonlarca problemi ispatlayarak ya da çürüterek eğitim gördü
- Yarışma sırasında da, problemlerin kendi ürettiği varyantları üzerindeki ispatları güçlendirirken tam çözüm arayan bir öğrenme döngüsü uygulandı

AlphaGeometry 2: daha zor geometri problemlerine genişleme

AlphaGeometry 2, önceki AlphaGeometry'nin büyük ölçüde geliştirilmiş bir sürümü
Bu sistem, sinir ağları ile sembolik akıl yürütmeyi birleştiren nöro-sembolik hibrit bir yapıya sahip
- Dil modeli Gemini tabanlı
- Önceki sürüme göre bir mertebe daha fazla sentetik veriyle sıfırdan eğitildi
Daha fazla veri ve iyileştirilmiş model sayesinde, cisim hareketi ile açı, oran ve uzaklık denklemlerini içeren daha zor geometri problemleri ele alınabiliyor
AlphaGeometry 2'nin sembolik motoru, önceki sürüme göre iki basamaklı katlar kadar daha hızlı
Yeni bir problem geldiğinde, yeni bilgi paylaşım mekanizması sayesinde farklı arama ağaçlarının üst düzey kombinasyonlarını kullanarak daha karmaşık problemleri işleyebiliyor
Son 25 yıldaki IMO geometri sorularında çözüm oranı: {b:83,53}
- 2024 yarışması öncesi ölçümlere göre AlphaGeometry 2, son 25 yıldaki IMO geometri sorularının %83'ünü çözebiliyordu
- Önceki AlphaGeometry'nin çözüm oranı ise %53'tü
IMO 2024'te Problem 4, biçimselleştirilmiş girdi sonrasında 19 saniye içinde çözüldü

Doğal dilde akıl yürütme ve gelecekteki kullanım

DeepMind, IMO çalışmasının bir parçası olarak Gemini ve en güncel araştırmalara dayanan bir doğal dilde akıl yürütme sistemini de denedi
Bu sistem, problemi biçimsel dile çevirmeyi gerektirmiyor ve başka yapay zeka sistemleriyle birleştirilebiliyor
Bu yaklaşım 2024 IMO sorularında da test edildi ve sonuçlar umut verici olarak değerlendirildi
AlphaProof'un daha teknik metodolojisi bir Nature makalesi ile yayımlandı
DeepMind, matematikçilerin yapay zeka araçlarıyla birlikte hipotezleri keşfettiği, eski problemlere yeni yaklaşımlar denediği ve ispatların zaman alan unsurlarını hızla tamamladığı bir geleceği hedefliyor

3 yorum

chabulhwi 2024-07-26

Biçimsel matematik kütüphanesinin geliştirilmesine katkıda bulunan matematikçilerin sayısı arttıkça, performansı yüksek matematik yapay zekası geliştirmek de kolaylaşacaktır. Bildiğim kadarıyla, kendi başına Lean kanıt yardımcısının diliyle biçimselleştirdiği matematik kuramlarını Lean’in matematik kütüphanesi Mathlib’e aktaran Koreli şu anda 3 kişi var.

Ben geçen yıl Mathlib’in Lean 3’ten Lean 4’e taşınması çalışmalarına biraz katkıda bulundum ve bu yıl da Lean 4 Batteries kütüphanesindeki çözülmemiş bir teoremden birini kanıtladım.

GN⁺ 2024-07-26

Hacker News yorumları

Bu duyuru beni gerçekten heyecanlandırıyor; ancak “önce problemleri sistemin anlayabileceği biçimsel matematik diline insanlar elle çevirdi” cümlesinin ne kadar işi üstlendiği belirsiz.
Geometri olmayan problemlerin hepsi “... olan tüm X’leri bulun” biçimindeydi; teorem ifadeleri de “tüm X’lerin kümesinin {foo} olduğunu gösterin” biçimindeydi.
https://storage.googleapis.com/deepmind-media/DeepMind.com/B... adresindeki indirilebilir çözümlere bakınca, çeviri aşamasında {foo}’yu insanın mı belirlediğini yoksa bilgisayarın mı bulduğunu anlamak zor. Bilgisayarın bulduğuna inanmak istiyorum ama bunu doğrulayacak bir dayanak bulamadım.
- Cevabı bilgisayarın kendisi buldu. Yani P1’de çift tam sayıları, P2’de {1,1}’i, P6’da 2’yi buldu ve her durumda buna eşlik eden bir Lean kanıtı da sundu.
- Genel olarak söylemek gerekirse, o çeviri aşaması kanıt aşamasından çok daha kolay. Otomatik çevirideki sorun, çeviri sonucunun yanlış olabilmesi.
  İnsanlar da biçimsel yöntemlerle doğrudan uğraşırken bunun sıkça yaşandığını görüyor; bu yüzden araştırmacılar, LLM ya da başka araçlar olsun, sonunda tüm çevirileri denetlemeleri gerektiğine karar vermiş olmalı.
- Bağlantı verilen sayfada “problem ifadeleri insanlar tarafından Lean’de biçimselleştirildi, ancak problem ifadesinin içindeki cevap ajan tarafından üretildi ve biçimselleştirildi” deniyor.
  Ancak bu aşamanın mümkün olması için ajana başlangıçta nasıl bir biçim verildiği belirsiz.
- Eğitim verisi üretmek için kullanılan bir biçimselleştirme aracı var; burada kullanılmamış olması ilginç. Demek ki henüz yeterince güvenilir değildi.
- Açıklama kulağa şöyle geliyor: “Bir problem verildiğinde AlphaProof bir çözüm adayı üretir, ardından Lean’de olası kanıt adımlarını arayarak bunu kanıtlar ya da çürütür.”
  Yani AlphaProof ne tür bir “problem” alıyor olursa olsun ve “... olan tüm X’leri bulun” ifadesi nasıl biçimselleştirilmiş olursa olsun, aday teoremleri muhtemelen Lean’de üretiyor. Örneğin kümenin, belirli bir P formülü için {n: P(n)} biçiminde olması gibi. Sonra kanıt aramasına geçiyor.
  Eğer {foo}’yu AlphaProof bulmadı da ona verildiyse, problemi çözdüğünü iddia etmek epey saçma olurdu. Yine de bu sonuç beni çok heyecanlandırıyor.
Kesinlikle etkileyici, ama IMO’dan söz edilirken bir uyarı gerekiyor. Madalyalar katılımcıların, yani lise öğrencilerinin %50’sine veriliyor ve altın-gümüş-bronz oranı 1:2:3 olduğundan altın ve gümüş madalya alanlar tüm katılımcıların ilk %25’ine giriyor.
Dolayısıyla ifade “yapay zeka IMO problemlerini öğrencilerin %75’inden daha iyi çözdü” oluyor; aslında bu bile daha etkileyici olabilir.
Ama “bir problem birkaç dakika, diğer problemlerin her biri en fazla 3 gün” koşulu, öğrencilerin sahip olduğu 9 saatten farklı olduğu için gerçek bir karşılaştırma sayılmaz. Öğrencilere de 9 saat yerine 15 güne kadar süre verilseydi, bu skora ulaşan ya da onu aşan daha fazla kişi olurdu.
Gerçekte yapay zeka, öğrencilere verilen 9 saat içinde yalnızca bir problem çözmüş sayılır; dolayısıyla madalya düzeyinden oldukça uzak kalmış olması muhtemel. Bu kadar etkileyici bir sonucu neden özellikle elmayla armudu karşılaştırarak bulanıklaştırmak gereksin ki?
Daha nesnel olarak, daha uzun sürdüğü ama problemlerin %X’ini çözdüğü ya da N puan üzerinden X puan aldığı bildirilebilir.
- IMO katılımcılarıyla tanışmışlığım var; gerçekten akıl almaz derecede zekiler. Böyle bir toplulukla karşılaşmadan önce insanların o kadar zeki olabileceğini hayal edemezdim. Bu yüzden onları, tüm lise öğrencilerinin %0,01’lik kesiminin de üst %25’ine yakın görmek gerekir.
  Burada zaman pek ilginç bir eksen değil. Çünkü insanlar dev bir GPU kümesine denk CPU’lar kullanmıyor. “Yeterli kaynak verildiğinde çözüme ulaşabiliyor mu?” ikili sorusu daha ilginç; GPT/Claude için yanıt açıkça hayırdı.
- “Katılımcı lise öğrencilerinin %50’sine madalya veriliyor” ifadesi kafa karıştırabilir; burada kastedilen lise öğrencileri sıradan lise öğrencilerinden oluşan bir örneklem değil. Bildiğim kadarıyla her ülkeden olimpiyat problemi çözmede en güçlü yaklaşık 6 kişiden oluşan milli takımlar.
- Kişisel görüşüm, Google’ın pozisyonu değil ama, bu yıl altın madalya alamamalarının tek nedeni problem seçiminde şanssız olmaları ve P3/P5’te kısmi puan hedeflememeleriydi.
  Baraja çok yakındılar ve genelde küçük bir ilerleme bile 1 puan getirebilir. Ancak teknik nedenlerle altın madalya aldıkları şeklinde haberler iyi görünmezdi; bu yüzden tartışmasız bir gümüşle yetinmiş gibiler.
- İnsanlara daha fazla süre vermek ile bir bilgisayar programına daha fazla süre vermek arasındaki temel fark, tarihsel olarak ikincisini daha hızlı çalıştırma konusunda çok daha başarılı olmuş olmamız.
- DeepMind araştırmalarının çoğu şirket açısından bir maliyet merkezi. Bu tür basın bültenleri, yatırımcılara ve kamuoyuna sürekli yatırımı gerekçelendirmeye yardımcı oluyor.
Bu gerçekten önemli. AlphaGeometry, çok fazla kaba kuvvet aramasıyla çok sınırlı bir problem kümesini çözmüştü.
Bu seferki yöntem çok daha geniş; matematik yapma biçimini ciddi biçimde etkileyeceğini düşünüyorum. Doğal dilli matematikten biçimselleştirilmiş matematiğe uzanıyor ve orada hem biçimselleştirmeyi hem de kanıtı eğitebilen, kendi kendini besleyen bir hattı gerçekten hayata geçiriyor.
İlke olarak bu hat, yardımcı tanımlar ve lemmalar üretmek gibi temel teori inşasını da öğrenebilir. Kanıt asistanlarının kutsal kâsesine yakın; doğal biçimde ürettiğimiz matematiğin büyük kısmını biçimselleştirmemizi sağlayacağını düşünüyorum. İnsanlar sonradan titizleştirme yöntemiyle çalışacak, ayrıntıları doldurma işinde ise makineler yardımcı olacak.
- Katılıyorum. Büyük bir ilerleme. Geometri problemleri, polinom denklem sistemlerine çevrilip iyi bilinen bilgisayar cebiri algoritmalarıyla çözülebildiği için başka bir kategoriye giriyor.
  Buna karşılık bu tür açık uçlu biçimselleştirme, ilerlemenin çok yavaş ve kademeli olduğu bir alandı. 5 yıl önce komşu bir alanda çalışıyordum; bu sonucun geleneksel otomatik akıl yürütme teknikleriyle ulaşılması imkânsız bir seviye olduğu söylenebilir.
  Gerçek otomatik teorem ispatı, saf matematikten çok daha geniş bir alanda faydalı olur. Örneğin küçük bir programlama dilinin aksiyomatik semantiğini Lean’de yazıp “bu belirtimi karşılayan bir programın var olduğunu göster” gibi sorular sorabilirsiniz.
  Bu yaklaşım ölçeklenirse, son birkaç yılda çıkan herhangi bir makine öğrenimi uygulamasından daha önemli hale gelecek.
- Aramayı küçümsememek gerek. Kaba kuvvet gibi görünebilir ama arama, Go’da insan seviyesini geçti ve IMO’da gümüş madalya seviyesine kadar geldi.
  Bizi ortaya çıkaran evrim de muazzam sayıda kaba kuvvet denemesiyle işleyen bir aramadır; bilimsel yöntemdeki araştırma da özünde aramadır.
- Bu alanda çalışan insanlar zaten var.
  https://leandojo.org/
  https://machine-learning-for-theorem-proving.github.io/
  https://www.youtube.com/watch?v=P5ew0BrRm_I
  https://paperswithcode.com/task/automated-theorem-proving
  https://old.reddit.com/r/math/comments/11mb9lx/future_of_aut...
  https://github.com/RiccardoBiosas/LeanGPT
- Bu tür sistemler matematik araştırmasının dışında çok daha faydalı olacak gibi.
  Faydalı işler yapmak için çok zor problemler kanıtlamaya gerek yok. Çoğu zaman basit şeyleri kanıtlamak yeterli. Bir dil modeline iş tamamlama, maddeleri düzenleme, takvim ayarlama, X’i yapan kod yazma vb. görevler verdiğinizde sonuca hemen güvenmek zor; ama sistem problemin bir kısmını mantığa çevirebilir ve çözüm bulabilirse çok daha güvenilir hale gelir.
- Hayır. Bu, çözüm bulmak için arama motoru kullanabilmesini sağlamaya benziyor; daha fazlası değil.
Asıl nokta biraz arka planda kalmış: Lean kullanıyorlar.
Bu, matematik problemlerinin ötesinde önemli. Bir makine öğrenimi modelini kanıt sistemiyle boğuşturmak, genel saçmalamalardan kaçınmanın iyi bir yolu.
Umarım ileride daha fazla kişi Lean veya benzeri sistemlerde tipler yazarak bunu prompt yazmanın çok daha iyi bir yolu olarak kullanır.
- AlphaProof kesinlikle etkileyici ama IMO’da bilgisayara, insanların sahip olmadığı avantajlar da veriyor. Kimse kafasının içinde Gröbner bazı oluşturamaz; oysa polyrith için sekiz karakter yazmak yetiyor. AlphaProof’un nlinarith kullandığını da gördüm.
- Şaşırtıcı. Tam “bunu Lean’e bağlasalar harika olur” diye yorum yazacaktım. İleri matematiğin bundan sonra bu yöne gitmesi gerekiyor gibi. Çünkü önemli kanıtlar o kadar karmaşık hale geldi ki neredeyse hiç kimse tüm parçaları baştan sona anlamıyor.
  1. https://lean-lang.org/
- Bununla Riemann hipotezini de hedeflerler artık, hehe.
Tim Gowers’ın temel uyarı noktalarını açıklayıp bağlama oturttuğu iyi ve kısa bir genel bakış var. Kendisi Fields madalyalı ve bu çalışmaya da katıldı: https://x.com/wtgowers/status/1816509803407040909
Doğru, ama her ülkenin milli takımına girmek başlı başına çok zorlu bir süreç. Bölgesel matematik olimpiyatları, ulusal matematik olimpiyatları vb. her aşamada acımasız bir eleme var.
Ardından bu seçkin grup için ek eğitim geliyor; bazı durumlarda ek seçmeler de olabiliyor.
Kısacası bir ülkenin IMO milli takımına seçilmek başlı başına büyük bir iş; bunun içinde altın ya da gümüş madalya almak ise tek kelimeyle muazzam bir başarı.
- Bazı ülkeler bu çocukları yıl boyunca okuldan alıp IMO eğitimine yoğunlaştırıyor ve kendi ülkelerindeki en iyi üniversitelere kabul garantisi bile verebiliyor.
  Kaynak: IMO gümüş madalyası kazanmış bir arkadaşım.
Bu işi yapıp para alan insanlara gerçekten imreniyorum. Çok eğlenceli görünüyor; bu şekilde en ileri düzeyi yukarı taşımak çok tatmin edici olsa gerek.
- Öyle olmayabilir de. Çok tatmin edici olması gereken işlerin fena halde sıkıcı, hatta zararlı bir yöne kaydığı çok oldu; tersine, dışarıdan sıradan görünen işlerin gerçekten ilginç çıktığı da oldu.
  İş tatmininde konudan çok çalışma ortamının daha önemli olduğunu düşünüyorum. Dünyayı değiştiren bir konu üzerinde çalışsanız bile ekip berbat durumdaysa zor zaman geçirirsiniz. Bazı insanların tüm eğlenceyi emip alma yeteneği vardır; şirket içi siyaset her yerdedir, özellikle de dünyayı değiştiren konularda daha da böyledir.
  Öte yandan müşteri verilerini veritabanına koymak gibi en sıkıcı görünen bir konuda bile, nazik bir ekip, iyi tasarlanmış bir mimari, deney ve bilgi paylaşımı için zaman varsa harika vakit geçirebilirsiniz. Sadece düzgün çalışan basit şeylerin güzelliğini giderek daha çok takdir eder oldum. Bunlar bilimsel atılımlardan bile daha nadir olabilir.
  Elbette harika bir çalışma ortamı ile harika bir konu birlikte de gelebilir; bu da jackpot’a yakın bir şeydir ve imrenmeye değer.
- Bu alanda, daha spesifik olarak LLM ön eğitimi tarafında çalışıyorum. Dışarıdan göründüğü kadar gösterişli değil. Devasa YAML dosyalarıyla uğraşmayı ve büyük ölçekte regex kullanmayı içeriyor. Tabii bu biraz basitleştirilmiş bir ifade.
  Böyle bir işi yapabildiğim için heyecanlı ve minnettar olmam gerekir ama kaba saba araçlar işin keyfinin büyük kısmını alıp götürüyor.
- Muhtemelen jealous değil envious demek gerekirdi.
- Yapabileceğimiz en iyi şey güncel gelişmeleri takip etmeye ve desteklemeye devam etmek.
- Şimdi K8s için 3.292.329 satırlık YML’yi yeniden yapılandırma zamanı değil mi?
  (/s)
Makinelerin insanlardan daha iyi satranç oynamasının üzerinden onlarca yıl geçti.
Yine de kimse umursamıyor. Herkes Magnus Carlsen’i izlemekle meşgul.
İnsan olduğumuz için diğer insanların yaptıklarıyla ilgileniyoruz. Makinelerle ise ancak bize faydaları olduğu ölçüde ilgileniyoruz.
Bu ilke iş ve sanata da geniş ölçüde uzanıyor. İnsan var olduğu sürece, bu alanlarda insanın yeri her zaman kalacak.
- Yapay zeka satrançta ve sanatta ne kadar daha iyi olursa olsun, insanlar bunlardan keyif almaya devam edecek. Benzer şekilde, matematiği hobi olarak çalışan insanlar da muhtemelen var olmaya devam edecek.
  Ancak yakın gelecekte yapay zekanın çoğunu ya da tamamını keşfetmediği yeni matematiksel ilerlemeler yayımlayan matematikçiler kalıp kalmayacağından ciddi şekilde şüpheliyim. İnsan ilk soruyu sorduğu için kanıtın takdirini alabilir, ama bilgisayar anlamlı matematik problemlerini kolayca çözebiliyorken insanların bunları daha yavaş ve daha pahalı şekilde çözmesinde ısrar edecek bir dünya pek yok.
- Doğru ama örneğin yapay zeka Goldbach varsayımını kanıtlarsa bu muazzam bir şey olur.
- Tüketici açısından bir et işleme tesisi ya da Amazon deposunun 5000 kişi mi yoksa 5 kişi mi çalıştırdığı fark etmez.
  Bu ilke sanata kesinlikle uygulanır, ama iş için yalnızca bazı ya da çoğu alanlarda geçerlidir.
- Matematiğin satrançtan veya sanattan farklı olarak gerçekten faydalı olduğuna inanan insanlar var. Çoğu matematikçi böyle düşünmez, ama bir anlığına bu çılgın fikri kabul edersek, kanıt yalnızca “bu matematik parçasını doğru uyguladın” diyen bir araçtır.
  O zaman kanıtı anlamaya gerek yoktur ve bir yerlerdeki bir matematikçinin o kanıtı tamamen anlayıp anlamadığını kimse umursamaz. Makinelerin kanıt bulma ve doğrulamada bizden daha iyi olması sorun değildir; hatta beklenebilir bir şey haline gelir.
- Bu ilkenin matematiksel kanıtlara pek uzanmadığını düşünüyorum. Bir kanıtı doğrulamak, onu oluşturmaktan çok ama çok daha kolaydır; ikinci kanıt ise yalnızca bir dipnot olur.
  Birçok matematikçinin böyle bir işe takılıp kalmak isteyeceğini sanmıyorum. Yine de IMO ile araştırma matematiğinin en ön cephesi arasında hâlâ büyük bir mesafe var.
Teorem kanıtlamanın, akıl almaz derecede büyük bir arama uzayına sahip tek oyunculu bir oyun olduğu için AGI’den çok önce çözüleceğini hep düşünmüştüm.
Bana göre AlphaProof’un en büyük katkıcıları Lean ve Mathlib’in arkasındaki insanlar; çünkü tüm matematiği biçimselleştirme gibi göz korkutucu bir işi üstlendiler.
Matematik makalelerindeki biçimselleştirme eksikliği, otomasyon girişimlerini sürekli öldürdü. Çünkü yapay zeka araştırmacıları, yazara özgü gösterim, örtük bilgi, atlanmış kanıt adımları gibi insani unsurlarla boğuşmak zorunda kaldı.
- “Teorem kanıtlama, çok büyük bir arama uzayına sahip tek oyunculu bir oyun olduğu için AGI’den çok önce çözülecek” demek kulağa tuhaf geliyor.
  AGI teriminin kendisinin tanımlı olmadığını düşünüyorum, ama neden “genel olarak zeki bir şey”, yani ortanca insan düzeyi zekâ yaratmanın, “matematikte Terrence Tao’dan daha iyi olmaktan” çok daha zor olmasının beklendiğini anlamıyorum.
- Tüm matematiği biçimselleştirmiş değiller. IMO için tüm matematiğe ihtiyaç olmaması neyse ki iyi bir şey. Ama IMO için yeterli olacak kadarını bile biçimselleştiremediler. Muhtemelen bu yüzden kombinatorik problemini çözememişlerdir.
En iyi tartışma burada: https://leanprover.zulipchat.com/#narrow/stream/219941-Machi...