Google’ın yapay zekâsı 56 yıldır açık olan matematik problemlerini birkaç yüz dolara çözdü

Google DeepMind’ın bir araştırma sistemi, matematikçi Paul Erdős’un ortaya attığı dokuz açık problem için makineyle doğrulanmış tam ispatlar üretti; bunların ikisi 56 yıldır çözülememişti. Aynı sistem, Tam Sayı Dizileri Çevrimiçi Ansiklopedisi’nden alınan 44 sanıyı kapattı, cebirsel geometride 15 yıldır açık duran bir soruyu çözdü ve dışbükey optimizasyonda bilinen bir sınırı daraltdı. Dikkat çeken sayı, yöntemden daha az önemli. Bu ispatların her biri yalnızca bir makine tarafından öne sürülmedi, bir makine tarafından doğrulandı.

1996’da ölen Erdős, geride yüzlerce kesin ve inatçı soru bıraktı; çoğu söylemesi kolay, kapatması korkunç zor. Onlarca yıl içinde bunlar alanın kalıcı bir sınavına dönüştü. Dizi sanıları, matematikçilerin örüntü aradığı, tahmin edilen bir formülün yıllarca kanıtlanmadan kalabildiği halka açık bir veritabanından geliyor. Bir modeli pohpohlamak için kurgulanmış testler değil bunlar. Açık matematiğin gerçek birikmiş işi.

İşte bu ayrım, hikâyenin tamamı. AlphaProof Nexus adlı sistem, argümanlarını, doğrulayamadığı her adımı reddeden biçimsel bir dil olan Lean’de yazıyor. Bir ispat ya geçer ya geçmez; sonradan yanlış çıkan kendinden emin bir paragrafa yer yoktur. Bir yapay zekâ ‘keşfinin’ gerçek olup olmadığını tartmak isteyen için, basın bülteni ile sonuç arasındaki sınır tam burası.

Önerilen OkumalarZehirli bir VS Code eklentisi GitHub’ın 3.800 iç deposunu çaldı

Kaputun altında ispatlayıcı, Gemini 3.1 Pro üzerinde çalışıyor; sıralama işini daha hafif bir model üstleniyor. Döngü neredeyse sıkıcı. Model Lean’de bir ispat taslağı yazıyor, derleyici hataları geri veriyor ve o hatalar bir sonraki denemeyi besliyor. Dürüstlüğü ayakta tutan, akıcı düzyazı değil, simgesel geri bildirim. Ekip, biri rakip ispat taslakları üretip sıralayabilen, karmaşıklığı giderek artan dört sürüm kurdu. Yine de en yalın sürüm, salt model ile derleyiciden oluşan döngü, dokuz Erdős probleminin hepsini tek başına çözdü.

Sessizce şaşırtan kısım, ekonomisi. Çözülen her problem, hesaplama süresinde birkaç yüz dolara mal oldu. Kariyerleri yutmuş sorular, aşağı yukarı bir hafta sonu kaçamağının fiyatına kapandı. Bu, matematikçiyi emekliye ayırmıyor. Hangi problemlerin saldırmaya değer olduğunu seçmek, onları sistemin okuyabileceği bir biçimde kurmak ve bir cevabın ne anlama geldiğine karar vermek hâlâ birine düşüyor. Değişen şey, neyin denemeye değer olduğunun hesabı.

Çekinceler başlıktan ağır basıyor. Denenen 353 Erdős probleminden dokuzunun çözülmesi, yaklaşık yüzde 2,5’lik bir isabet oranı. Dizilerdeki sayı, 492’de 44, yüzde dokuzun altında. Yazarlar açıkça, bu problemlerin çoğunun hâlâ erişilemez olduğunu, kapsamlı yeni kuram gerektirenlerin ise daha da öyle olduğunu ve başarıların Lean’in matematik kütüphanesinin zaten derin olduğu alanlarda toplandığını söylüyor. İnsan eliyle kurulan o iskeleyi ve özenle seçilmiş hedef listesini kaldırın, sisteme basacak pek az yer kalır.

İhtiyat hak edilmiş. Çokça alay konusu olan bir olayda, rakip bir laboratuvar modelinin on Erdős problemini çözdüğünü duyurdu; ta ki matematikçiler cevapların zaten yayımlanmış literatürde bulunduğunu gösterene dek. Model onları bulmuştu, kanıtlamamıştı. AlphaProof Nexus, tam da bu hataya bağışık olacak biçimde kuruldu. Bilinen bir sonucun Lean’deki ispatı hâlâ geçerli bir ispattır ve gerçekten yeni bir şeyin Lean’deki ispatı blöfle üretilemez. DeepMind’ı yöneten Demis Hassabis, çalışmanın genel yapay zekâ olmadığını özellikle belirtti; modelleri konusunda nadiren çekingen olan bir şirket için alışılmadık derecede temkinli bir not.

Araştırmacıların altını çizdiği daha incelikli bir kazanç da var. Başarısızlıklar bile işe yaradı. Her kısmi ispat biçimsel olarak doğrulandığı için, matematikçiler tüm argümanı elle yeniden denetlemeden, sistemin hangi alt hedefleri kapatabildiğini, hangilerini kapatamadığını tam olarak görebildi. Makine bir kâhin olmaktan çıkıp, işini gösteren ve zor kısmın hâlâ nerede saklandığını işaret eden yorulmak bilmez bir iş arkadaşına dönüşüyor.

Sonuç tek başına durmuyor. Rakip bir akıl yürütme modelinden gelen ayrı bir iddiayla aynı döneme denk geliyor; bu modelin, ayrık geometride yaklaşık 80 yıllık bir Erdős sanısını çürüttüğü bildirildi ve bulguyu çalışan matematikçiler inceltip onayladı. İki laboratuvar, iki yöntem; biri biçimsel doğrulamaya, öteki ham akıl yürütme zincirlerine yaslanarak, haftalar arayla aynı sınıra ulaştı. Yarış artık zekiymiş gibi konuşan sohbet botlarıyla ilgili değil.

Çalışma, bu ay yayımlanan bir makalede ayrıntılandırıldı ve yöntemler açık araçlara, yani Lean’e ve topluluğun kurduğu kütüphaneye dayanıyor; böylece dışarıdaki gruplar bir şirket bloguna inanmak yerine ispatları inceleyip yeniden çalıştırabilir. DeepMind, sistemin şirket dışındaki araştırmacılara ulaşıp ulaşmayacağını söylemedi. İzlenmesi gereken sayı dokuz değil. O yüzde 2,5’in ona, sonra yirmiye çıkıp çıkmayacağı; çünkü o gün geldiğinde, bu makinelerin ne işe yaradığına dair tartışma baştan başlamak zorunda kalacak.

Buna benzer içerikler

Yapay zekâ ile inşa edilen 380.000 uygulamanın taraması, binlercesinde hiçbir kimlik doğrulamasının bulunmadığını ortaya çıkardı

Google’ın yeni Android asistanı alışveriş listenizi kendiliğinden sepete kopyalıyor

Advantech, Snapdragon X Elite Gücüyle Endüstriyel Yapay Zekada Çıtayı Yükseltiyor

Spotify Premium 1.400 Peloton antrenmanını ücretsiz aldı — bisiklete gerek yok

DJI Osmo Pocket 4 dünyaya çıktı — ABD’de resmi satış yasak

Google’ın Gemini Spark’ı dizüstü kapatıldıktan sonra da çalışmaya devam ediyor — ücretli beta 26 Mayıs haftası başlıyor