Yapay zekanın matematik becerilerine dair bir matematikçinin görüşü

• OpenAI’ın yeni dil modeli o3, zorlu matematik benchmark’ı FrontierMath’te %25 skor elde ederek matematik yapay zekasının lisans seviyesini aşıp aşamayacağına dair değerlendirmeleri yeniden sarstı
• FrontierMath, Epoch AI tarafından oluşturulan kapalı bir veri kümesi; “teorem kanıtı”ndan ziyade otomatik olarak doğrulanabilir sayısal cevaplar gerektiren yüzlerce zor matematik probleminden oluşuyor
• Açıklanan 5 örnek, araştırmacı matematikçiler için bile kolay değildi; Tao bunları “son derece zorlayıcı” diye nitelerken Borcherds, sayısal cevap üretmenin özgün kanıt ile aynı şey olmadığını düşünüyor
• Epoch AI’dan Elliot Glazer’ın problemlerin %25’ini “IMO/lisans tarzı problemler” olarak tanımlaması, o3’ün %25’lik skorunun gerçekte hangi zorluk seviyesine ulaştığını kapalı veri kümesi niteliği nedeniyle doğrulamayı zorlaştırıyor
• Matematikçiler için daha önemli hedef, “bu sayıyı bul”dan ziyade teoremleri doğru biçimde kanıtlamak ve insanların anlayabileceği şekilde açıklamak; dil modelleri ile Lean tabanlı yaklaşımların farklı sınırlamaları var

---

o3 ve FrontierMath’in sarstığı eşik

• o3, OpenAI’ın yeni dil modeli ve FrontierMath’te %25 skor elde etti
• ChatGPT’den sonra açık dil modelleri hızla gelişiyor; matematik problemi çözme becerileri de bu akış içinde değerlendiriliyor
• FrontierMath, Epoch AI tarafından oluşturulan kapalı bir matematik problemi veri kümesi; makale özetinde “yüzlerce” zor matematik problemi bulunduğu belirtiliyor
• Veri kümesi yayımlanırsa dil modelleri problem ve cevapları öğrenebileceğinden, problem sayısı gibi temel bilgiler bile temkinli ele alınıyor
  • Problem ve cevaplar açıklanırsa model daha önce gördüğü cevapları yeniden üretebilir
  • Bu nedenle kapalı benchmark’ların gerçek zorluk düzeyini ve temsil gücünü dışarıdan doğrulamak zor

FrontierMath problemlerinin biçimi ve zorluğu

• FrontierMath problemleri “bu teoremi kanıtla”dan çok “bu sayıyı bul” biçimine yakın
• Problemlerin açık ve hesaplanabilir bir cevabı olmalı ve otomatik doğrulamaya uygun olmalı
• Açıklanan 5 örnek problemin cevaplarının tamamı pozitif tam sayı
  • Örnek cevaplar arasında 9811 ve 367707 var
  • Diğer üç cevap daha büyük; rastgele tahminle bulunmaları zor olacak şekilde tasarlanmış
• Açık örnekler araştırmacı matematikçiler için bile bariz değil
  • Yazar, 5 problemin ifadelerinin tamamını anlıyor
  • Üçüncü problemi görece hızlı çözebildi; beşinci problem için eğriler için Weil varsayımlarını kullanan standart bir teknikle nasıl çözüleceğini biliyordu, ancak 13 basamaklı cevabı hesaplamadı
  • Birinci ve ikinci problemleri çözemeyeceğine karar verdi; dördüncü problemde çaba gösterirse ilerleme kaydedilebileceğini düşündü ama denemeden çözümü okudu
• Genel olarak zeki bir matematik lisans öğrencisi bu problemlerin hiçbirini çözmekte zorlanabilir
  • Birinci problemin analitik sayı teorisinde doktora düzeyi veya üstünü gerektireceği düşünülüyor

Sayısal cevap benchmark’larının avantajları ve sınırları

• FrontierMath’in sayısal cevaplı problemler kullanmasının temel nedeni değerlendirme maliyeti
• “Teoremi kanıtla” türünde yüzlerce cevabı değerlendirmek için insan uzman gerekir
  • 2024 itibarıyla bu seviyedeki değerlendirmeyi makinelere bırakmanın zor olduğu düşünülüyor
• Buna karşılık sayısal cevap listeleri bilgisayar tarafından çok hızlı karşılaştırılabilir
• Borcherds’e göre araştırmacı matematikçiler zamanlarının çoğunu sayılar değil, kanıtlar ve fikirler arayarak geçirir
• Yine de FrontierMath matematik yapay zekası alanında değerli
  • Zor veri kümeleri çok az
  • Böyle veri kümeleri oluşturmak çok zor veya maliyetli
  • Frieder ve diğerlerinin yakın tarihli yazısı, matematik yapay zekası veri kümelerinin sınırlarını daha derinlemesine ele alıyor

o3’ün %25’inin şaşırtıcı olmasının nedeni

• Mevcut algıda matematik yapay zekası lisans veya lisans öncesi seviyeye yakındı
• Yapay zeka, üstün yetenekli lise öğrencilerinin çözdüğü olimpiyat tarzı problemlerde çok güçleniyor
• Bir yıl içinde yapay zekanın lisans matematik sınavlarını geçeceği açık görülüyor
  • Lisans sınavları, dersi temelde anlamış öğrencilerin geçebilmesi için standart problemler içerebiliyor
  • Makineler bu tür problemleri kolayca doğru yanıtlayabilir
