AlphaGeometry İsimli Yapay Zeka, Uluslararası Matematik Olimpiyatları'ndaki Onlarca Geometrik Teoremi İspatlayabiliyor!

Uluslararası Matematik Olimpiyatı (IMO) üniversite öncesi öğrenciler için muhtemelen en prestijli yarışmadır. Her yıl dünyanın dört bir yanından gelen öğrenciler bronz, gümüş ve altın madalyalar için yarışıyor. Yakında yapay zeka programları da onlarla yarışabilir.

Ocak ayında Google DeepMind'dan Google DeepMind ve New York Üniversitesi'nden Trieu H. Trinh, Nature dergisinde AlphaGeometry adlı yeni bir yapay zeka programını tanıttı. Araştırmacılar, programın geçmiş Uluslararası Matematik Olimpiyatı'ndaki 30 geometri probleminden 25'ini çözebildiğini, bunun da insan altın madalya sahiplerininkine benzer bir başarı oranı olduğunu bildirdi. Yapay zeka ayrıca 2004 IMO'sunda uzmanların dikkatinden kaçan bir soruya daha genel bir çözüm buldu.

Uluslararası Matematik Olimpiyatı'nda yarışan öğrencilerin iki gün boyunca farklı matematik alanlarından altı problemi çözmeleri gerekiyor. Bazı problemler o kadar karmaşık ki uzmanlar bile çözemiyor. Bu soruların genellikle kısa ve zarif çözümleri var; ancak her biri çok fazla yaratıcılık gerektiriyor. Bu da onları yapay zeka araştırmacıları için özellikle ilginç kılıyor.

Matematiksel bir ispatı bilgisayarların bildiği bir programlama diline çevirmek zor bir iştir. Geometri için özel olarak geliştirilmiş resmi programlama dilleri vardır, ancak bunlar matematiğin diğer alanlarındaki yöntemleri çok az kullanır; bu nedenle bir ispat, örneğin karmaşık sayıları içeren bir ara adım gerektiriyorsa, geometri için özelleşmiş programlama dilleri kullanılamaz.

Bu sorunu çözmek için Trinh ve meslektaşları, insan tarafından üretilen ispatların resmi bir dile çevrilmesini gerektirmeyen bir veri seti oluşturdu. İlk olarak bir algoritmanın bir dizi geometrik "öncül" veya başlangıç noktası oluşturmasını sağladılar: örneğin, bazı ölçüleri çizilmiş ve kenarları boyunca ek noktalar işaretlenmiş bir üçgen. Araştırmacılar daha sonra üçgenin hangi açıların eşleştiği ve hangi doğruların birbirine dik olduğu gibi diğer özelliklerini çıkarmak için tümdengelimli bir algoritma kullandılar. Araştırmacılar, öncülleri türetilen özelliklerle birleştirerek teoremler ve bunlara karşılık gelen ispatlardan oluşan bir eğitim veri seti oluşturdular. Örneğin, bir problem bir üçgenin belirli bir özelliğini, örneğin iki açısının eşit olduğunu kanıtlamayı içerebilir. İlgili çözüm daha sonra tümdengelim algoritmasını buna götüren adımlardan oluşacaktı.

Ancak bir Uluslararası Matematik Olimpiyatı düzeyindeki sorunları çözmek için AlphaGeometry'nin daha da ileri gitmesi gerekiyordu. Trinh ve ekibi makalelerinde şöyle yazıyorlar:

Eksik olan kilit parça, yeni ispat terimleri üretmektir.

Örneğin, bir üçgenle ilgili bir şeyi kanıtlamak için, problemde bahsedilmeyen yeni noktalar ve çizgiler eklemeniz gerekebilir ve bu da büyük dil modellerinin (LLM'ler) yapmak için çok uygun olduğu bir şeydir.

Büyük Dil Modelleri, bir kelimenin diğerini takip etme olasılığını hesaplayarak bir metin oluşturabilen modellerdir. Trinh ve ekibi, AlphaGeometry'yi teoremler ve ispatlar üzerinde benzer bir şekilde eğitmek için veritabanlarını kullanabildiler. Geliştirdikleri Büyük Dil Modeli, bir problemin çözümünde yer alan tümdengelim adımlarını öğrenmiyordu; bu iş hala diğer özel algoritmalar tarafından yapılıyordu. Yapay zeka modeli, bunun yerine noktaları, çizgileri ve diğer yararlı yardımcı nesneleri bulmaya odaklandı.

AlphaGeometry'ye bir problem verildiğinde, tümdengelim algoritması önce bu problemle ilgili bir ifade listesi türetiyor. Kanıtlanacak ifade bu listede yer almıyorsa, yapay zeka devreye giriyor. Örneğin, ABCX'in bir paralelkenarı temsil etmesi için ABC üçgenine dördüncü bir X noktası eklemeye karar verebiliyor; bu, programın önceki eğitimden yapmayı öğrendiği bir şey. Bunu yaparken yapay zeka, tümdengelim algoritmasına üzerinde çalışabileceği yeni bilgiler veriyor. Bu süreç, YZ ve tümdengelim programı istenen sonuca ulaşana kadar tekrarlanabiliyor. Uluslararası Matematik Olimpiyatı'na üç kez altın madalya kazanan Fields Madalyası sahibi Peter Scholze, şöyle diyor:

Yöntem kulağa makul geliyor ve bazı yönlerden Uluslararası Matematik Olimpiyatı katılımcılarının eğitimine benziyor.

AlphaGeometry'yi test etmek için bilim insanları 2000 yılından bu yana IMO'da yer alan 30 geometrik problemi seçti. Daha önce geometrik problemleri çözmek için kullanılan ve "Wu'nun algoritması" olarak adlandırılan program, sadece 10 tanesini doğru çözmeyi başarırken ve GPT-4 hepsinde başarısız olurken, AlphaGeometry bunların 25 tanesini başarıyla çözdü. Araştırmacılara göre yapay zeka, 30 problemden ortalama 15,2'sini çözen Uluslararası Matematik Olimpiyatı katılımcılarının çoğundan daha iyi performans gösterdi (altın madalya kazananlar ortalama 25,9 problemi doğru çözüyor).

Araştırmacılar, yapay zeka tarafından üretilen ispatları incelediklerinde, bir problemi çözme sürecinde programın sağlanan tüm bilgileri kullanmadığını fark ettiler. Bu, AlphaGeometry'nin kendi başına yola çıktığı ve ilgili (ancak daha genel bir teoreme) bir çözüm bulduğu anlamına geliyordu. Ayrıca, Uluslararası Matematik Olimpiyatı katılımcılarının kötü performans gösterdiği karmaşık görevlerin genellikle yapay zekadan daha uzun kanıtlar gerektirdiği de açıktı. Görünüşe göre makine, insanlarla aynı zorluklarla mücadele ediyor!

AlphaGeometry, henüz Uluslararası Matematik Olimpiyatı'nda yer alamıyor, çünkü geometri, yarışmanın sadece üçte birini oluşturuyor; ancak Trinh ve meslektaşları, yaklaşımlarının kombinatorik gibi diğer matematiksel alt disiplinlere de uygulanabileceğini düşünüyorlar.

Kim bilir, belki de birkaç yıl içinde insan olmayan bir katılımcı ilk kez Uluslararası Matematik Olimpiyatı'nda yer alır. Belki altın madalya bile kazanır.