Gowers: modellerin çözdüğü matematik problemleri karşı örnekle çözüldü, ispatla değil

Fields Madalyalı matematikçi Timothy Gowers, kendi blogunda dikkat çekici bir ayrım yapıyor: dil modellerinin bugüne kadar çözdüğü ünlü matematik problemlerinin neredeyse tamamı ispatla değil karşı örnekle çözüldü.

Fark ne

Matematikte bir iddiayı çürütmekle kanıtlamak birbirinden çok farklı iki iş.

Karşı örnek bulmak, iddianın yanlış olduğunu gösteren tek bir nesne üretmek demek. "Şu özellikteki her sayı şunu sağlar" diyen bir iddiayı yıkmak için sağlamayan tek bir sayı bulmak yeterli. Bu bir arama işi: doğru yerde, doğru biçimde bakmak gerekiyor.

İspat ise iddianın sonsuz sayıda durumun hepsinde doğru olduğunu göstermek. Tek bir örnekle olmaz; her durumu kapsayan bir akıl yürütme zinciri kurmak gerekiyor. Bu bir kurgu işi.

Neden modeller birinde daha iyi

Ayrım, modellerin nasıl çalıştığıyla doğrudan ilgili. Karşı örnek arama, geniş bir olasılık uzayında hızla dolaşmayı, çok sayıda adayı denemeyi ve elemeyi gerektiriyor. Dil modelleri bunda iyi: hızlılar, yorulmuyorlar ve insanın aklına gelmeyecek tuhaf adayları da deniyorlar.

İspat kurmak ise farklı bir şey istiyor — her adımın bir öncekinden zorunlu olarak çıktığı, hiçbir yerinde boşluk olmayan bir yapı. Bir ispatta "muhtemelen" ya da "genellikle" yok; tek bir gevşek halka bütün zinciri geçersiz kılıyor.

Neden önemli

Gowers'ın gözlemi, "yapay zeka matematik problemi çözdü" başlıklarının nasıl okunması gerektiğini gösteriyor. İki farklı başarı aynı cümleyle anlatılıyor ama aynı şey değil:

• Karşı örnek — gerçek ve değerli bir katkı. Yıllardır açık duran bir sorunun cevabını verebiliyor ve o cevap doğrulanabiliyor.
• İspat — matematiğin asıl işi. Bir teoremin neden doğru olduğunu açıklıyor, sadece doğru olduğunu değil.

Bu ayrım küçümseme değil. Karşı örnek bulmak da zor bir iş ve modellerin bunda gösterdiği başarı gerçek. Ama katkının niteliğini doğru adlandırmak, bir sonraki adımın ne olduğunu görmeyi sağlıyor.

Doğrulanabilirlik meselesi

Ayrımın pratik bir sonucu daha var. Bir karşı örnek tek başına doğrulanabilir: örneği alıp iddiayı sağlamadığını kontrol edersiniz, iş biter. Karşı örneğin nasıl bulunduğu önemli değil.

Bir ispat ise satır satır denetlenmek zorunda. Modelin ürettiği ispatta gizli bir boşluk olabilir ve bunu bulmak, ispatı okuyan bir matematikçinin emeğini gerektiriyor. Yani modelin ispat üretmesi, doğrulama yükünü ortadan kaldırmıyor — yalnızca yer değiştiriyor.

Bu da modellerin matematikte neden karşı örnek tarafında daha hızlı ilerlediğini açıklıyor: o tarafta sonuç kendini doğruluyor.

Aynı ayrım başka alanlarda

Gowers'ın matematikte yaptığı ayrım, yapay zekanın kullanıldığı hemen her alanda karşılığı olan bir kalıp. Modeller cevabı kolay doğrulanan işlerde belirgin biçimde daha güvenilir.

Bir kod parçasının çalışıp çalışmadığı testle anlaşılıyor; bir açığın gerçekten sömürülebilir olup olmadığı denenerek görülüyor; bir hipotezin yanlış olduğu tek bir veriyle gösterilebiliyor. Bunların hepsinde model üretiyor, doğrulama başka bir mekanizma yapıyor.

Buna karşılık cevabın doğruluğu ancak uzman değerlendirmesiyle anlaşılan işlerde — bir stratejinin isabetli olup olmadığı, bir metnin bir olayı doğru anlatıp anlatmadığı, bir ispatın kusursuz olup olmadığı — model aynı hızda ilerlemiyor. Çünkü orada hatanın kendini ele veren bir yolu yok.

Pratik sonuç

Bir işi yapay zekaya vermeden önce sorulacak soru, modelin o işi yapıp yapamayacağı değil: çıktının doğruluğunu ucuza doğrulayabiliyor muyum? Cevap evetse model güçlü bir araç. Hayırsa, kazanılan hız doğrulama emeğiyle geri ödeniyor.