Olimpiyat düzeyinde geometri yapay zeka sistemi AlphaGeometry

 (deepmind.google)
1 puan yazan GN⁺ 2024-01-18 | 1 yorum | WhatsApp'ta paylaş
  • Uluslararası Matematik Olimpiyatı, yapay zekanın matematiksel akıl yürütmesi için bir sınama alanı haline gelirken, AlphaGeometry geometri problemlerinden 30’un 25’ini süre sınırı içinde çözerek insan altın madalyalıların 25,9’luk ortalamasına yaklaştı
  • Temel unsur, sinir ağı dil modeli ile kural tabanlı sembolik çıkarım motorunun birleşimi; böylece sezgisel yapı önerileri ile biçimsel mantık doğrulaması tek bir döngü içinde işleniyor
  • İnsan gösterimleri olmadan oluşturulan 100 milyon benzersiz sentetik örnek, eğitim darboğazını azalttı; bunların 9 milyonu, ispat için gerekli yardımcı yapıları içeriyor
  • Tüm olimpiyat çözümleri bilgisayar tarafından doğrulandı ve Evan Chen, çıktının makine tarafından doğrulanabilir olmasının yanı sıra insanlar tarafından okunabildiğini ve öğrencilerin kullandığı klasik geometri kurallarını izlediğini söyledi
  • Bir IMO oturumunda genelde 6 sorudan yalnızca 2’si geometri olduğundan uygulama alanı sınırlı, ancak yalnızca geometri performansıyla bile 2000 ve 2015 IMO bronz madalya barajını aşabilen ilk yapay zeka modeli oldu

IMO geometri kıyaslama başarısı

  • Nature’da yayımlanan AlphaGeometry, karmaşık geometri problemlerini insan olimpiyat altın madalyalılarına yakın bir seviyede çözüyor
  • Kıyaslama seti, 2000’den 2022’ye kadar olimpiyatlardan seçilen IMO-AG-30 adlı 30 geometri probleminden oluşuyor
    • AlphaGeometry: süre sınırı içinde 25 problem çözdü
    • Önceki en iyi yaklaşım olan Wu’s method: 10 problem çözdü
    • İnsan altın madalyalıların ortalaması: 25,9 problem çözdü
  • Google DeepMind, AlphaGeometry kodunu ve modelini açık kaynak olarak yayımladı

Nöro-sembolik sistem mimarisi

  • AlphaGeometry bir nöro-sembolik sistem; sinir ağı dil modeli ile sembolik çıkarım motoru birlikte çalışarak karmaşık geometri teoremlerinin ispatını buluyor
  • Dil modeli, verideki genel örüntüleri ve ilişkileri hızla belirleyerek işe yarama olasılığı yüksek yapıları tahmin ediyor
    • Ancak katı akıl yürütme ya da kararları açıklama konusunda yetersiz kalabilir
  • Sembolik çıkarım motoru ise biçimsel mantık ve açık kuralları izleyerek sonuca ulaşıyor
    • Açıklanabilir ve tutarlı olsa da, büyük problemleri tek başına ele aldığında yavaş ve daha az esnek olabilir
  • Bu iki bileşen birlikte kullanıldığında, dil modeli yeni nokta, doğru ve çember gibi yardımcı yapıları öneriyor; çıkarım motoru da bunlara dayanarak şekil hakkında ek sonuçlar üretiyor

Yardımcı yapıları bulan çözüm döngüsü

  • Olimpiyat geometri problemleri çoğu zaman yalnızca verilen şekille doğrudan çözülemez; çözüm için yeni geometrik öğeler eklemek gerekebilir
  • AlphaGeometry’nin çözüm süreci, sembolik çıkarım ile dil modeli önerilerinin dönüşümlü çalıştığı bir yapı izliyor
    • Verilen şekil ve teoremin öncüllerinden sembolik çıkarım motoru yeni önermeler türetiyor
    • Çözüm bulunamazsa ya da artık yeni önerme üretilemezse, dil modeli faydalı olma ihtimali yüksek bir yardımcı yapıyı ekliyor
    • Eklenen yapı, çıkarım motoruna yeni bir yol açıyor ve çözüm bulunana kadar bu süreç tekrarlanıyor
  • 2015 Uluslararası Matematik Olimpiyatı 3. sorusunda AlphaGeometry’nin çözümü 109 mantıksal adımdan oluşuyordu