• Ancak standart fikirlerin yeniden kullanımının ötesine geçip ileri lisans/erken doktora seviyesinde yenilikçi fikirlere sıçramanın büyük olduğu düşünülüyor
• ChatGPT’nin yakın tarihli Putnam sınavı cevapları beklentilerin altında kaldı
  • Makinenin uygun yanıt verdiği tek soru B4 gibi görünüyordu
  • Diğer cevapların çoğu 10 üzerinden 1–2 puan seviyesinde değerlendirildi
• Bu nedenle FrontierMath’in birkaç yıl boyunca neredeyse aşılamaz olacağı bekleniyordu

Kapalı veri kümesinin bıraktığı belirsizlik

• Epoch AI’dan Elliot Glazer, Reddit’te FrontierMath problemlerinin %25’inin IMO/lisans tarzı problemler olduğunu açıkladı
• Bu ifade, açıklanan 5 problemle pek uyuşmuyor gibi görünüyor
  • Açık örnekler içindeki en kolay problemde bile eğriler için Weil varsayımlarını kullanan bir yöntem vardı
  • Ya da sonlu cisimler üzerinde derecesi 10^12 olan bir üçüncü derece polinomu çarpanlara ayırmayı gerektiren zahmetli bir kaba kuvvet yöntemi gerekebilirdi
• Bu bilgi, gerçek kapalı veri kümesinin zorluk düzeyi ve açıklanan 5 problemin temsilî bir örnek olup olmadığı konusunda soru işaretleri bırakıyor
• Veri kümesi kapalı olduğundan bu soruları kolayca doğrulamak zor
• Eğer %25’i lisans seviyesi problemlerse, o3’ün %25’lik skoru daha az şaşırtıcı olabilir
• Beklenen büyük kırılım, “qual level” olarak tanımlanan sonraki %50’lik problemlerde yapay zekanın anlamlı performans göstermeye başladığı an olacak

“Teoremi kanıtla” hâlâ farklı bir problem

• Araştırma matematiğinde önemli soru genellikle “bu teoremi kanıtla”dır
• Sayı bulma problemlerinde insanüstü performans gösteren makineler ortaya çıksa bile, birçok araştırma matematiği alanında uygulanabilirlikleri sınırlı kalabilir
• 2024’ün en büyük başarı örneği olarak DeepMind’ın AlphaProof sistemi gösteriliyor
  • AlphaProof, 2024 IMO’daki 6 problemden 4’ünü çözdü
  • Problemler “teoremi kanıtla” veya “sayıyı bul ve doğru olduğunu kanıtla” türündeydi
  • Bunlardan 3’ü tamamen biçimselleştirilmiş Lean kanıtları olarak çıktılandı
• Lean etkileşimli bir teorem kanıtlayıcıdır; mathlib ise IMO problemlerini çözmek için gereken çeşitli teknikleri ve daha fazlasını içeren bir matematik kütüphanesidir
• DeepMind sisteminin çözümleri insanlar tarafından kontrol edildi ve “tam puanlık” çözümler olarak doğrulandı
• Ancak IMO problemleri çok zor olsa da çözümleri yalnızca okul düzeyi teknikler kullandığından, bir bakıma yine lise düzeyi problemlere dönülmüş oluyor
• 2025’te makinelerin IMO altın madalya seviyesinde performans göstereceği tahmin ediliyor

Makinenin cevabını kim değerlendirecek?

• Temmuz 2025’teki IMO’ya insan öğrencilerin yanında makinelerin de katıldığı bir durum hayal edilebilir
• Makine sistemleri iki türe ayrılabilir
  • Lean, Rocq, Isabelle gibi bilgisayar kanıt denetleyicisi dilleriyle cevap sunan sistemler
  • İnsan diliyle cevap sunan dil modelleri
• Kanıt denetleyicisi diliyle sunulan cevaplarda yalnızca problem ifadesinin doğru çevrilip çevrilmediğini kontrol etmek gerekir
  • Sonrasında kanıt derlenirse bunun fiilen “tam puanlık” bir çözüm olduğu anlaşılır
• Doğal dilde cevap sunan dil modelleri farklıdır
  • Cevap makul görünse bile insan değerlendiricinin dikkatle okuyup değerlendirmesi gerekir
  • Tam puanlık çözüm olduğuna dair garanti yoktur
• Dil modellerinin mantıksal akıl yürütmede uzman insanlardan en az bir mertebe daha az doğru olduğu düşünülüyor
• Riemann hipotezine dair bir dil modeli “kanıtının”, 10 sayfalık doğru matematiğin arasına belirsiz veya hatalı iddialar serpiştirebileceği endişesi var
• Teorem kanıtlayıcıları ise tersine en az bir mertebe daha doğru görülüyor
  • Lean, insan matematik literatüründeki bir argümanı kabul etmediğinde, yazarın gördüğü örneklerde hatalı olan taraf insandı

Kalan hedef: doğru kanıt ve insanın anlaması

• Matematikçilerin istediği şey yalnızca “teoremi kanıtla” değil, doğru kanıt ve insanların anlayabileceği açıklamadır
• Dil modeli yaklaşımında “doğruluk” büyük bir endişe olmaya devam ediyor
• Teorem kanıtlayıcı yaklaşımında ise “insanın anlayabileceği biçim” endişe konusu
• Hâlâ yapılacak çok iş var
• Gelişim hızı yüksek, ancak lisans bariyerinin ne zaman aşılacağını kimse bilmiyor