Uluslararası Matematik Olimpiyatlarında Yapay Zeka: AlphaProof ve AlphaGeometry 2 Gümüş Madalya Standardına Nasıl Ulaştı?

Matematiksel akıl yürütme, bilimsel keşiflerde ve teknolojik gelişmelerde ilerlemeyi yönlendiren, insanın bilişsel yeteneklerinin hayati bir yönüdür. İnsan bilişiyle eşleşen yapay genel zekayı geliştirmeye çalışırken, yapay zekayı gelişmiş matematiksel akıl yürütme yetenekleriyle donatmak çok önemlidir. Mevcut yapay zeka sistemleri temel matematik problemlerini çözebilirken cebir ve geometri gibi ileri matematik disiplinleri için gereken karmaşık akıl yürütmeyle mücadele ediyor. Ancak Google DeepMind'ın yaptığı gibi bu durum değişiyor olabilir önemli adımlar Bir yapay zeka sisteminin matematiksel akıl yürütme yeteneklerinin geliştirilmesinde bu atılım gerçekleştirildi. Uluslararası Matematik Olimpiyatı (IMO) 2024. 1959'da kurulan IMO, dünya çapındaki lise öğrencilerini cebir, kombinatorik, geometri ve sayı teorisi konularındaki problemlerle zorlayan en eski ve en prestijli matematik yarışmasıdır. Her yıl genç matematikçilerden oluşan takımlar altı zorlu problemi çözmek için yarışırlar. Bu yıl, Google DeepMind iki yapay zeka sistemini tanıttı: resmi matematiksel akıl yürütmeye odaklanan AlphaProof ve geometrik problemlerin çözümünde uzmanlaşmış AlphaGeometry 2. Bu yapay zeka sistemleri, gümüş madalya sahibi düzeyde performans göstererek altı problemden dördünü çözmeyi başardı. Bu yazıda bu sistemlerin matematik problemlerini çözmek için nasıl çalıştığını inceleyeceğiz.

AlphaProof: Matematiksel Teorem Kanıtı için Yapay Zeka ve Biçimsel Dilin Birleştirilmesi

AlphaProof, resmi dili kullanarak matematiksel ifadeleri kanıtlamak için tasarlanmış bir yapay zeka sistemidir. Yalın. Bütünleştirir İkizler burcuönceden eğitilmiş bir dil modeli olan AlfaSıfır, satranç, shogi ve Go'da ustalaşmakla ünlü bir takviyeli öğrenme algoritması.

Gemini modeli, doğal dildeki problem ifadelerini resmi olanlara çevirerek, değişen zorluk seviyelerindeki problemlerden oluşan bir kütüphane oluşturur. Bu iki amaca hizmet eder: matematiksel kanıtları doğrulamak için kesin olmayan doğal dili kesin biçimsel dile dönüştürmek ve resmi dil kesinliğiyle olası çözümlerin bir listesini oluşturmak için Gemini'nin tahmin yeteneklerini kullanmak.

AlphaProof bir sorunla karşılaştığında potansiyel çözümler üretir ve bunları doğrulamak veya çürütmek için Yalın'da kanıt adımları arar. Bu aslında sinir ağı Gemini'nin ifadeyi kanıtlamak veya çürütmek için doğal dil talimatlarını Lean sembolik biçimsel diline çevirdiği nöro-sembolik bir yaklaşımdır. Sistemin kendisine karşı oyun oynayarak öğrendiği AlphaZero'nun kendi kendine oynama mekanizmasına benzer şekilde AlphaProof, matematiksel ifadeleri kanıtlamaya çalışarak kendini eğitir. Her ispat denemesi, AlphaProof'un dil modelini geliştirir ve başarılı ispatlar, modelin daha zorlu problemlerle başa çıkma yeteneğini güçlendirir.

Uluslararası Matematik Olimpiyatı (IMO) için AlphaProof, farklı zorluk seviyelerini ve matematik konularını kapsayan milyonlarca problemin kanıtlanması veya çürütülmesi yoluyla eğitildi. Bu eğitim, AlphaProof'un sorunlara tam yanıtlar bulana kadar çözümlerini geliştirdiği yarışma boyunca da devam etti.

AlphaGeometry 2: Geometri Sorunlarını Çözmek için Yüksek Lisans ve Sembolik Yapay Zekayı Bütünleştirme

