OpenAI'ın 722 matematik makalesi: ispat yazmak ucuzladı, doğrulamak ucuzlamadı

Depoda ne var

OpenAI'ın depodaki açıklamasına göre model değerlendirme sürecinde yaklaşık 4.000 açık problemle sınandı. Her sonuç ortalama üç saatlik ChatGPT Pro "düşünme" hesaplamasıyla elde edildi; çıktılar konuya göre gruplandı ve yeterince önemli bulunanlar kataloğa alındı. Rakamların tamamı deponun kendi tanıtım ve sürüm geçmişi sayfalarından:

"Aile", birbiriyle bağlantılı makalelerden oluşan grup demek: ana sonuç, ona dayanan yan sonuçlar, alternatif ispatlar. Şirket depoda açıkça uyarıyor: koleksiyondaki sonuçlar farklı doğrulama aşamalarında, biçimsel ispatı olmayanların bir kısmında sorun çıkabilir ve bu sorunlar bulundukça düzeltilecek. Eski sürümler silinmeyecek, her düzeltme yeni sürüm olarak kayda geçecek.

Bir eksi işareti, üç makale

Geri çekilen makalelerden ilki, ayrık abelyen çeşitlerde Weil sınıflarının cebirselliğiyle ilgili bir çalışmaydı. OpenAI'ın sürüm notuna göre işaret hatası, ispattaki bir sadeleştirme adımını geçersiz kılıyordu. Aynı yapıyı kullanan K3 yüzeyleri üzerine iki makale de bu yüzden düştü. Aynı gün 14 makalede daha ispat onarımı, düzeltilmiş önerme ya da netleştirilmiş varsayım yapıldı.

Bu, matematikte yeni bir şey değil; insan yazarlar da hata yapar, makale geri çeker. Fark ölçekte. Bir insan makalesindeki hatayı genellikle o alanın birkaç uzmanı aylar içinde fark eder. Burada hata bir günde yakalandı, ama yalnızca biri bakmaya karar verdiği için. Bakılmayan yüzlerce makalede ne olduğunu şu an kimse bilmiyor.

Hakemlik: kimin emeği, kimin zamanı

Bir bilimsel derginin yayımladığı makale hakem denetiminden geçmiştir: alandan birkaç uzman metni okur, kusur arar, düzeltme ister. Bu iş çoğu zaman ücretsiz yapılır ve matematikte uzun sürer; karmaşık bir ispatın denetimi bir yılı aşabilir. OpenAI'ın makaleleri ise ön baskı, yani hiçbir denetimden geçmemiş metinler olarak yayımlandı.

Monash Üniversitesi'nden matematikçi Melissa Lee, The Conversation'da yazdığı ve ZME Science'ın yeniden yayımladığı yazıda, kıdemli bir meslektaşının makalelerden birini o kadar anlaşılmaz bulduğunu aktardı ki bir dergi editörü olarak eline geçse "doğrudan çöpe giderdi" demiş. Nature'ın haberinde Oxford Üniversitesi'nden Ursula Martin, OpenAI'ın camiaya "dağınık bir ilk taslak fırlatıp onu temizlememizi beklediğini" söyledi. Columbia Üniversitesi'nden sayı kuramcısı Michael Harris ise bu makaleleri okumayacağını belirtti.

Yük yalnız hakemlerde değil. Matematiğin ortak defteri sayılan ön baskı arşivi arXiv, yapay zekâyla üretilmiş gönderi yığını yüzünden ekim başında yazar başına aylık gönderi sınırı koymuştu. OpenAI'ın makaleleri arXiv'e değil GitHub'a yüklendi, ama sorun aynı: üretim maliyeti sıfıra yaklaşırken süzgeç hâlâ insan.

Lean neden tek başına yetmiyor

OpenAI'ın doğrulama yükünü hafifletmek için öne sürdüğü araç Lean. Lean, bir ispatı bilgisayarın adım adım denetleyebileceği biçimsel bir dile yazmayı sağlayan bir programlama dili ve ispat denetleyicisi. Bir ispat Lean'de derlenirse, o biçimsel ifadedeki her mantık adımının doğru olduğu makine tarafından onaylanmış olur. Depodaki ana sonuçların yaklaşık yüzde 42'sinin böyle bir biçimsel karşılığı var.

Ama burada ince bir tuzak var. Biçimsel ispatın doğruluğu, ancak makalede yazan cümleyle aynı şeyi söylüyorsa anlam taşır. Alexander Bastounis, Fabian Circelli ve Anders C. Hansen, 6 Ekim'de arXiv'e yükledikleri makalede tam olarak bu noktaya odaklandı. Yazarlara göre doğal dildeki bir matematik metnini Lean'e çeviren yapay zekâ, anlamı her zaman sadık biçimde aktaramıyor; metindeki belirsizlikleri çözme problemi kuramsal olarak durma probleminden bile daha zor. Örnek olarak OpenAI'ın eylülde duyurduğu Navier–Stokes ispatını incelediler ve Lean'deki biçimsel ispatın makaledeki ispatla örtüşmediğini gösterdiklerini yazdılar. TechCrunch'ın aktardığına göre yazarlar, kendiliğinden biçimselleştirilmiş Lean ispatlarına da diğer ispatlarla aynı hakem incelemesinden geçmeden güvenilmemesi gerektiğini savunuyor.