100 milyon sentetik veri üretimi

  • Geometri; uzam, mesafe, şekil ve göreli konum anlayışına dayanır ve sanat, mimarlık, mühendislik gibi birçok alanın temelini oluşturur
  • AlphaGeometry’nin sentetik veri üretim yöntemi, bir insanın şekle bakıp mevcut bilgisiyle yeni geometrik özellikler ve ilişkiler keşfetme sürecini büyük ölçekte taklit ediyor
  • Sistem, yüksek derecede paralelleştirilmiş hesaplama ile 1 milyar rastgele şekil üretiyor
    • Her şekil için nokta ve doğrular arasındaki tüm ilişkileri eksiksiz çıkarıyor
    • Her şeklin içerdiği tüm ispatları buluyor
    • Bu ispatlara ulaşmak için hangi ek yapıların gerektiğini geriye doğru izliyor
  • Bu süreç symbolic deduction and traceback olarak adlandırılıyor
  • Dev veri havuzu, benzer örnekleri dışlayacak şekilde filtreleniyor ve sonuçta zorluk seviyeleri farklı 100 milyon benzersiz eğitim örneği elde ediliyor
    • Bunların 9 milyonu, yardımcı yapı eklenmiş örneklerden oluşuyor
    • Dil modeli, yardımcı yapının ispata ulaştırdığı çok sayıda örnek gördüğü için olimpiyat problemlerinde de yeni yapılar önerebiliyor

Doğrulanabilirlik ve uygulama sınırları

  • AlphaGeometry’nin sunduğu tüm olimpiyat problem çözümleri bilgisayar tarafından kontrol edilip doğrulandı
  • Sonuçlar, önceki yapay zeka yöntemleri ve olimpiyatlardaki insan performanslarıyla karşılaştırıldı
  • Matematik koçu ve eski olimpiyat altın madalyalısı Evan Chen bazı çözümleri değerlendirdi
    • AlphaGeometry’nin çıktısı doğrulanabilir ve temiz
    • Geçmişte ispat temelli yarışma problemlerine verilen yapay zeka çözümleri bazen doğru, bazen yanlış olabiliyor ve insan kontrolü gerektirebiliyordu
    • AlphaGeometry’nin çözümleri hem makine tarafından doğrulanabilir bir yapıya sahip hem de insanlar tarafından okunabiliyor
    • Koordinat sistemiyle devasa cebirsel hesapları zorlamak yerine, öğrenciler gibi açı ve benzer üçgenler gibi klasik geometri kurallarını kullanıyor
  • Bir IMO oturumu 6 sorudan oluşuyor ve bunların genellikle yalnızca 2’si geometriye odaklanıyor
    • Bu nedenle AlphaGeometry, tek bir oturumdaki soruların yaklaşık üçte birine uygulanabiliyor
    • Buna rağmen yalnızca geometri yeteneğiyle 2000 ve 2015 IMO bronz madalya barajını geçebilen ilk yapay zeka modeli oldu

Matematiksel akıl yürüten yapay zekaya doğru genişleme

  • AlphaGeometry, yapay zekanın mantıksal olarak akıl yürütme ve yeni bilgiyi keşfedip doğrulama yeteneğinin büyüdüğünü gösteriyor
  • Olimpiyat düzeyindeki geometri problemlerini çözmek, daha derin matematiksel akıl yürütme ve daha gelişmiş genel amaçlı yapay zeka sistemlerine giden yolda önemli bir dönüm noktası
  • Yapay zekayı büyük ölçekli sentetik veriyle sıfırdan eğitme yaklaşımı, matematiğin ötesinde bilimde ve yapay zekada yeni bilgi keşfi yöntemlerini etkileyebilir
  • AlphaGeometry, Google DeepMind ve Google Research’ün matematiksel akıl yürütme yapan yapay zeka çalışmalarının çizgisi üzerinde yer alıyor
  • Uzun vadeli hedef; birden çok matematik alanına genelleşmek, genel amaçlı yapay zeka sistemleri için gerekli gelişmiş problem çözme ve akıl yürütmeyi geliştirmek ve insan bilgisinin sınırlarını genişleten yapay zeka sistemleri oluşturmak