AlphaGeometry 2, en son yinelemesidir. AlfaGeometri Geometrik problemleri gelişmiş hassasiyet ve verimlilikle çözmek için tasarlanan seri. Önceki modelin temellerini temel alan AlphaGeometry 2, sinirsel büyük dil modellerini (LLM'ler) sembolik yapay zeka ile birleştiren nöro-sembolik bir yaklaşım kullanıyor. Bu entegrasyon, kural tabanlı mantığı, sinir ağlarının, geometri problemlerini çözmek için gerekli olan yardımcı noktaları belirleme konusundaki tahmin yeteneği ile birleştirir. AlphaGeometry'deki Yüksek Lisans, yeni geometrik yapıları öngörürken sembolik yapay zeka, kanıt oluşturmak için resmi mantığı uygular.

Geometrik bir problemle karşı karşıya kalındığında, AlphaGeometry'nin LLM programı çok sayıda olasılığı değerlendirerek problem çözümü için kritik öneme sahip yapıları öngörür. Bu öngörüler, sembolik motoru doğru çıkarımlara yönlendiren ve bir çözüme yaklaştıran değerli ipuçları görevi görür. Bu yenilikçi yaklaşım, AlphaGeometry'nin geleneksel senaryoların ötesine uzanan karmaşık geometrik zorlukları ele almasını sağlar.

AlphaGeometry 2'deki önemli geliştirmelerden biri Gemini LLM'nin entegrasyonudur. Bu model, önceki modele göre çok daha fazla sentetik veriyle sıfırdan eğitiliyor. Bu kapsamlı eğitim, nesne hareketlerini ve açı, oran veya mesafe denklemlerini içerenler de dahil olmak üzere daha zor geometri problemlerini ele alacak şekilde donatır. Ek olarak AlphaGeometry 2, iki kat daha hızlı çalışan ve alternatif çözümleri benzeri görülmemiş bir hızla keşfetmesine olanak tanıyan sembolik bir motora sahiptir. Bu gelişmeler AlphaGeometry 2'yi karmaşık geometrik problemleri çözmek için güçlü bir araç haline getiriyor ve bu alanda yeni bir standart belirliyor.

IMO'da AlphaProof ve AlphaGeometry 2

Bu yıl Uluslararası Matematik Olimpiyatı'nda (IMO) katılımcılar altı farklı problemle test edildi: ikisi cebirde, biri sayı teorisinde, biri geometride ve ikisi kombinatorikte. Google araştırmacıları tercüme bu problemleri AlphaProof ve AlphaGeometry 2 için resmi matematik diline dönüştürdü. AlphaProof, bu yıl yalnızca beş insan yarışmacı tarafından çözülen, yarışmanın en zor problemi de dahil olmak üzere iki cebir problemini ve bir sayı teorisi problemini ele aldı. Bu arada AlphaGeometry 2, iki kombinatorik zorluğun üstesinden gelemese de geometri problemini başarıyla çözdü

IMO'daki her problem yedi puan değerinde olup toplamda maksimum 42 puan değerindedir. AlphaProof ve AlphaGeometry 2, çözdüğü problemlerde mükemmel puanlar elde ederek 28 puan kazandı. Bu onları gümüş madalya kategorisinin en üst sıralarına yerleştirdi. Bu yıl altın madalya eşiği 29 puanla 58 yarışmacının 609'ine ulaştı.

Sonraki Atılım: Matematik Zorlukları için Doğal Dil

AlphaProof ve AlphaGeometry 2, yapay zekânın matematiksel problem çözme yeteneklerinde etkileyici ilerlemeler sergilemiştir. Ancak bu sistemler, matematiksel problemleri işlenmek üzere resmi dile çevirmek için hâlâ insan uzmanlara güvenmektedir. Ayrıca, bu özel matematiksel becerilerin, hipotezleri araştırmak, uzun süredir devam eden sorunlara yenilikçi çözümler test etmek ve kanıtların zaman alıcı yönlerini verimli bir şekilde yönetmek gibi diğer yapay zekâ sistemlerine nasıl dahil edilebileceği belirsizdir.

Bu sınırlamaların üstesinden gelmek için Google araştırmacıları Gemini'yi ve en son araştırmalarını temel alan bir doğal dil akıl yürütme sistemi geliştiriyorlar. Bu yeni sistem, resmi dil çevirisi gerektirmeden problem çözme yeteneklerini geliştirmeyi amaçlıyor ve diğer yapay zeka sistemleriyle sorunsuz bir şekilde entegre olacak şekilde tasarlandı.

Alt çizgi

AlphaProof ve AlphaGeometry 2'nin Uluslararası Matematik Olimpiyatları'ndaki performansı, yapay zekânın karmaşık matematiksel akıl yürütme becerisinde kayda değer bir ilerlemedir. Her iki sistem de altı zorlu problemden dördünü çözerek gümüş madalya düzeyinde bir performans sergilemiş ve biçimsel ispat ve geometrik problem çözmede önemli ilerlemeler kaydetmiştir. Tüm bu başarılarına rağmen, bu yapay zekâ sistemleri problemleri biçimsel dile çevirmek için hâlâ insan girdisine bağımlıdır ve diğer yapay zekâ sistemleriyle entegrasyon zorluklarıyla karşı karşıyadır. Gelecekteki araştırmalar, bu sistemleri daha da geliştirmeyi ve potansiyel olarak doğal dil akıl yürütmesini entegre ederek yeteneklerini daha geniş bir matematiksel zorluk yelpazesine yaymayı amaçlamaktadır.