Benzetmeyle söylersek: Lean, bir tercümenin dilbilgisi hatası içermediğini garanti eder; tercümenin aslına sadık olduğunu garanti etmez. O ikinci denetimi yine bir insan yapmak zorunda.

Kim yazar, kim keşfeden

Depodaki tanıtım metni makaleleri "OpenAI'ın kurum içi bir modeli tarafından üretilmiş" olarak tanımlıyor. Bir insan yazar adı yok. Bu, bilim dünyasının alışık olduğu sorumluluk zincirini kırıyor: bir makalede hata çıkınca yazara soru sorulur, yazar konferansta sonucu anlatır, takip sorularını yanıtlar. Modelin kendisi bunların hiçbirini yapamıyor.

Terence Tao, yayımlamanın yapıldığı 6 Ekim'de Mathstodon'da yazdığı dört parçalık dizide bu boşluğu anlattı. Tao'ya göre geleneksel matematikte büyük bir ispat ardından konuşmalar, çalıştaylar, yeni işbirlikleri ve ders kitaplarına giden bir sindirme süreci doğurur. Bugünse problemlerin çoğu zaman, hedefleri "çözülünce" alanın geneline ilgi duymayan ve yapay zekâ çıktısını sonuç hakkında soru yanıtlayacak ya da konuşma yapacak kadar anlamayan kişilerce özerk biçimde çözüldüğünü yazdı. Bir problem bir kez "çözülmüş" sayıldığında geri alınamadığını, çözümün varlığını bilmenin bile başka yolları aramayı "kirlettiğini" ekledi ve araştırmacıların öne geçilme korkusuyla umut verici yönleri kamuyla paylaşmaktan kaçındığını not etti. Önerisi, yalnız problem çözmeyi değil anlatımı ve topluluk kurmayı da ödüllendiren bir "Matematik 2.0".

Herkes aynı kanıda değil. Rakip şirket Anthropic'te çalışan matematikçi Levent Alpöge, Nature'ın günlük bülteninin aktardığına göre sosyal medyada bunun "apaçık biçimde matematik tarihinin en önemli anı" olduğunu yazdı.

Bir de yöntem sorusu var. Princeton'daki İleri Araştırmalar Enstitüsü'nün ev sahipliğindeki Matematik ve Yapay Zekâ Danışma Grubu (AGMAI), eylül sonunda yapay zekâ şirketleri için yönergeler yayımlamıştı. TechCrunch'ın haberine göre grubun ilk isteklerinden biri ileri düzey matematik problemlerinin kapalı, dışarıdan incelenemeyen modellerle sınanmasının bırakılmasıydı; OpenAI ise depoda modellerini açık araştırma problemleriyle değerlendirdiğini açıkça yazıyor. Grup, önerilerine ne ölçüde uyulduğunu değerlendirmenin "nihayetinde matematik camiasına" kaldığını söylemekle yetindi.

Belirsiz kalanlar

Makalelerin kaç tanesinin gerçekten doğru ve yeni olduğu bilinmiyor; bu ancak okundukça ortaya çıkacak. Bazı haberlerde Riemann hipotezi ve Birch–Swinnerton-Dyer sanısı gibi Milenyum Ödülü problemleri anıldı, ama deponun kendi açıklamasında Riemann zeta fonksiyonu için bir "sıfırsız bölge" sonucu geçiyor; bu, hipotezin kendisinin ispatı değil, ona dair kısmi bir ilerleme iddiası. Üstelik OpenAI bu sonucun yazımının okunabilirlik için insanlarca düzenlendiğini ve sabit üretim yönteminin dışında kaldığını belirtiyor. Modelin adı, tam olarak nasıl yönlendirildiği ve 4.000 denemenin kaçının başarısız olduğu da açıklanmış değil.

Önümüzdeki aylarda bakılacak şey, depodaki sürüm geçmişinin nasıl uzadığı olacak. Her geri çekme ve düzeltme, birinin oturup okuduğunun kanıtı. Asıl açık soru da burada duruyor: bir model bir öğleden sonrada makale üretebiliyorsa, matematikçilerin sınırlı okuma saatleri hangi makalelere ayrılacak ve bu kararı kim verecek?

Fotoğraf: MathKnight ✡ (Talk) No machine-readable author provided. MathKnight assumed (based on copyright claims)., CC BY 2.5, Wikimedia Commons