Yapay Zeka, İnsan Akıl Yürütmesinin Sınırlarını Zorluyor: Matematikte Sessiz Bir Devrim

Bu ayın başlarında bir yapay zeka (YZ) girişimi, geliştirdikleri yapay zeka ajanının, son derece zorlu "yüksek boyutlu küre paketleme problemi"nin (İng: "higher dimensional sphere-packing problem") iki durumuna ait ispatı doğruladığını duyurdu. Bu ispatlar, 2022 yılında Ukraynalı matematikçi Maryna Viazovska'ya matematiğin en prestijli ödüllerinden biri olan Fields Madalyası'nı kazandırmıştı.

Bu gelişme, alanda sessiz bir devrimin ortaya çıkışına işaret eden devasa bir adımdır.

Yüzeyden bakıldığında bu durum o kadar da olağanüstü görünmeyebilir. Sonuçta matematikçiler, yeteneklerini geliştirmek için uzun zamandır abaküsler, sürgülü cetveller, hesap makineleri ve nihayetinde bilgisayarlar gibi çeşitli araçlar kullanıyorlar. Ancak bu araçların hiçbiri matematikçilerin yerini almadı; sadece dikkatimizi daha ilginç problemlere yeniden odaklamamıza olanak tanıdılar. Yapay zekanın matematiğe girişi de bu sürecin bir başka adımı gibi hissedilebilir. Fakat arada çok önemli bir fark var: Bu kez araçlar bize sadece hesaplama yapmada yardımcı olmuyor; akıl yürütmemize veya en azından insan akıl yürütmesinin temelinde yatan birçok rutini gerçekleştirmemize de destek oluyorlar.

Bu durum, matematik yapmanın ne anlama geldiği konusunda sismik bir değişimi temsil ediyor. Herhangi bir yardım almadan çalışıp kendi bilişsel sınırlarımızın uçlarında mücadele etmek yerine, insan sezgisi ile makine düzeyindeki disiplini eşleştirerek bu sınırları genişletmemizi sağlayacak araçlar inşa etmeye ve bu araçların ayarlarını yapmaya başlıyoruz. Bu da en karmaşık ispatlarımızın tek bir zihnin kavrayabileceği eserler olmayacağı anlamına gelebilir; daha ziyade, söz konusu ispatlar, yalnızca yapay zeka araçlarına büyük ölçüde dayanan kolektif bir zihinde tam olarak anlaşılabileceklerdir. Bu aynı zamanda ele alabileceğimiz matematiğin kapsamının dramatik bir şekilde artacağı anlamına da gelmektedir.

Makine Kontrollü İspatların Yükselişi

Aslında bu değişim bir süredir ayak seslerini duyuruyordu. Yıllardır en büyük ispatlarımız tek bir matematikçinin bireysel çabası olmaktan çıkmış durumdadır. Pür matematikteki (İng: "pure mathematics") birçok modern araştırma makalesi, artık devasa kavramsal çerçevelere, uzun bağımlılık zincirlerine ve tek bir kişinin tam olarak içselleştiremeyeceği devasa sonuç kataloglarına dayanıyor. Dört renk teoremi ve Kepler varsayımı gibi büyük ispatlarda bilgisayarlar daha önce de rol oynamıştı. Ancak şu anda asıl değişen şey, matematiksel argümanları kontrol etmek için tasarlanmış programlar olan resmi ispat asistanlarıyla birlikte çalışan yapay zeka sistemlerinden bekleyebileceğimiz özerklik ve güvenilirlik düzeyidir.

Bu resmi doğrulama dilleri, matematiksel argümanları bir bilgisayarın adım adım kontrol edebileceği şekilde ifade ederek ispatın her bir parçasının mantıksal olarak sağlam olduğunu garanti eder. Örneğin Lean dilini ele alalım. Sıradan matematiksel yazımın aksine Lean, her tanımın ve çıkarımın açıkça yapılmasını gerektirir ve her adımı mekanik ile yöntemsel olarak kontrol eder. Bu dil son derece tavizsizdir ancak bunu üretken bir şekilde yapar: Eğer argüman Lean tarafından onaylanırsa, bu durum teorik olarak ispatın gizli varsayımlara veya asılsız inanç sıçramalarına sahip olmadığı anlamına gelir. Geçtiğimiz birkaç yıl içinde Lean, araştırma düzeyindeki matematik için standart bir ispat alanı haline geldi ve matematikçiler giderek daha karmaşık hale gelen problemleri desteklemek için yeni "kütüphaneler" inşa ediyorlar.

Bu kütüphaneler, özenle programlanmış tanımların ve halihazırda doğrulanmış teoremlerin devasa koleksiyonlarıdır. Bu sayede araştırmacıların söz konusu dili kullanarak yeni sonuçları ispatlamalarına olanak tanınır. Ancak yakın zamana kadar, en yeni ispatları makine tarafından kontrol edilebilir bir forma dönüştürmek, uzmanların aylarını veya yıllarını bu işe ayırmasını gerektiriyordu.

Viazovska'nın yüksek boyutlu küre paketleme sonuçlarının yakın zamanda yapılan resmi doğrulaması tam da bu bağlamda anlaşılmalıdır. Küre paketleme problemi, sadece içinde yaşadığımız üç boyutlu dünyada değil, her boyuttaki uzayda özdeş kürelerin birbirine ne kadar sıkı paketlenebileceğini sorar. Viazovska'nın atılımından önce küre paketleme problemi sadece bir, iki ve üç boyutlarda tam olarak çözülebilmişti; daha yüksek boyutlu durumların tamamı ise çözümsüz kalmıştı. Viazovska'nın sekiz ve yirmi dört boyutlu küre paketleme problemine getirdiği ispatlar, daha önce ulaşılamaz olduğu düşünülen problemleri çözen son derece derin matematiksel içgörülerdir.