İlgili okumalar

1 yorum

 
GN⁺ 2024-01-18
Hacker News yorumları

  • IMO gibi yarışmalarda problem hazırlayan biri olarak bu makaleyi çok ilginç buldum. Aynı zamanda yapay zekaya, yani akıllı bir bilgi dizini ve akıl yürütme biçimleri dizinine ilk yenilecek konunun geometri olmak zorunda olduğunu düşünüyorum.
    Matematik olimpiyatı konuları arasında geometri problemleri genelde en “mekanik” olanlardır. Bir problemi koordinatlarla, örneğin XY koordinatlarıyla ya da karmaşık düzlemde ifade edebiliyorsanız, bilgisayarın çözümü bulmak için kullanabileceği sonlu bir adımlar kümesi ortaya çıkar. Elbette IMO ortamında zaman sınırı ve insan hatası bunun pratikliğini engeller. Eskiden bu yöntemle kendi hazırladığım geometri problemlerinin ve varsayımlarımın kanıtlarını WolframAlpha ile doğrulardım.
    Cebir, özellikle de eşitsizlikler de benzer; güçlü hesaplamayı zorladığınızda çoğu zaman yanıt çıkar.
    Akıllı sistemlerin gerçekten geliştiğini görmek istediğim alanlar sayılar teorisi ve kombinatorik. Arama uzayı çok daha karmaşık ve çoğu zaman bir şeyin imkânsız olduğuna dair kanıt gerektiriyor. Bu tür problemleri kaba kuvvet hesaplamayla çözmek zor.

    • Bu problemleri çözen biri olarak öncelikle teşekkür ederim. Liseden mezun olalı onlarca yıl geçmiş olsa da hâlâ ara sıra keyifle çözüyorum.
      Geometrinin ilk olacağına katılıyorum. Burada gördüğüm kadarıyla, cebirsel geometri, vektörler ve karmaşık sayı çözümlerine dayanma anlamında “kaba kuvvet” değil; ama “ilginç” yardımcı çizimleri baştan sona arama anlamında kaba kuvvet aramaya yakın.
      Geometri her zaman en kötü dersimdi, ama doğru çizim verildiğinde problemin çok daha kolaylaştığını hissederdim. Ne var ki böyle çizimleri hızla akla getiren sezgiyi edinemedim. Bu yapay zekanın da böyle bir sezgisi var gibi görünmüyor, ama çok daha hızlı şekilde seçenek yağdırabiliyor. Dikey doğrular, paralel doğrular, açıortaylar gibi oluşturulabilecek adaylar sonuçta sınırlı; açıları ve oranları tamamen açıp dökmek ya da bir noktanın kuvvetini denemek gibi yöntemlerle oldukça mekanik biçimde değerlendirilebiliyor.
      Çok etkileyici, ama “motor ve yapay zeka” anlamında bana DeepMind:Kasparov::AlphaGeo:Terry Tao gibi görünüyor.
      Sıranın büyük olasılıkla cebire geleceğine katılıyorum. Geometride olduğu gibi, çoğu zaman bir, iki ya da üç akıllıca değişken dönüşümü bulmak yeterli oluyor ve seçenekler sınırlı.
      Bazı kombinatorik problemleri de bu arama stratejisine uyabilir. Örneğin aynı nesneyi iki farklı yolla sayma türündeki problemler. Ancak bu daha uzak bir köprü ve toplam problemlerin yalnızca bir kısmını yakalayabilir.
      Sayılar teorisinin tam 42 puana giden yoldaki son sınır olacağını düşünüyorum.
    • Bu gelişmeleri olumlu görme tavrınız hoşuma gitti. Matematikte çok iyi olma yeteneğinin yakında makineler tarafından yakalanabileceği olasılığı sizde bir kayıp hissi yaratıyor mu, merak ediyorum. Yoksa böyle bir şeyin yakın zamanda olma ihtimalini görmüyor musunuz?
    • Böyle bir problem hazırlayıcı konumuna nasıl gelindiğini merak ediyorum. Bir tür başvuru süreci mi var?
      Çözülebilir olduğu doğrulandıktan sonra, nihai problem setine girecek belirli problemlerin nasıl seçildiğini de merak ediyorum. Oylama mı yapılıyor, yoksa başka bir değerlendirme yöntemi mi var?
    • Başta üç değişkenli eşitsizliklerin önce çözüleceğini sanıyordum. Çünkü neyin kanıt sayılacağı konusunda belirsizlik daha az. Ama sonraki problemin zaten 2000 yılında çözülmüş olduğunu bilmiyordum (http://www.mmrc.iss.ac.cn/~xgao/paper/jar-gdbase.pdf)
      Birileri sentetik geometriyi bir macera oyununa dönüştürmeli. Lean’den daha basit bir kanıt yazma dili kullanılabilir ve görsel olarak da güzel hale getirilebilir.

  • Makaleyi doğru okuduysam bu gerçekten sağlam bir çalışma gibi görünüyor. Geçen ay DeepMind’ın açık bir matematik araştırma problemini çözdüğünü yanlış biçimde pazarladığı yapay zeka matematik makalesinden çok daha meşru. Yine de yapısının genelde düşündüğümüz otomatik akıl yürütme/zeka fikrinden ne kadar farklı olduğu epey dikkat çekici
    Anladığım kadarıyla Transformer’ı milyonlarca temel geometri teoremiyle eğitip kanıtı kaba kuvvetle aramak için kullanıyorlar. Temel geometri bağlamı nedeniyle yapı kaçınılmaz olarak temel düzeyde kalıyor ve doğru/yanlış sembolik olarak kolayca karara bağlanabiliyor. Kaba kuvvet arama başarısız olursa, orta nokta eklemek gibi yardımcı geometrik inşaları rastgele ekleyip bu ek malzemeyle arama yapılabiliyor mu diye baktıklarını düşündüm
    Düzenleme: Imnimo’nun düzeltmesinde olduğu gibi, ters anlamışım. Kaba kuvvet arama saf kaba kuvvet arama; Transformer ise hangi yardımcı inşanın ekleneceğini tahmin etmek için kullanılıyor
    Ayrıca blog yazısında yok ama gerçek problem ifadelerinin de düzeltilmesi/uyarlanması gerekmişti. Örneğin özgün metindeki “ABC üçgeninin yükseklikleri AH1, BH2, CH3 olsun…” gibi bir cümle, “ABC bir üçgen olsun. Yapay zeka, CI açı ACB’nin açıortayı olacak şekilde BAC açısının açıortayı olan I noktasını tanımlasın…” gibi çok daha açık bir tanım listesine dönüştürülmüş ve sonunda “T1I=IZ olduğunu kanıtlayın” biçimini alıyor

    • Bu açıklama bana biraz doğru gelmiyor. Kaba kuvvet aramayı Transformer değil, sembolik çözücü yapıyor. Yeni çıkarım gelmediğinde Transformer’dan olası yardımcı inşalar önermesi isteniyor; rastgele eklenmiyor
    • Neden bunun otomatik akıl yürütme/zekaya dair genel fikirden uzak olduğunu düşündüğünü anlamıyorum. Akıl yürütme temelde bir arama problemidir
      Anlattığın süreç, insanların kullandığı süreçle birebir aynı. Yararlı görünen bir şeyi tahmin eder, ayrıntıları mekanik biçimde çözeriz. Takılırsak başka bir tahmin yaparız. Sonuçta bir ağacı aramaya benzer
      İnsanlar bu süreci 1955’te zaten çözmüş ve teoremleri kanıtlayabilen çalışan bir prototip de yapmıştı: https://en.wikipedia.org/wiki/Logic_Theorist Kilit nokta iyi sezgisel yöntemler kullanmakta. Sinir ağları veriden sezgisel yöntemler çıkarabildiği için burada anlamlı
      “Otomatik akıl yürütme”nin genel fikrini ne olarak gördüğünü merak ediyorum. Her problemi tek bir doğrusal geçişte çözen sihirli bir cihaz mı?
    • “Kaba kuvvet arama başarısız olursa orta nokta eklemek gibi yardımcı geometrik inşalar ekleyip, o ek malzemeyle arama yapılabiliyor mu diye bakmak” okulda öğrendiğim geometriyle birebir aynıydı ve bundan gerçekten nefret ederdim
      Ancak üniversitede matematik bölümüne girdikten sonra işi doğru yapmayı öğrenip keyif almaya başladım
    • Yardımcı çizgi çizme rolü için LLM kullanmak fazlasıyla verimsiz. Basit bir IMO problemini çözmek için sayısız makinenin seferber edildiğini hayal etmek zor
      Bu alan hâlâ erken aşamada ve bitmemiş çok iş var gibi görünüyor. Arama kısmı küçük bir sinir ağıyla değiştirilmeli; akıl yürütme kısmı ise zor değil ve büyük ölçüde iyileştirilmesi gerekiyor gibi durmuyor
      Artık performansı öz-oyun ile artırma zamanı. Düzlem geometri problemlerinde kanıtlanması gereken sonucu şeklin bir noktası, koşulları başka bir nokta olarak görüp iki oyuncunun birbirlerine doğru olabildiğince ilerlemesini ve veri paylaşmasını sağlayabiliriz. Bu süreçte her oyuncunun katkısı, Go’daki galibiyet/mağlubiyet hesabına benzetilerek performans iyileştirmede kullanılabilir

  • Bu belirli model genellenebilir görünmese de sinirsel-sembolik yaklaşım çok umut verici görünüyor
    Bu, günümüzde makine öğrenmesinin büyük kısmını oluşturan giderek güçlenen “Sistem 1” araçlarını, mantıksal kanıt üretimi gibi yapılandırılmış “Sistem 2” araçlarıyla bağlama yöntemi. Sistem 2 plan yapabilir ve çıktının doğruluğunu ya da değerini kontrol edebilir
    Sistem 2 takılana kadar ilerler; takıldığında Sistem 1, durum uzayının hangi kısmının sırada kontrol edileceğine dair sezgisel bir tahmin sağlar
    Burada bilgisayarla kanıt üretilebilmesinden yararlanarak 100 milyon kanıttan oluşan bir veri kümesi oluşturulmuş ve ölçeklenebilir özdenetimli öğrenme mümkün kılınmış. Sembolik alanlar, bu tür veri üretimine iyi izin veren bir biçimde görünüyor. Tekil örneklerin değeri düşük olsa da bir araya geldiklerinde yararlı bir ön eğitim mümkün olabilir
    Bu unsurları birleştirince, epey uzağa gidebilecek bir yaklaşım ortaya çıkıyor
    Temel kilometre taşı, belirli bir biçimsel/sembolik alana bağımlı olma gereğinden kurtulup, o alanda öğrenilen becerileri genelleyebilen bir ön eğitim sistemi yapmak

    • Her şeyi tek seferde çözmek gerekmiyor. Bu yaklaşım hem matematiği hem de programlamayı değiştirme potansiyeline sahip. Çünkü biçimsel doğrulamayı yalnızca kısmen kullanılan niş bir araç olmaktan çıkarıp tüm uygulayıcıların genel araç kutusunun bir parçası hâline getirebilir
      Ayrıca uygulanabildiği alanlarda, mevcut yapay zeka akımında “halüsinasyon” denen temel sorunlardan birini tamamen çözer. Ancak bu çözüm, doğruluğu kanıtlayan yapay zeka dışı bir sistem olduğu için mümkün
      Büyük resimde bu yaklaşım çok yeni değil. Biyokimyada yapay zeka ile aday moleküller bulup fiziksel deneylerle doğrulama yöntemi kullanılageldi
      Kombinatoryal oyun yapay zekaları da yapay zekayı uzun zamandır eski usul Monte Carlo araması için girdi olarak kullanıyor
    • Bu, bir tür genel yapay zekaya ulaşmak için en yakın olasılık gibi görünüyor

  • Makaleyle birlikte kod ve ağırlıkları yayımlamalarına sevindim. Hatırladığım kadarıyla, çalıştırılabilir akıl yürütme kodu ve checkpoint yayımlayan ilk ünlü DeepMind makalesi bu. Daha erken bir örnek varsa düzeltilmek isterim
    Henüz yayımlanmış bir eğitim seti ya da örnek eğitim kodu görünmüyor ama yine de başka araştırmacıların üzerine inşa edebileceği bir şey sunmuş olmaları iyi bir ilerleme. Sonuçta akademik makalenin amacı da bu

    • Veri kümesinin de eksik olması üzücü. 100 milyon sentetik örnek ürettiklerini söylüyorlar; bu örnekler AlphaGeometry ile mi üretildi? Bu sentetik veriyi üretmek için kullanılan filtreleme kodu ve başlangıç girdileri nerede?
      Yanılmıyorsam t5 modeli mi kullanıyorlar? En azından SentencePiece t5 sözlüğünü kullanıyor gibi görünüyor
      Bu modeli eğitmek için ne kadar GPU zamanı harcandığını ve hangi eğitim parametrelerinin kullanıldığını da merak ediyorum
      Yanlış anlaşılmak istemem. Bu sistem büyüleyici ve uygulamalı mühendisliğin nasıl görünmesi gerektiğini gösteriyor. Sadece eğitim ayrıntıları, başlangıç verileri ve sentetik verinin nasıl üretildiği hakkında daha fazlasını bilmek isterdim

  • Dil modelinin ne sıklıkla işe yarar çizimler ürettiğini çok merak ediyorum. Rastgele olandan kesinlikle daha iyidir, ama iyi bir şey bulana kadar binlerce çizim mi fırlatıyor, yoksa insan uzmanlarla benzer oranda işe yarar öneriler mi sunuyor, bilmiyorum.
    Makalede şöyle deniyor: “Dil modeli çözümleme süreci, k adet alternatif yardımcı çizimi açıklayan k farklı dizi döndürdüğü için, her ışının skorunu bir değer fonksiyonu olarak kullanıp bu k seçenek üzerinde beam search yapıyoruz. Bu kurulumda ışınlar arasında paralelleştirme çok kolay olduğundan, paralel hesaplama kaynağı olduğunda büyük ölçüde hızlanıyor. Deneylerde beam boyutu k=512, maksimum yineleme sayısı 16 ve her düğümün dallanma katsayısı, yani çözümleme batch boyutu 32 kullanılıyor.”
    Ama 512 ve 16’nın önerilen toplam çizim sayısına nasıl çevrildiğini tam olarak anlamıyorum. Beam boyutu ve maksimum yineleme kaldırıldığında performansın yalnızca bir miktar düştüğü de söyleniyor. Bu, modelin gerçekten işe yarar çizimleri üst sıralara oldukça iyi taşıdığı ve binlercesinin yalnızca en zor problemler için gerektiği anlamına mı geliyor?

    • Kişisel tahminim, bu kısmın dil ile insan-makine benzetmesinin sınırlarına sertçe çarptığı yönünde.
      Yine de deneyecek olursak özet 262.144, ama bunu harfi harfine almamak gerek.
      Çözümleme fonksiyonunun çıktısı token’dır; kabaca bir kelimenin 3/4’ü kadar olsa da burada 1 kelime varsayalım.
      Çıktı token’ı başına değerlendirilen token sayısı beam_size * branching_factor * max_iterations = 512 * 32 * 16 = 262.144.
      Örnek çözümdeki kelime sayısını saymak yeterli: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      Çözümün toplam token sayısı 2289 ve değerlendirilen toplam token sayısı 262.144 * 2289 = 600.047.616.
      Zorlama bir hesapla “değerlendirilen çözüm sayısını” toplam değerlendirilen token sayısı / çözümün toplam token sayısı olarak alırsak 262.144 eder. Her yineleme adımında görülen token sayısıyla aynı değer olduğu için kulağa mantıklı geliyor.

  • Kullanılan Transformer’ın küçük olması ilginç. Makaleye göre Meliad kütüphanesinin varsayılan ayarlarıyla eğitilmiş; 12 katman, 1.024 embedding boyutu, 8 attention head’i ve ReLU aktivasyonu kullanan 4.096 boyutlu attention arası yoğun katmana sahip.
    Giriş ve çıkış head’lerinin embedding katmanları hariç tüm Transformer’da 151 milyon parametre var. Özel tokenizer, SentencePiece’in ‘word’ moduyla eğitilmiş ve sözlük boyutu 757. Maksimum bağlam uzunluğu 1.024 token ile sınırlandırılmış ve T5 tarzı göreli konum embedding’leri kullanılmış. Dizilerin %90’dan fazlası 200’den kısa olduğu için sequence packing de kullanılmış.

    • Küçük demek zor. LLM alanının dışında epey olağan bir boyut. Örneğin normal boyutlu bir dil modeli, çeviri modeli veya akustik model düzeyinde. Bazıları bu boyuta bile büyük diyebilir.
    • Bu sonuç, doğru biçimde formüle edilebilirse Transformer’ların hard science alanlarında kapabileceği başka alçakta asılı meyveler olabileceğini gösteriyor. Bu örnek ölçek büyütme meselesi değilmiş gibi görünüyor.

  • Benim için gerçekten yeni olan şey, önceki en iyi sistemin bile bu problemlerden 10’unu çözebilmesiydi. Düzlem geometri problemleri için karar algoritmaları olduğunu duymuştum ama pratik algoritmalar olduklarını bilmiyordum. Bakınca kaynak olarak http://www.mmrc.iss.ac.cn/~xgao/paper/book-area.pdf çıkıyor.

    • Evet. Üstelik AlphaGeometry’nin sinir ağı olmayan kısmı, yani sembolik işleme ve lineer cebir bileşenleri tek başına da önceki en iyi performansı aşabiliyor. Burada ciddi miktarda çalışma sinir ağı olmayan bileşenlere de girmiş.
    • İlginç, ama Evan Chen’in kitabındaki formüllerle ağırlık merkezi koordinatı hesaplarını zorlayarak modern bir dizüstü bilgisayarda bile IMO’nun yaklaşık %30’unun çözülebileceğini düşünüyorum. Çoğunun üçgen problemi olduğu düşünülürse bu makul.

  • Bu tür sonuçlar için genelde “insan ispatına benzemiyor” diye şüphelenmeye hazırdım, ama Evan Chen’in bunların gerçekten temiz ve insanların okuyabileceği ispatlar olduğunu söylediğini görünce fikrim değişti.
    Evan Chen, olimpiyat matematiği topluluğunda tanınmış bir isim ve ünlü bir olimpiyat geometri kitabının da yazarı[1]; bu yüzden bu kez makinenin IMO problemlerinin bir kısmını gerçekten fethettiğini kabul etmek gerek.
    [1]: https://web.evanchen.cc/geombook.html

    • Yine de ek materyaldeki[1] tam ispatta IMO P3 ispatı Fig1.f ve Step 26’da bir hata var gibi geldi. ∠GMD = ∠GO2D deniyor; bunun yanlış olduğunu ve ∠GMD + ∠GO2D = π olması gerektiğini düşündüm. Mantığı takip etmeye çalıştım ama Step 25’i yorumlayamadım. Bu adım bir halüsinasyon mu diye düşündüm.
      Yine de O2’nin dokuz nokta çemberi üzerinde olduğu fikri doğru.
      Düzenleme: Sözümü geri alıyorum. Yönlü açılar[2] kullanıyor gibi görünüyor; o durumda bu ifade doğru.
      [1]: https://storage.googleapis.com/deepmind-media/DeepMind.com/B...
      [2]: https://web.evanchen.cc/handouts/Directed-Angles/Directed-An...

  • Bununla ilgili olarak https://www.nytimes.com/2024/01/17/science/ai-computers-math... da görülmeye değer
    https://news.ycombinator.com/item?id=39030186 üzerinden gelmiş ve ilgili başlık buraya birleştirilecek

  • İlgili: https://aimoprize.com/
    IMO’da iyi performans gösteren modele verilen 10 milyon dolarlık ödül