OpenAI'dan 700'den fazla yapay zekâ üretimi matematik el yazması, kanıtların doğrulanması konusunda endişe yaratıyor

Makine yazımı matematiğin toplu yayımı

Teorik bilgisayar bilimci Nisheeth Vishnoi'ye göre OpenAI, 6 Ekim'de dahili bir yapay zekâ sistemi tarafından üretilmiş yedi yüzden fazla matematiksel el yazmasını yayımladı. Hacker News ana sayfasına ulaşan "Makinelere Matematiği Kim Öğretti?" başlıklı denemesinde Vishnoi, el yazmalarının bir kısmının Lean proof assistant ile resmî kanıtlar içerdiğini, diğerlerinin ise doğrulamanın daha erken aşamalarında olduğunu belirtiyor. OpenAI'nin sonuçlardan bazılarının hata içerebileceğini kabul ettiğini ve topluluğu bunları incelemeye davet ettiğini yazıyor.

Ölçek hakkında bir fikir vermek için Vishnoi, bu yayını 2021'de, yaklaşık dört yüz gönderinin birkaç gün içinde geldiği FOCS program komitesine başkanlık etmesine benzetiyor. O sel, tanıdığı bir topluluğun yıllık üretimi gibi hissettirmişti; bu yayım ise, yazdığına göre, üzerinde geçemediği bir mesafe duygusu yarattı ve sonuçta el yazmalarının çok azını okuyabildi.

Bireysel iddialar için kurulmuş güven gelenekleri

Denemenin temel gözlemi, matematiğin kendini kişisel sorumluluk yoluyla denetlediğidir. Bir sonuç duyuran matematikçi itibarını o sonuca bağlar, kamuya açılmadan önce argümanı anlamak için aylarca ya da yıllarca zaman harcamış olması beklenir ve ciddi bir hatanın bedelini sonraki yıllar boyunca ödeyebilir. Vishnoi, en iyi matematikçilerin, kendisi dahil, hatalı kanıtlar yayımladığını belirtiyor.

Şirket kaynaklı toplu bir yayım bu yapıyı tersine çevirir. Dikkat, sonuçların salt sayısından doğar; tek bir hatanın maliyeti ise bütün grup boyunca seyrekleşir. Vishnoi, matematiğin güveni korumak için kullandığı geleneklerin bu şekilde üretilip duyurulan sonuçlar için tasarlanıp tasarlanmadığından emin değil.

Pahalı olan kısım kontrol etmenin kendisi

Vishnoi'nin yazdığına göre tanıdık olmayan bir kanıtı anlamak bir matematikçinin günlerini ya da haftalarını alabilir: ayrıntıları teker teker incelemek, önermenin özgün problemi yansıttığını doğrulamak ve bilinenlerle karşılaştırmak gerekiyor. Resmî kanıt sistemleri önemli ölçüde yardımcı olur; ancak hangi sonuçların önemli olduğuna karar vermek ayrı bir soru, bir zevk meselesi ve Vishnoi, matematiksel zevki tanımaya eğitilmiş bir makinenin OpenAI'nin sunduklarının parçası olmadığını not ediyor.

Sonuç bir asimetri. Şirket el yazmalarını görece ucuza üretebiliyor; buna karşılık onları anlamlı kılmak için gereken dikkat, yayımlanmış olmalarıyla kendiliğinden ortaya çıkmıyor. Vishnoi, bunu Mayıs ayında yazdığı, doğrulamanın yıllar süren bir çıraklıkla öğrenilen bir beceri olduğunu ve matematik giderek makinelere devredilirse aşınabileceğinden endişe ettiği "Dal ve Dilek" adlı denemesiyle ilişkilendiriyor. Yeni yayım ikinci bir olasılık daha ekliyor: mevcut doğrulama kapasitesi, malzemenin niceliği karşısında basitçe boğulabilir.

Makinelerin matematiği nereden geldi

Vishnoi'nin kendi alanları, Unique Games Conjecture, sparsest cut, graph Laplacian'lar ve optimizasyon dahil, yayımda yer alıyor ve OpenAI'nin üzerinde yıllar geçirdiği bazı problemleri çözdüğünü iddia ettiğini söylüyor. Öğrencileri eğitmeye ve meslektaşlarını sonuçlar boyunca yönlendirmeye harcanan zamanı, nadiren basıya ulaşan bir bilgiyi aktarmayı düşünüyor: belirli bir reduction neden işe yarar, doğal bir yaklaşım neden başarısız olur, bir problemin kötü biçimlendirildiği nasıl anlaşılır. Bunların çoğu makalelerde değil sohbetlerde ve tahtalarda yaşardı.

Üniversitelerde eğitim almış birçok matematikçi, kendisinin öğrettikleri ve birlikte çalıştıkları dahil, yapay zekâ şirketlerine geçti. Vishnoi bu harekete itirazının olmadığını vurguluyor ve eski endüstriyel laboratuvarların kendi alanlarının açık katılımcıları olduğunu belirtiyor. Endişesi değişimin biçimiyle ilgili: üniversiteler insanları kamusal destekle ve bilgi paylaşımına adanmış bir kültür içinde eğitiyor; şirketler sonra nesiller boyunca inşa edilmiş uzmanlığı toplayıp üniversitelerin eşleşemeyeceği hesaplama kaynaklarıyla desteklenen tescilli sistemlere dönüştürüyor; ve o bilgiyi geliştirenler, ondan ne inşa edileceği konusunda çok az söz sahibi.

Neden önemli

Resmî doğrulama açısından bu yayım bir merak değil pratik bir dönüm noktası: yüzlerce makine üretimi matematiksel sonuç, bir alt kümesi Lean kanıtları taşıyor, makine denetimli matematiği toplu üretime doğru götürüyor; bu noktada doğruluk artık bir yazarın itibarına bağlı değil. Vishnoi'nin denemesi, bu çıktının çevresindeki insan sistemlerinin — inceleme kapasitesinden önceliklendirmeye, alacak ve sorumluluğun nasıl atandığına — ucuz üretim karşısında kötü ölçeklendiğini savunuyor. Böyle yayımlar rutin hâle gelirse, alanın darboğazı kanıt üretmekten, hangilerinin kıt insan dikkatini hak ettiğine karar vermeye kayıyor. Deneme ayrıca araştırma kurumları için daha geniş bir soru çerçeveliyor: kamusal olarak geliştirilen bilgi tescilli bir yeteneğe dönüştüğünde, üniversite ile endüstri arasındaki geleneksel değişim, iki tarafın da varsaydığı şekilde çalışmayı bırakıyor.