Matematikte bazı ispatlar o kadar uzundur ki tek bir insanın baştan sona okuması neredeyse imkânsızdır. Bunların en ünlüsü, Sonlu Basit Grupların Sınıflandırması. Yaklaşık 100 matematikçinin 500’den fazla makalede yazdığı, toplamda 15 bin sayfa civarına ulaşan bu ispata matematikçiler “dev teorem” adını veriyor. Yapay zekâ şirketi Axiom, 26 Ekim’de bu ispatın ilk eksiksiz, bilgisayarla denetlenmiş sürümünü yayımladığını duyurdu.
Şirkete göre Axiom’daki mühendisler ve matematikçiler, 24 gün boyunca onlarca yapay zekâ ajanından oluşan “sürüleri” yöneterek Lean ispat asistanında yaklaşık 43,1 milyon satır kod üretti. Lean, matematiksel tanımların, iddiaların ve ispatların bir bilgisayarın her adımı kontrol edebileceği kesinlikte yazılmasını sağlayan bir programlama dili.
Dev teorem nedir, neden önemli?
Gruplar, simetriyi tarif eden temel matematiksel nesneler. Örneğin bir küpü, başlangıçtaki görünümünü bozmadan 24 farklı şekilde döndürebilirsiniz; bu dönüşler bir grup oluşturur. Sonlu gruplar, tıpkı moleküllerin atomlara ayrılması gibi “basit” parçalara ayrılabilir. Sınıflandırma teoremi, bu yapı taşlarının tam listesini veriyor: bir tür “simetrinin periyodik tablosu”.
Teoreme göre her sonlu basit grup ya asal mertebeli devirli bir grup, ya bir alterne grup, ya Lie tipi gruplardan biri ya da 26 “düzensiz” (sporadik) gruptan biri. Bunların en büyüğü olan Canavar grubu yaklaşık 8×1053 elemana sahip. Sonuç cebirden sayılar kuramına, hatta matematiksel fiziğe kadar pek çok alanda kullanılıyor. Ancak ispat onlarca yıla ve yüzlerce makaleye dağıldığı için bütünüyle denetlemek son derece zordu. 1983’te tamamlandığı ilan edilen ispattaki önemli bir boşluk ancak 2004’te 1.221 sayfalık bir çalışmayla kapatılabilmişti.
Yapay zekâ ajanları nasıl çalıştı?
Proje 1 Ekim’de bir mesajlaşma kanalının açılmasıyla başladı. Mevcut Lean çalışmaları ve literatürden çıkarılan bir “ispat haritası” işi 108 ana kilometre taşına ve yaklaşık 380 küçük göreve böldü. 2 Ekim’de ilk ajan sürüsü devreye girdi.
- Lider ajanlar zor argümanları parçalara ayırdı ve biçimselleştirilen ifadeleri gözden geçirdi.
- Diğer ajanlar mevcut sonuçları aradı ya da Lean ispatları yazdı; eksik bir ön koşul olduğunda işi başka ajanlara devredebildi.
- İnsan matematikçiler matematiksel engelleri araştırdı, mühendisler ise büyüyen sistemin verimli çalışmasını sağladı.
Süreç kusursuz ilerlemedi. Şirket, bazı kilometre taşlarının ajanların ispatlamak yerine varsaydığı devasa ön koşullar gizlediğini, bu nedenle on binlerce satırı silip işin bir kısmını yeniden başlattıklarını anlatıyor. 13 Ekim’de yalnızca bir kilometre taşı tamamlanınca, ajanlar bitmemiş hedefleri daha küçük ve kesin ifadelere bölmek üzere yeniden görevlendirildi. 10 Ekim’de ise kanala şu mesaj düştü: “Canavar grubunun basit olduğunu ispatladık.”
Makineler literatürde ne buldu?
Biçimselleştirme, insan okurun deneyimiyle tamamladığı boşlukları açıkça yazmayı zorunlu kılıyor. Bu süreçte çoğu küçük olmak üzere pek çok sorun ortaya çıktı: yazım hataları, tablolardaki yanlışlar, düşürülmüş varsayımlar. Ancak Axiom’a göre yayımlanmış kayıttan 34 önemli sapma çözülmek zorundaydı.
En önemlisi, ispatın kritik bir parçası olan “Dengesiz Grup Teoremi” için kullanılan yayımlanmış bir argümandaki kapanış iddiasına karşı örneklerin bulunmasıydı. Bu, teoremin kendisini çürütmüyordu; ama ispatın o adımı gerekçesiz kalıyordu. Ekip, sınıflandırma üzerinde çalışmış deneyimli grup kuramcılarıyla istişare ederek alternatif bir yol geliştirdi. Bu süreçte AxiomProver tarafından ispatlanan yeni bir grup kuramı sonucu da ortaya çıktı ve ayrı bir makalede yayımlandı. Şirket, hataların listesini grup kuramı topluluğuyla paylaşacağını açıkladı.
Sınırlar: Bilgisayar neyi denetler, insan neyi?
Axiom, sürecin bir sınırını açıkça vurguluyor: Lean, ispatın her mantıksal adımını kontrol eder; ancak biçimsel ifadenin gerçekten amaçlanan matematiği anlatıp anlatmadığını insanlar incelemek zorunda. Ek, ispatlanmamış bir varsayımla kanıtlanan bir sonuç da Lean’de “doğrulanmış” görünebilir. Bu yüzden ilerlemeyi saymak kolay, abartmak da kolay. Proje kodu açık lisansla yayımlandı ve tüm geliştirmenin denetlenmesi 24 saatin altında sürüyor; isteyen herkes ispatı kendi bilgisayarında kontrol edebiliyor.
Yapay zekâ okuryazarlığı açısından: Bu haber bize ne anlatıyor?
- Yapay zekânın ürettiği bir sonuca güvenmek için, onu bağımsız biçimde denetleyebilecek bir mekanizma var mı?
- “Doğrulandı” denen bir şeyde, neyin doğrulandığını ve neyin varsayıldığını ayırt edebiliyor muyuz?
- Ajan sürüleri hızlı çalışsa da yön veren, hataları yorumlayan ve son kararı veren insan uzmanlığı neden hâlâ vazgeçilmez?
- Uzun süredir “doğru” kabul ettiğimiz bilgilerde, sistematik denetimle hangi gizli hatalar ortaya çıkabilir?
Bu çalışma, yapay zekânın bilimde en verimli kullanımının belki de “cevap üretmek” değil, insan bilgisini denetlenebilir hâle getirmek olduğunu gösteriyor. Makine hızını, insan muhakemesiyle birleştiren bir model.
Kaynak: Axiom, Unite.AI
