Dr. Tahsin Ziya/ 30 Temmuz 2024
Matematiksel muhakeme, bilimsel keşiflerde ve teknolojik gelişmelerde ilerlemeyi yönlendiren, insan bilişsel yeteneklerinin hayati bir yönüdür.
İnsan bilişine uyan yapay genel zeka geliştirilmeye çalışırken, yapay zekayı gelişmiş matematiksel muhakeme yetenekleriyle donatmak esastır. Mevcut yapay zeka sistemleri temel matematik problemlerini çözebilirken, cebir ve geometri gibi gelişmiş matematik disiplinleri için gereken karmaşık mukakemeyi kullanırlar.
Ancak, Google DeepMind bir yapay zeka sisteminin matematiksel muhakeme yeteneklerini geliştirmede önemli adımlar attığından, bu durum değişebilir. Bu atılım , Uluslararası Matematik Olimpiyatı (IMO) 2024’te gerçekleştirildi. 1959’da kurulan IMO, dünya çapındaki lise öğrencilerine cebir, kombinatorik, geometri ve sayılar teorisindeki problemlerle meydan okuyan en eski ve en prestijli matematik yarışmasıdır. Her yıl, genç matematikçilerden oluşan takımlar altı çok zorlu problemi çözmek için yarışıyor.
Bu yıl, Google DeepMind iki yapay zeka sistemi tanıttı: Biçimsel matematiksel muhakemeye odaklanan AlphaProof ve geometrik problemleri çözmede uzmanlaşmış AlphaGeometry 2. Bu YZ sistemleri, gümüş madalyalı bir sporcunun seviyesinde performans göstererek altı problemden dördünü çözmeyi başardı. Bu makalede, bu sistemlerin matematiksel problemleri çözmek için nasıl çalıştığını inceleyeceğiz.
AlphaProof: Matematiksel Teorem Kanıtlama İçin Yapay Zeka ve Biçimsel Dili Birleştiriyor
AlphaProof, matematiksel ifadeleri resmi dil Lean kullanarak kanıtlamak için tasarlanmış bir YZ sistemidir. Önceden eğitilmiş bir dil modeli olan Gemini’yi , satranç, shogi ve Go’da ustalaşmakla ünlü bir takviyeli öğrenme algoritması olan AlphaZero ile entegre eder .
Gemini modeli, doğal dil problem ifadelerini resmi olanlara çevirerek, farklı zorluk seviyelerine sahip problemlerden oluşan bir kütüphane oluşturur. Bu, iki amaca hizmet eder: matematiksel kanıtları doğrulamak için belirsiz doğal dili kesin resmi dile dönüştürmek ve Gemini’nin tahmin yeteneklerini kullanarak resmi dil hassasiyetine sahip olası çözümler listesi oluşturmak.
AlphaProof bir sorunla karşılaştığında, olası çözümler üretir ve bunları doğrulamak veya çürütmek için Lean’de kanıt adımları arar. Bu, esasen sinir ağı Gemini’nin doğal dil talimatlarını, ifadeyi kanıtlamak veya çürütmek için sembolik biçimsel dil Lean’e çevirdiği nöro-sembolik bir yaklaşımdır. Sistemin kendisine karşı oyunlar oynayarak öğrendiği AlphaZero’nun kendi kendine oynama mekanizmasına benzer şekilde, AlphaProof matematiksel ifadeleri kanıtlamaya çalışarak kendini eğitir. Her kanıt girişimi, AlphaProof’un dil modelini iyileştirir ve başarılı kanıtlar, modelin daha zorlu sorunları ele alma yeteneğini güçlendirir.
Uluslararası Matematik Olimpiyatı (IMO) için AlphaProof, farklı zorluk seviyelerini ve matematik konularını kapsayan milyonlarca problemi kanıtlayarak veya çürüterek eğitildi. Bu eğitim, AlphaProof’un problemlere tam cevaplar bulana kadar çözümlerini geliştirdiği yarışma sırasında devam etti.
AlphaGeometry 2: Geometri Problemlerini Çözmek İçin LLM’leri ve Sembolik Yapay Zekayı Entegre Etme
AlphaGeometry 2, geometrik problemleri gelişmiş hassasiyet ve verimlilikle ele almak için tasarlanmış AlphaGeometry serisinin en son yinelemesidir . Öncülünün temelleri üzerine inşa edilen AlphaGeometry 2, sinirsel büyük dil modellerini (LLM’ler) sembolik AI ile birleştiren nöro-sembolik bir yaklaşım kullanır. Bu bütünleştirme, kural tabanlı mantığı, geometri problemlerini çözmek için gerekli olan yardımcı noktaları belirlemek için sinir ağlarının tahmin yeteneğiyle birleştirir. AlphaGeometry’deki LLM yeni geometrik yapıları tahmin ederken, sembolik AI kanıtlar üretmek için resmi mantığı uygular.
Geometrik bir problemle karşı karşıya kalındığında, AlphaGeometry’nin LLM’si çok sayıda olasılığı değerlendirir ve problem çözme için kritik öneme sahip yapıları tahmin eder. Bu tahminler değerli ipuçları olarak hizmet eder, sembolik motoru doğru çıkarımlara yönlendirir ve bir çözüme daha da yaklaşmasını sağlar. 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 bir geliştirme, Gemini LLM’nin entegrasyonudur. Bu model, selefinden önemli ölçüde daha fazla sentetik veri üzerinde sıfırdan eğitilmiştir. Bu kapsamlı eğitim, nesne hareketleri ve açı, oran veya mesafe denklemlerini içerenler de dahil olmak üzere daha zor geometri problemlerini ele alması için onu donatır. Ek olarak, AlphaGeometry 2, iki büyüklük sırası daha hızlı çalışan sembolik bir motora sahiptir ve bu da alternatif çözümleri benzeri görülmemiş bir hızla keşfetmesini sağlar. Bu gelişmeler, AlphaGeometry 2’yi karmaşık geometrik problemleri çözmek için güçlü bir araç haline getirerek alanda yeni bir standart belirler.
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ılar teorisinde, biri geometride ve ikisi de kombinatorikte. Google araştırmacıları bu problemleri AlphaProof ve AlphaGeometry 2 için resmi matematik diline çevirdi . AlphaProof, bu yıl sadece beş insan yarışmacının çözdüğü yarışmanın en zor problemi de dahil olmak üzere iki cebir problemi ve bir sayı teorisi problemiyle uğraştı. Bu arada, AlphaGeometry 2 geometri problemini başarıyla çözdü, ancak iki kombinatorik zorluğunu çözemedi
IMO’daki her problem yedi puan değerindedir ve en fazla 42’ye ulaşır. AlphaProof ve AlphaGeometry 2, çözdükleri problemlerde mükemmel puanlar alarak 28 puan kazandı. Bu onları gümüş madalya kategorisinin en üst noktasına yerleştirdi. Bu yılki altın madalya eşiği 29 puandı ve 609 yarışmacının 58’i bunu başardı.
Sonraki Adım: Matematik Zorlukları İçin Doğal Dil
AlphaProof ve AlphaGeometry 2, yapay zekanın matematiksel problem çözme yeteneklerinde etkileyici ilerlemeler sergiledi. Ancak, bu sistemler hala matematiksel problemleri işleme için resmi dile çevirmek için insan uzmanlara güveniyor. Ayrıca, bu özel matematiksel becerilerin hipotezleri keşfetmek, uzun süredir devam eden problemlere yenilikçi çözümler test etmek ve kanıtların zaman alıcı yönlerini verimli bir şekilde yönetmek gibi diğer yapay zeka sistemlerine nasıl dahil edilebileceği belirsizdir.
Bu sınırlamaların üstesinden gelmek için Google araştırmacıları, Gemini ve son araştırmalarına dayalı 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 AI sistemleriyle sorunsuz bir şekilde entegre olacak şekilde tasarlandı.
Alt çizgi
AlphaProof ve AlphaGeometry 2’nin Uluslararası Matematik Olimpiyatı’ndaki performansı, yapay zekanın karmaşık matematiksel akıl yürütmeyi ele alma yeteneğinde kayda değer bir sıçramadır. Her iki sistem de altı zorlu problemden dördünü çözerek gümüş madalya seviyesinde performans gösterdi ve resmi kanıt ve geometrik problem çözmede önemli ilerlemeler gösterdi.
Başarılarına rağmen, bu yapay zeka sistemleri hala problemleri resmi dile çevirmek için insan girdisine bağımlıdır ve diğer yapay zeka sistemleriyle entegrasyon zorluklarıyla karşı karşıyadır. Gelecekteki araştırmalar, bu sistemleri daha da geliştirmeyi, potansiyel olarak daha geniş bir matematiksel zorluk yelpazesinde yeteneklerini genişletmek için doğal dil akıl yürütmeyi entegre etmeyi amaçlamaktadır.
Not: Bu yazıda DeepL yapay zeka tecüme algoritması kullanılmış ve daha sonra revize edilmiştir.