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ş

Google DeepMind'in AlphaProof ve AlphaGeometry 2 sistemleri, Uluslararası Matematik Olimpiyatı sorularını çözdü
- AlphaProof: pekiştirmeli öğrenme tabanlı matematiksel akıl yürütme sistemi
- AlphaGeometry 2: geliştirilmiş geometri problemi çözme sistemi
- İki sistem, bu yılki Uluslararası Matematik Olimpiyatı'nda (IMO) 6 sorudan 4'ünü çözerek gümüş madalya düzeyinde bir başarı elde etti

Karmaşık matematik problemlerinin çözümünde yapay zeka başarısı

IMO'ya giriş
- 1959'dan bu yana her yıl düzenlenen en eski ve en prestijli gençlik matematik yarışması
- Yarışma soruları cebir, kombinatorik, geometri ve sayı teorisi gibi alanlardan seçiliyor
- Fields Madalyası kazananlarının önemli bir kısmı IMO çıkışlı
Yapay zeka sistemlerinin IMO meydan okuması
- AlphaProof ve AlphaGeometry 2, bu yılki IMO sorularını çözdü
- Sorular, resmi yarışma kurallarına göre puanlandı
- AlphaProof, 2 cebir sorusu ve 1 sayı teorisi sorusunu çözdü
- AlphaGeometry 2, 1 geometri sorusunu çözdü
- İki kombinatorik sorusu ise çözülemedi
- Toplam 42 puan üzerinden 28 puan alarak gümüş madalya düzeyinde bir sonuç elde edildi

AlphaProof: biçimsel akıl yürütme yaklaşımı

AlphaProof nasıl çalışıyor
- Matematiksel önermeleri Lean biçimsel diliyle ispatlıyor
- Önceden eğitilmiş bir dil modeli ile AlphaZero pekiştirmeli öğrenme algoritmasını birleştiriyor
- Doğal dildeki problemleri biçimsel önermelere çevirerek farklı zorluk seviyelerindeki sorunları çözüyor
- Bir problem verildiğinde AlphaProof, çözüm adayları üretip bunları ispatlıyor veya çürütüyor
- İspatlanan sonuçlar, AlphaProof'un dil modelini güçlendirerek daha zor problemleri çözme yeteneğini artırıyor
Eğitim süreci
- Milyonlarca problemi ispatlayarak veya çürüterek eğitildi
- Yarışma sırasında da eğitim döngüsü uygulanarak problem varyasyonları ispatlandı

Daha rekabetçi AlphaGeometry 2

AlphaGeometry 2'deki iyileştirmeler
- Gemini tabanlı bir dil modeli ve nöral-sembolik hibrit sistem
- Önceki sürüme göre 10 kat daha fazla sentetik veriyle eğitildi
- Geometri problemi çözme hızı ve doğruluğu artırıldı
- Yeni problemleri çözerken bilgi paylaşım mekanizması kullanıyor
IMO 2024 performansı
- Son 25 yıldaki IMO geometri sorularının %83'ünü çözdü
- Bu yılki yarışmada 4. soruyu 19 saniyede çözdü

Matematiksel akıl yürütmede yeni bir frontier

Doğal dil akıl yürütme sistemi deneyi
- Gemini tabanlı doğal dil akıl yürütme sistemi denendi
- Biçimsel dile çevirmeden problem çözebiliyor
- Diğer yapay zeka sistemleriyle birleştirme olasılığı araştırılıyor
Gelecek görünümü
- Matematikçiler, yapay zeka araçlarıyla birlikte çalışarak yeni hipotezleri keşfedebilir, problem çözme yaklaşımlarını deneyebilir ve ispat süreçlerini kısaltabilir
- Gemini gibi yapay zeka sistemleri, matematikte ve genel akıl yürütmede ilerleme sağlayabilir

GN⁺ özeti

AlphaProof ve AlphaGeometry 2, matematiksel akıl yürütmede yapay zekanın potansiyelini gösteriyor
Uluslararası Matematik Olimpiyatı'nda gümüş madalya düzeyinde performans göstererek yapay zekanın matematik problemi çözme yeteneğini kanıtladı
Matematikçilerin yapay zekayla birlikte yeni problem çözme yaklaşımlarını keşfetmesinin önünü açıyor
Benzer yeteneklere sahip projeler arasında OpenAI'nin GPT-3 gibi doğal dil işleme modelleri de bulunuyor

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ı

Birinci yorum
- Bu proje için çok heyecanlıyım, ancak matematik problemlerini biçimsel dile çevirme sürecinde bilgisayarın ne kadar katkı sağladığı belirsiz
- İndirilebilir çözümlerde, çeviri sürecinde neyin insan tarafından kararlaştırıldığı ve neyin bilgisayar tarafından bulunduğu net değil
İkinci yorum
- IMO'da madalyalar katılımcıların %50'sine verilir ve altın, gümüş, bronz madalya oranı 1:2:3'tür
- Yapay zekanın öğrencilerin %75'inden daha iyi çözüm üretmiş olması etkileyici
- Ancak yapay zekanın problemleri çözmek için harcadığı süre, öğrencilerin sınavda sahip olduğu süreden farklı olduğu için doğrudan karşılaştırma uygun değil
Üçüncü yorum
- AlphaGeometry sınırlı problemleri çözdü, ancak bu yöntemin matematik üzerinde daha geniş bir etkisi olacak
- Doğal dildeki matematiği biçimselleştirilmiş matematiğe dönüştüren bir pipeline uyguluyorlar ve bu, temel teori inşasını da öğrenebilir
- Bu, ispat yardımcılarının kutsal kasesi ve insanların matematiği daha doğal şekilde biçimselleştirmesine yardımcı olacak
Dördüncü yorum
- Sistem bir problemi çözmek için 3 gün harcadıysa, bu basit brute force'tan farklı değil
- Bu gerçek akıl yürütme değil
Beşinci yorum
- Lean kullanılıyor
- Bu, yalnızca matematik problemleri için değil, genel olarak anlamsız sonuçlardan kaçınmak açısından önemli
- Daha fazla insanın Lean gibi sistemlerde tipler yazmasını umuyorum
Altıncı yorum
- Bu projede yer alan insanları kıskanıyorum
- En ileri düzey teknolojiyi geliştirmek çok eğlenceli ve tatmin edici olmalı
Yedinci yorum
- En iyi tartışmalar LeanProver'ın Zulip sohbetinde yapılıyor
Sekizinci yorum
- Fields Madalyası sahibi Tim Gowers, önemli çekinceleri açıklayan ve bağlam sağlayan iyi bir genel değerlendirme sunuyor
Dokuzuncu yorum
- Teorem ispatı, çok büyük bir arama alanına sahip tek oyunculu bir oyun
- AlphaProof'a en büyük katkıyı yapanlar Lean ve Mathlib geliştiricileri
- Matematik makalelerinde biçimselleştirmenin eksikliği, otomasyon girişimlerini engelledi
Onuncu yorum
- Makineler onlarca yıldır satrançta insanlardan üstün
- Ancak insanlar hâlâ Magnus Carlsen'i izliyor
- İnsanlar, diğer insanların ne yaptığıyla ilgileniyor
- Makineler yalnızca insanlara yardımcı oldukları ölçüde ilgi çekiyor