Fields Madalyası Düzeyindeki Gelişmeler

Son dönemde atılan önemli adım, bir insan ve yapay zeka işbirliğinin artık bu argümanları tamamen doğrulanmış Lean koduna çevirmiş olması ve bu kodun her bir adımı kontrol etmiş olmasıdır. Bu başarının salt boyutu bile şaşırtıcıdır; çünkü bunlar yakın tarihli Fields Madalyası düzeyindeki sonuçlardır ve artık bireysel hakemlerin veya büyük uzman insan ekiplerinin bile yardım almadan yeniden üretemeyeceği bir ayrıntı ve kesinlik düzeyinde onaylanmışlardır.

Bu süreçteki kilit bileşen, insanlara ait matematiksel argümanların Lean ispatlarına dönüştürülmesine yardımcı olmada hayati bir rol oynayan Math, Inc. şirketine ait yapay zeka akıl yürütme ajanı Gauss idi. Yapay zeka sistemi tamamen yardımsız çalışmıyordu; matematikçilerin yine de planı ortaya koyması, genel yapıyı şekillendirmesi ve doğru kavramların yerli yerinde olmasını sağlaması gerekiyordu. Ancak bu iskelet bir kez kurulduktan sonra sistem, eksik parçaları olağanüstü bir hızla doldurabildi. Sekiz boyutlu durumda, insan katılımcıların aylar süreceğini tahmin ettikleri çalışmayı sadece günler içinde tamamladı. Daha da karmaşık olan yirmi dört boyutlu durum ise kısa bir süre sonra onu takip etti.

Matematiğin Yeni Düzeni ve Geleceği

Bu başarı, sadece teknik bir dönüm noktasından çok daha fazlasıdır; matematikçilerin çalışmalarını organize etme biçimlerindeki yapısal bir değişime işaret etmektedir. Orijinal makalenin yazarı ve matematiksel biyoloji profesörü Kit Yates, Kaliforniya Üniversitesi (UCLA) matematikçisi ve Fields Madalyası sahibi Terence Tao ile görüştüğünde Tao, yapay zekanın acil değerinin en zor problemlerimizi doğrudan çözmekten ziyade bizi angaryadan kurtarmaktan gelebileceğini öne sürdü. Tao'nun bahsettiği bu angarya; kavramsal olarak çok basit olan ancak herhangi bir kişinin elle uğraşamayacağı kadar fazla zaman alan binlerce küçük kontrol durumudur.

Tao, bazı yapay zeka sistemlerinin bu görevlerin üstesinden gelmede halihazırda şaşırtıcı derecede iyi olduğunu ve matematikçilerin dikkatlerini sadece kayıt tutmaktan ziyade asıl stratejiye adamalarına izin verdiğini savundu. Lean gibi araçlar son derece önemlidir çünkü fikir üretmenin yaratıcılığını, o fikirleri kontrol etmenin zorluğundan ayırmamız için bize pratik bir yol sunarlar.

Imperial College London'dan yapay zeka ispat uzmanı Kevin Buzzard da bu durumu tamamlayıcı bir görüş dile getiriyor. Doğruluğu garanti etmeden kulağa çok kesin ve otoritermiş gibi gelen büyük dil modellerine (İng: "large language models") körü körüne güvenmenin tehlikeleri konusunda haklı olarak endişeleniyor. Ancak aynı zamanda formelleştirmenin (İng: "formalization") bu sorunu aşmak için geçerli bir yol sunduğunu da savunuyor. Lean'de eğer program tüm adımları kabul ederse, bu geçerli bir ispattır. Bu durum bilgisayarın mutlaka zekice bir şey yaptığı anlamına gelmez; daha ziyade resmi doğrulama dilinin gizli adımlara veya kulağa mantıklı gelen ancak aslında eksik olan argümanlara hiçbir şekilde yer bırakmadığı anlamına gelir. Buzzard'a göre buradaki asıl zorluk, modern matematiğin büyük bir kısmının henüz resmi kütüphanelere çevrilmemiş olmasıdır. Bu nedenle sistemler henüz ihtiyaç duydukları kavramlara tam olarak sahip değillerdir.

Atılan bu son adım, aradaki boşluğun kapanmaya başladığını gösteriyor. Küre paketleme projesi, neyin mümkün hale geldiğinin muhtemelen bugüne kadarki en net ve somut göstergesidir.

Bütün bunlar matematikçilerin yok olmanın eşiğinde olduğu anlamına gelmiyor. Hatta durumun tam tersi olduğunu söyleyebiliriz. Doğrulanabilir matematik alanı genişledikçe doğru soruları sorabilen, yeni tanımlar oluşturabilen ve bir argümanın ne zaman gerçekten ufuk açıcı olduğunu fark edebilen insanlara duyulan ihtiyaç da artmaktadır. Ancak bu yeni döneme uyum sağlamamız gerekecek. İnsan sezgisini ve yapay zeka azmini bir araya getirerek makine tarafından doğrulanmış kesinlik üretmek için, yalnız teorisyenler gibi değil de adeta bilimsel araç üreticileri gibi davrandığımız bir gelecekle yüzleşebiliriz.

Matematik bilimi her zaman yardımcı araçlarla ortaklık kurarak ilerlemiştir. Yapay zeka bu temel uygulamayı değiştirmiyor; sadece onu bir sonraki seviyeye taşıyor. Matematiksel kavramların ispatlanması elbette daha kolay hale gelmeyecektir ancak onları test etme, doğrulama ve sürekli olarak üzerlerine yenilerini inşa etme kapasitemiz kesinlikle artacaktır.