DeepMind, yeni yapay zekâsı AlphaProof Nexus’ın daha önce çözülememiş çeşitli matematik soruları için biçimsel kanıtlar ürettiğini duyurdu. Sonuçlar, Science dergisinde yayımlanan hakem değerlendirmesinden geçmiş bir makalede yer alıyor. Sistem, Lean biçimsel dilinde kanıtlar yazmak için Gemini 3.1 Pro’yu kullanıyor ve her adımı otomatik olarak denetliyor.
AlphaProof Nexus neler başardı?
Makaleye göre AlphaProof Nexus, hâlâ açık olarak listelenen 353 Erdős probleminden dokuzunu çözdü; bunlardan ikisi 56 yıldır çözülememişti. Sistem ayrıca OEIS tam sayı dizileri veri tabanındaki 44 varsayımı kanıtladı, cebirsel geometride açık bir soruyu çözdü ve bazı yapay zekâ modellerinin eğitiminde kullanılan bir yöntem olan min-maks optimizasyonundaki bilinen bir sınırı iyileştirdi.
Sistem nasıl çalışıyor?
AlphaProof Nexus, Lean’de kanıt taslakları hazırlayan ve Lean doğrulayıcısından anında geri bildirim alan Gemini 3.1 Pro’yu temel alıyor. Taslak başarısız olduğunda Lean, sonraki denemeye yön veren bir hata mesajı veriyor. Özellikle zor alt problemler için sistem, AlphaProof adlı özel bir aracı devreye sokabiliyor. Ekip, makale yayımlanmadan önce dokuz Erdős problemine ilişkin çözümleri çevrimiçi olarak paylaştı.
Neden önemli
Matematikçiler için bu yapay zekâ, zor problemleri araştırmanın ve kanıtları otomatik olarak doğrulamanın yeni bir yolunu sunarak araştırmaları hızlandırabilir. Yapay zekâ araçlarını kullanan herkes içinse min-maks optimizasyonundaki iyileşme, gelecekteki modellerin daha verimli eğitilmesine katkıda bulunabilir. Çalışmanın hakem değerlendirmesinden geçerek yayımlanması, yapay zekâ tarafından üretilen kanıtların bilim dünyasında ciddiye alındığını gösteriyor; ancak daha geniş kapsamlı doğrulama hâlâ gerekiyor.
