Sayılarla arası oldukça iyi olan bilgisayarlar, matematikçilerin pek de işini elinden alamamıştı. Hatta yakın zamana kadar, ortaokul seviyesindeki matematik yarışmalarında bile pek varlık gösteremiyorlardı. Ancak Google'ın DeepMind ekibi, bu durumu AlphaProof adını verdiği yapay zeka sistemiyle değiştirdi. AlphaProof, dünyanın en prestijli lisansüstü matematik yarışması olan Uluslararası Matematik Olimpiyatı'nda (IMO) gümüş madalya kazananların performansına eşdeğer bir başarı göstererek, altın madalyadan sadece bir puan uzakta kaldı. Bu, hiç de küçümsenecek bir gelişme değil.
Gerçek Anlayış
Bilgisayarların matematik yarışmalarında neden yetersiz kaldığının sebebi şuydu: Hesaplama yetenekleri insanlığın çok ötesindeyken, ileri düzey matematik için gereken mantık ve akıl yürütme konusunda pek de başarılı değillerdi. Başka bir deyişle, hızlı hesaplama yapabiliyorlardı ancak neden bu hesaplamaları yaptıklarını anlamakta zorlanıyorlardı. Toplama işlemi basit görünse de, insanlar toplama tanımlarına dayalı yarı-resmi kanıtlar oluşturabilir veya doğal sayılar ile toplama gibi işlemlerin özelliklerini aksiyomlarla tanımlayan tam-resmi Peano aksiyomları üzerinden ilerleyebilir.
Bir kanıtı ortaya koymak için insanların matematiğin yapısını anlaması gerekir. Matematikçilerin kanıtları oluşturma şekilleri, sonuca ulaşmak için kaç adım attıkları ve bu adımları ne kadar ustaca tasarladıkları, onların parlaklığının, zekasının ve matematiksel zarafetinin bir göstergesidir. Bir DeepMind araştırmacısı ve AlphaProof çalışmasının baş yazarı olan Thomas Hubert, "Bertrand Russell'ın bir artı birin iki ettiğini kanıtlamak için 500 sayfalık bir kitap yayımladığını biliyorsunuz," diyor.
DeepMind ekibi, matematiği bu seviyede anlayan bir yapay zeka geliştirmek istedi. Çalışma, yapay zeka alanındaki yaygın bir sorun olan eğitim verisi eksikliğiyle başladı.
Matematik Problemleri Çevirmeni
ChatGPT gibi yapay zeka sistemlerini güçlendiren büyük dil modelleri, milyarlarca sayfa metinden öğrenir. Eğitim veritabanlarında matematik metinleri bulunduğundan (tüm el kitapları ve ünlü matematikçilerin eserleri gibi), matematiksel ifadeleri kanıtlama konusunda bir dereceye kadar başarı gösterirler. Ancak işleyiş biçimleri nedeniyle sınırlıdırlar: Kullanıcı istemlerine verilen yanıtlarda bir sonraki kelimeyi veya token'ı tahmin etmek için devasa sinir ağları kullanırlar. Mantık yürütmeleri tasarımsal olarak istatistikseldir, bu da yalnızca doğru "gibi görünen" cevaplar verdikleri anlamına gelir.
DeepMind'ın yapay zekâsının doğru "gibi görünmesi" yeterli değildi; yüksek seviye matematikte bu kabul edilemezdi. Yapay zekânın doğru "olması", mutlak kesinliği garanti etmesi gerekiyordu. Bu da tamamen yeni, daha biçimsel bir eğitim ortamı gerektiriyordu. Bunu sağlamak için ekip, Lean adlı bir yazılım paketini kullandı.
Lean, matematikçilerin hassas tanımlar ve kanıtlar yazmasına yardımcı olan bir bilgisayar programıdır. Matematiksel ifadelerin çevrilebildiği hassas, biçimsel bir programlama diline dayanır. Çevrilmiş veya biçimselleştirilmiş ifade programa yüklendiğinde, doğruluğunu kontrol edebilir ve "bu doğru", "bir şeyler eksik" veya "henüz kanıtlanmamış bir gerçeği kullandın" gibi yanıtlar alabilir.
Sorun şuydu ki, çevrimiçi olarak bulunan matematiksel ifadelerin ve kanıtların çoğu "doğal dil" ile yazılmıştı (örneğin, "doğal sayılar kümesi X olsun ki..."). Lean dilinde yazılmış ifade sayısı oldukça sınırlıydı. Hubert, "Biçimsel dillerle çalışmanın en büyük zorluğu, çok az veri olmasıdır," diyor. Bunu aşmak için araştırmacılar, matematiksel ifadeleri doğal dilden Lean'e çeviren bir Gemini büyük dil modelini eğitti. Model, otomatik bir biçimselleştirici gibi çalıştı ve yaklaşık 80 milyon biçimselleştirilmiş matematiksel ifade üretti.
Mükemmel değildi, ancak ekip bunu kendi avantajlarına kullanmayı başardı. Hubert, "Yaklaşık çevirilerden yararlanabileceğiniz birçok yol vardır," diye belirtiyor.
Düşünmeyi Öğrenmek
DeepMind'ın AlphaProof için fikri, ekibin satranç, Go ve shogi oynayan AlphaZero yapay zeka sistemlerinde kullandığı mimariyi kullanmaktı. Lean'de ve genel olarak matematikte kanıt oluşturmak, ustalaşılması gereken bir başka oyun olarak görülüyordu. Hubert, "Bu oyunu deneme yanılma yoluyla öğrenmeye çalışıyorduk," diyor. Kusurlu biçimselleştirilmiş problemler, hata yapma fırsatları sunuyordu. Öğrenme aşamasında AlphaProof, veritabanındaki problemleri basitçe kanıtlıyor ve çürütüyordu. Eğer bir çeviri kötü yapılmışsa, bir şeylerin yanlış olduğunu anlamak faydalı bir alıştırma biçimiydi.
AlphaZero gibi, AlphaProof da çoğu durumda iki ana bileşen kullandı. Birincisi, deneme yanılma yoluyla Lean ortamında çalışmayı öğrenen birkaç milyar parametreli devasa bir sinir ağıydı. Kanıtlanan veya çürütülen her ifade için ödüllendirildi ve attığı her mantık adımı için cezalandırıldı; bu, kısa ve zarif kanıtları teşvik etmenin bir yoluydu.
Ayrıca, ikinci bir bileşen olan ağaç arama algoritmasını kullanmak üzere eğitildi. Bu algoritma, her adımda kanıtı ilerletmek için alınabilecek tüm olası eylemleri keşfediyordu. Matematikteki olası eylem sayısı neredeyse sonsuz olabileceğinden, sinir ağının görevi arama ağacındaki mevcut dallara bakmak ve yalnızca en umut vadedenlere hesaplama bütçesi ayırmaktı.
Birkaç haftalık eğitimin ardından sistem, geçmiş lise seviyesi yarışmalarından alınan problemler üzerine kurulu çoğu matematik yarışması kıyaslamasında iyi puan alabiliyordu, ancak en zorlularında hala zorlanıyordu. Bunlarla başa çıkmak için ekip, AlphaZero'da veya başka bir yerde bulunmayan üçüncü bir bileşen ekledi.
İnsanlığın Kıvılcımı
Test-Zamanı Pekiştirmeli Öğrenme (TTRL) adı verilen üçüncü bileşen, matematikçilerin en zor problemlerle nasıl başa çıktığını kabaca taklit ediyordu. Öğrenme kısmı, sinir ağları ve arama ağacı algoritmalarının aynı kombinasyonuna dayanıyordu. Fark, neyden öğrendiğinde geliyordu. Otomatik biçimselleştirilmiş problemlerin geniş bir veritabanına dayanmak yerine, TTRL modunda çalışan AlphaProof, ele aldığı probleme dayalı olarak tamamen yeni bir eğitim veri seti oluşturarak çalışmaya başladı.
Süreç, orijinal ifadenin sayısız varyasyonunu oluşturmayı içeriyordu; bazıları biraz daha basitleştirilmiş, bazıları daha genel, bazıları ise yalnızca gevşek bir şekilde bağlıydı. Sistem daha sonra bunları kanıtlamaya veya çürütmeye çalıştı. Bu, çoğu insanın özellikle zor bir bulmacayla karşılaştığında yaptığına kabaca benziyordu; yapay zekanın "Anlamadım, bu yüzden pratik yapmak için önce bunun daha kolay bir versiyonunu deneyelim" demesinin karşılığıydı. Bu, AlphaProof'un anında öğrenmesini sağladı ve inanılmaz derecede iyi çalıştı.
2024 Uluslararası Matematik Olimpiyatı'nda, her biri yedi puan değerinde altı farklı problemi çözmek için 42 puan vardı. Altın madalya kazanmak için katılımcıların 29 puan veya üzerinde alması gerekiyordu ve 609 katılımcıdan 58'i bunu başardı. Gümüş madalyalar 22 ila 28 puan alan kişilere verildi (123 gümüş madalya sahibi vardı). Problemler zorluk seviyesine göre değişiyordu, en zor problem "nihai boss" olarak görev yapıyordu. Bu problemi yalnızca altı katılımcı çözebildi. AlphaProof yedinci oldu.
Ancak AlphaProof, her şeyi çözen bir matematik dehası değildi. Gümüş madalyasının bir bedeli vardı; kelimenin tam anlamıyla.
Yaratıcılığı Optimize Etmek
AlphaProof'un performansındaki ilk sorun, tek başına çalışmamasıydı. Başlangıç olarak, yazılım çalışmaya başlamadan önce insanların problemleri Lean ile uyumlu hale getirmesi gerekiyordu. Ve altı Olimpiyat probleminden dördüncüsü geometriyle ilgiliydi ve yapay zeka bunun için optimize edilmemişti. Bununla başa çıkmak için AlphaProof, geometri konusunda uzmanlaşmış bir yapay zeka olan AlphaGeometry 2'yi çağırmak zorunda kaldı; bu yapay zeka görevi birkaç dakika içinde ter dökmeden tamamladı. Kendi başına AlphaProof 21 puan aldı, 28 değil. Bu nedenle teknik olarak gümüş değil, bronz kazanırdı. Ancak kazanmazdı.
Olimpiyatın insan katılımcıları altı problemlerini dört buçuk saat süren iki oturumda çözmek zorundaydı. AlphaProof ise, onlarla günlerce, birden fazla tensör işlem birimini tam kapasiteyle kullanarak mücadele etti. Zaman ve enerji açısından en çok tüketen bileşen, çözebildiği üç problemle üçer gün boyunca uğraşan TTRL idi. AlphaProof'a insan katılımcılarla aynı standartlar uygulansaydı, temelde süresi dolmuş olurdu. Ve yüz milyarlarca dolarlık bir teknoloji devinde doğmamış olsaydı, parası da tükenirdi.
Makalede, ekibin AlphaProof'u çalıştırmak için gereken hesaplama gereksinimlerinin çoğu araştırma grubu ve hevesli matematikçiler için muhtemelen karşılanamaz derecede pahalı olduğunu kabul ediyorlar. Yapay zeka uygulamalarındaki hesaplama gücü genellikle TPU-gün olarak ölçülür; bu, bir tensör işlem biriminin tam gün boyunca çalışması anlamına gelir. AlphaProof, problem başına yüzlerce TPU-gün gerektiriyordu.
Üstelik Uluslararası Matematik Olimpiyatı lise seviyesinde bir yarışmadır ve problemler, zor olduğu kabul edilmekle birlikte, matematikçilerin zaten bildiği temellere dayanıyordu. Araştırma düzeyindeki matematik, mevcut kavramlarla çalışmak yerine tamamen yeni kavramlar icat etmeyi gerektirir.
Ancak DeepMind, bu engelleri aşabileceğine ve AlphaProof'u daha az kaynak tüketecek şekilde optimize edebileceğine inanıyor. Hubert, "Matematik yarışmalarında durmak istemiyoruz. Gerçekten araştırma düzeyindeki matematiğe katkıda bulunabilecek bir yapay zeka sistemi inşa etmek istiyoruz," diyor. Hedefi, AlphaProof'u daha geniş araştırma topluluğunun erişimine sunmak. "Ayrıca bir tür AlphaProof aracı da yayınlıyoruz," diye ekliyor. "Bu, matematikçiler için kullanışlı olup olmadığını görmek amacıyla küçük bir güvenilir test kullanıcı programı olacaktır."
