Uluslararası Matematik Olimpiyatı, 2024 yılında alışılmadık bir yarışmacıyı ağırladı: Google DeepMind tarafından geliştirilen AlphaProof adlı yapay zeka programı. Resmi yarışmacı olmasa da, bu yapay zeka modelinin performansı büyük ilgi çekti. İki gün süren yarışmada, dünya çapından en yetenekli matematik öğrencileri altı zorlu problemi çözmeye çalışırken, AlphaProof 42 puan üzerinden 28 puan alarak gümüş madalya seviyesini yakaladı. Bu sonuç, matematik ve yapay zeka alanında önemli bir dönüm noktası olarak kabul ediliyor.
AlphaProof, matematiksel teoremleri kanıtlamak üzere tasarlanmış bir yapay zeka sistemi. Henüz dört yıl önce matematiksel akıl yürütmeyi otomatikleştirmek, bilim dünyasının en büyük zorluklarından biriydi. Ancak Google DeepMind ve diğer araştırma grupları, yapay zekanın mantıksal düşünme becerilerini geliştirerek gerçek dünya problemlerinde kullanmayı hedefliyor. Bu sayede, yapay zekanın bilgi üretirken hata yapma veya yanlış bilgi oluşturma gibi sorunlarının önüne geçilmesi amaçlanıyor.
Bu başarının arkasında, 2013 yılında Microsoft Research’te çalışan yazılım mühendisi Leo de Moura tarafından geliştirilen Lean adlı kanıt asistanı programı yer alıyor. Başlangıçta yazılım kodlarını doğrulamak için tasarlanan Lean, zamanla matematikçiler ve yapay zeka araştırmacıları tarafından yeni teoremlerin doğruluğunu kontrol etmek için kullanılır hale geldi. Kevin Hartnett’in “The Proof in the Code” adlı kitabında, Lean’in nasıl bir doğruluk makinesine dönüştüğü ve onun etrafında şekillenen iş birliği hikayeleri detaylı şekilde anlatılıyor.
Lean, matematiksel ifadeleri ve kanıtları programlama diline benzer bir mantık düzeninde yazarak işlemesiyle dikkat çekiyor. Hartnett’in kitabında belirttiği gibi, matematiksel bir kanıttaki mantık boşlukları, yazılım kodundaki hatalar gibidir. Lean bu tür hataları otomatik olarak tespit ederek, teorilerin güvenilirliğini artırıyor. Carnegie Mellon Üniversitesi’nden Jeremy Avigad, Lean’i matematiksel kanıt yazımı için uyarlayan ilk isimlerden biri oldu ve bu program insan tarafından oluşturulan uzun ve karmaşık kanıtların doğrulanmasını mümkün kıldı.
Ancak Lean’i kullanmak başlangıçta kolay değildi. Matematikçilerin sorunları sıradan dilden koda çevirmesi ve temel matematik kavramlarını temsil eden kütüphaneler oluşturması gerekiyordu. Imperial College London’dan Kevin Buzzard, öğrencileri için Lean ile ders hazırlarken temel bir eşitsizliği bile kanıtlaması gerektiğini fark etti. 2 sayısının 1 sayısına eşit olmadığı, günlük hayatta sorgulanmayan bir gerçek olsa da, Lean’in mantıksal doğruluğu sağlaması için böyle basit adımların da kanıtlanması şarttı. Bu durum, bilimin dijitalleşmesindeki temel zorluklardan birini ortaya koyuyor.
Lean’in matematik kütüphanesinin yetersizliği, programın yaygınlaşmasını ilk etapta engelledi. Ancak 2018’den itibaren Buzzard ve diğer matematikçiler, gelişmiş matematiksel kavramlar olan “mükemmel alanlar” gibi soyut matematik terimlerini Lean’e adapte etmeye başladılar. Bu zorlu süreç, aylar süren kodlama çalışmalarıyla tamamlandı ve milyonlarca satırlık kod ortaya çıktı. Sonuçta, 2025 yılında akademi ve teknoloji alanından on binlerce kullanıcı Lean’i yoğun şekilde kullanır hale geldi. Bu artan ilgi, matematik tabanlı yapay zeka modellerinin gelişimine de önemli destek sağladı.
Lean’i geliştirenler, mutlak doğruluğa dayalı bir “gerçeklik makinesi” yaratmayı amaçladı. Bu makine, mantık zincirinin tamamen hatasız olduğunu kesin olarak garanti edebilecek bir bilgisayar programı anlamına geliyor. De Moura için bu, bilgisayar programlarının hatasız çalışmasını sağlamak ve örneğin Microsoft Word gibi programlarda hataları ortadan kaldırmak demekti. Matematikçiler içinse, Lean keşif süreçlerini çok daha titiz, düzenli ve kesin hale getiren bir araç oldu.
Kevin Hartnett’in kitabı, Lean’in ve AlphaProof gibi yapay zeka destekli çözücülerin matematiksel dünyaya nasıl entegre olduğunu anlatırken, okuyucuya yeni bir bilimsel çağın eşiğinde olunduğunu de hissettiriyor. Yapay zekanın matematikte daha derin kavrayışlara ulaşması, sadece akademik araştırmaları hızlandırmakla kalmayacak; teknoloji, mühendislik ve temel bilimlerde de radikal yeniliklerin önünü açacak. Bu gelişmelerin önümüzdeki yıllarda yapay zekanın sınırlarını genişletmesi ve insan bilgi birikimini derinlemesine etkileyerek daha önce çözülemeyen sorunlara ışık tutması bekleniyor.
📎 Kaynak: sciencenews.org
