Dünyanın en karmaşık matematik problemlerini çözmek için geliştirilen yapay zeka AlphaProof, 2024 Uluslararası Matematik Olimpiyatı’nda dikkat çeken bir başarıya imza attı. Google DeepMind tarafından özel olarak eğitilen bu yapay zeka, genç matematikçilerin yarıştığı zorlu turnuvada 42 puan üzerinden 28 puan alarak gümüş madalya seviyesine ulaştı. Henüz resmi bir katılımcı olmamasına rağmen elde ettiği sonuç, yapay zekanın matematiksel düşünme alanında geldiği noktayı gösterdi.
AlphaProof, matematiksel teoremleri kanıtlamak üzere tasarlanmış bir yapay zeka sistemidir. Sadece dört yıl öncesine kadar matematikte mantıksal çıkarım yapabilen bir yapay zeka oluşturmak bilim dünyasının en büyük zorluklarından biriydi. Ancak Google DeepMind ve çeşitli araştırma grupları, bu tür projelerle yapay zekanın gerçek dünya problemlerinde kullanılabilecek daha geniş akıl yürütme kabiliyetlerine sahip olmasını hedefliyor. Bu sayede yapay zeka, mantığa dayalı hareket ederek, yanlış veya uydurma bilgi üretme sorunundan da kurtulabilir.
AlphaProof gibi yapay zekaların başarısında Lean adlı kanıt asistanı programının etkisi büyüktür. 2013 yılında Microsoft Research’te yazılım mühendisi olarak çalışan Leo de Moura tarafından geliştirilen Lean, başlangıçta yazılım kodu denetlemek için tasarlandı. Ancak zamanla matematikçiler ve yapay zeka araştırmacıları tarafından matematiksel teoremlerin doğruluğunu sınamak için de vazgeçilmez bir araç haline geldi. Kevin Hartnett’in “The Proof in the Code” adlı eserinde Lean’in bu evrimi detaylı biçimde ele alınıyor ve programın matematik dünyasında nasıl benimsendiği anlatılıyor.
Lean ve benzeri kanıt asistanları, matematiksel ifadeleri biçimsel dile çevirerek doğruluk kontrolü yapabiliyor. İnsanların günlerce hatta aylarca süren incelemeleri gerektiren karmaşık kanıtlar, bu yazılımlar sayesinde çok daha hızlı ve hatasız onaylanabiliyor. Ancak bu sistemlerin kullanımı ilk başlarda zorlu ve matematiksel ifadelerin kodlanması için kapsamlı kütüphanelerin oluşturulması gerekiyordu. Örneğin, Londra Imperial College’dan profesör Kevin Buzzard’ın, öğrencilerine Lean ile çalışma öğrettiği sırada, “2’nin 1’den farklı olduğunu kanıtlaması” istenmişti. Bu tür temel ama otomatik olarak doğrulanması gereken ifadeler, programın mantığını anlamak için zorunlu bir adım olarak öne çıkıyordu.
Başlangıçta Lean’in matematiksel kapsamı sınırlıydı ve bunu artırmak için çok sayıda matematikçinin programa katılması gerekiyordu. Buzzard ve meslektaşları 2018’de karmaşık matematiksel kavramlar olan “perfectoid uzaylar”ı programa dahil etmek için aylara yayılan yoğun çalışmalar yaptı. Bu çalışmalar, Lean’in matematik dünyasında yaygınlaşmasını sağladı ve 2025’e gelindiğinde akademi ile teknoloji alanında on binlerce kullanıcı programı kullanarak daha karmaşık projeler geliştirmeye başladı. Yapay zeka araştırmacıları da Lean’in sunduğu zengin kütüphanelerden yararlanarak, AlphaProof gibi modelleri eğitti.
Lean’in yaratıcısı Leo de Moura ve matematikçiler, programlarını “gerçeği kesin olarak doğrulayan bir makine” olarak tanımlıyor. Kodlarda hata olmadığını yüzde yüz garanti altına almak isteyen de Moura için bu, yazılımların güvenliği anlamına gelirken, matematikçiler için yeni teoremlerin keşfini daha tutarlı ve düzenli hâle getirerek bilimin ilerlemesini hızlandırmak demekti. Böylece matematiksel kanıtların doğruluğu, insan hatalarından arındırılarak daha sağlam temellere oturtuluyor.
Kevin Hartnett’in kitabı, Lean’in yükseliş hikayesini karmaşık karakterler ve detaylarla zenginleştirirken, matematikle bilgisayar kodlaması arasındaki bağları da gözler önüne seriyor. Math ve kodlamanın benzer mantık yapıları, bu tür yapay zeka destekli sistemlerin matematik dünyasında köklü değişiklikler yaratmasının yolunu açtı. Bu gelişme sadece akademik çevreler için değil, yapay zekanın mantıksal düşünme kapasitesini artırarak daha güvenli ve doğru bilgi üretimi sağlaması açısından da büyük öneme sahip.
Gelecekte Lean ve AlphaProof gibi yapay zekalar, matematikte bilinmeyen yeni bölgelerin keşfedilmesine olanak tanıyabilir. Karmaşık kanıtların otomatik kontrolü, bilim insanlarının zamanlarını daha yaratıcı ve yenilikçi çalışmalara ayırmasını mümkün kılabilir. Ayrıca teknolojinin diğer alanlarında, özellikle büyük veri analizi ve algoritma geliştirme süreçlerinde, kanıt asistanlarının rolü giderek artacak gibi görünüyor. Matematiğin ve yapay zekanın bu kesişimi, bilimsel düşüncenin ve insan bilgisinin sınırlarını yeniden tanımlama potansiyelini taşıyor.
📎 Kaynak: sciencenews.org
