OpenAI bu hafta, modellerinin ileri düzey problemlerle başa çıkma becerisini göstermek amacıyla zor matematik problemleri için yüzlerce sözde çözüm yayımladı. Ancak yayımlananlar, matematik araştırmacılarından oluşan bir danışma grubunun belirlediği yönergelere tamamen uymadı ve temel soruyu yeniden gündeme getirdi: Modellerin programlanabilir bir çözüm üretmesi yeterli mi, yoksa çözümün matematikçiler tarafından anlaşılabilir ve denetlenebilir olması mı gerekiyor?
Advisory Group on Mathematics and Artificial Intelligence (AGMAI), önde gelen dokuz araştırmacıdan oluşuyor ve Princeton Üniversitesi'ndeki İleri Araştırmalar Enstitüsü tarafından ağırlanıyor. Grup, eylül ayının sonunda matematik problemlerini çözmek için ileri düzey modeller geliştiren laboratuvarlara yönelik yönergeler yayımlamıştı.
Araştırmacıların yönergelerine kısmi uyum
AGMAI, tavsiyelerine ne ölçüde uyulduğunu değerlendirmenin nihai olarak matematik camiasına ait olduğunu belirtti. En önemli tavsiyeleri arasında, ileri düzey matematik problemlerinin ticari olarak sahip olunan modeller üzerinde test edilmesine son verilmesi yer alıyordu. Buna karşılık OpenAI, kendi modellerini değerlendirmek için açık araştırma problemleri kullandığını açıkça belirtti.
OpenAI, sonuçları hızla yayımlamak ve modellerin sonuçlarına nasıl ulaştığı hakkında bilgi sunmak gibi bazı ilkeleri izledi. Ancak 719 metinden yalnızca 10'u modele ait düşünce zincirlerini içeriyordu. Ayrıca yayımlanan kanıtların %42'si biçimsel hâle getirilmedi.
Grup, insanların anlamasının zor olduğu kanıtların biçimsel bir biçime dönüştürülmesi gerektiğini düşünüyor. Bununla birlikte laboratuvarın, sonuçların yayımlanmasına bunların insanlar tarafından anlaşılmasının eşlik etmesini sağlama sorumluluğunu da vurguladı ve bu sonuçların gerçekten bilimsel anlam taşımasına yardımcı olacak matematikçilerin finanse edilmesini önerdi.
Doğal dil ile Lean kodu arasındaki boşluk
Modeller genellikle önce doğal dilde bir açıklama oluşturuyor, ardından bunu, derleyicisinin kanıtın tutarlılığını çalıştırılabilir bir biçimde doğrulayabildiği bir programlama dili olan Lean'e dönüştürmeye çalışıyor. Ancak otomatik dönüşüm, kanıtın içeriğini değiştirebilir veya açıklamanın söyledikleri ile kodun kanıtladıkları arasındaki bağı koparabilir.
Cambridge Üniversitesi ve King's College London'dan matematikçilerin yayımladığı bir makale, OpenAI'nin karmaşık akışkanların davranışına ilişkin Navier-Stokes denklemlerinden türetilen bir problem için sunduğu çözüme bağlı doğal dildeki bir kanıt ile Lean kodu arasında en az iki farklılık belgeledi. Bu farklılıklar, çözümlerden herhangi birinin mutlaka hatalı olduğunu kanıtlamıyor; ancak modellerin kendi çözümlerini insan müdahalesi olmadan biçimsel olarak ifade etmesine izin verilmesi konusunda şüphe uyandırıyor.
AGMAI ayrıca metinsel kanıt ile biçimsel sürüm arasında bağlantı kuran, makine tarafından okunabilir meta verilerin eklenmesini istedi; OpenAI bu sürümlerde böyle bir veri sunmadı. “lost in translation” adıyla bilinen makalenin yazarları, metinsel kanıtların ve otomatik olarak dönüştürülen Lean kanıtlarının, diğer kanıtların tabi olduğu inceleme ve denetime benzer bir hakem değerlendirmesinden geçirilmeden ilke olarak kabul edilmemesi gerektiği sonucuna vardı.
Bu haber neden önemli?
Sorun yalnızca kodun başarıyla derlendiğini kanıtlamakla değil, kodun gerçekten metnin açıkladığı matematiksel fikri temsil ettiğini kanıtlamakla ilgili. Geleneksel araştırmada bilim insanları sonuçlarının sorumluluğunu üstlenir ve bunları makaleler, dersler ve seminerler aracılığıyla tartışır. Bu süreç, hataların keşfedilmesine ve yeniden kullanılabilir yöntemlerin anlaşılmasına yardımcı olur.
Modeller zor bir probleme çözüm ürettiğinde ise yayımlanma anında bu insan anlayışı mevcut olmayabilir. Bu nedenle OpenAI'nin mevcut sonuçları, sorunun sona ermesinden çok bilimsel doğrulama sürecinin başlangıcına daha yakın görünüyor; bu kanıtların matematik camiası içinde kabul edilmesinden önce insan incelemesi ile metinsel ve biçimsel çıktılar arasında bağlantı kurulması hâlâ yerine getirilmesi gereken iki koşul olarak duruyor.