Yapay Zeka Şimdiye Kadarki En Zorlu Matematik Kanıtını Doğrulamak İçin Kullanıldı

Yapay zeka destekli matematik araştırmalarında önemli bir dönüm noktasını temsil eden Axiom Math'daki bir ekip, şirketin yapay zeka sistemi AxiomProver'ı kullanarak asal sayılarla ilgili bir teoremin (halk dilinde "246 teoremi" olarak anılır) kanıtını ilk kez otomatik olarak doğruladı. Resmi doğrulamada, matematikçiler bir bilgisayarı bir ispatın makine tarafından okunabilir bir versiyonunu kontrol etmekle görevlendirir. Süreç, kanıtın doğru olduğuna dair yüzde 100 garanti vermiyor; yakın zamanda yapılan bir gösterinin gösterdiği gibi, yöntemdeki bir hatanın yapay zeka tarafından oluşturulan sahte bir kanıtı kabul etmek için nasıl istismar edilebileceğini ortaya koyuyor. Yine de hesaplamalı yöntem, alabildiğiniz kadar lastik damgaya yakındır. Bu özel doğrulama sayı teorisinde önemli bir ilerlemeyi resmileştiriyor. Bu özel kanıtın ötesinde, yakında dünya genelindeki yazılımların temelini oluşturacak olan yapay zeka tarafından oluşturulan bilgisayar kodunun doğruluğunu sağlamak için otomatikleştirilmiş yapay zeka doğrulamasının gelecekte nasıl kullanılabileceğini gösteriyor. Tasarım yoluyla faydalı biçimlendirme Bu, AxiomProver'ın ilk rodeosu değil. Axiom Math, çözülmemiş birçok matematik problemini çözmek için matematiksel ifadeleri makine tarafından kontrol edilebilir kanıtlara dönüştüren özerk, çok aracılı sistemini kullandı ve bu yıl çok daha fazla kanıtı doğruladı.

Ancak Axiom Math'ın kurucu matematikçisi Ken Ono'nun açıkladığı gibi, 246 teoreminin kanıt biçimlendirmesi açık ara en önemlisidir: "Bu teorem şu anda insanlığın asal sayılar hakkındaki bilgisinin eşiğini temsil ediyor." Bu yılın başlarında, Axiom Math'ın rakibi Math, Inc., Maryna Viazovska'nın 2022 Fields Madalyası kazanan küre paketleme sorununun 8 ve 24 boyuttaki kanıtını resmileştirmek için Gauss aracısını kullandı. Sidharth Hariharan, Ph.D. Viazovska'nın kanıtını resmileştirmeye yönelik plan üzerinde insani çabalara öncülük eden Carnegie Mellon Üniversitesi öğrencisi, 246 teoremini resmileştirmenin daha kapsamlı ve faydalı bir başarı olduğunu söylüyor. İLGİLİ: Matematikte Yapay Zeka-İnsan İşbirliği için Dönüm Noktası Axiom Math'da stajyer olan Hariharan, şirketin 246 teorem kanıtını resmileştirmesinde yoğun bir şekilde yer alıyor. Buradaki temel farklardan birinin, Axiom Math'ın tek bir problemle ilgili tek seferlik bir yaklaşım yerine, formalleştirmenin bileşenlerini diğer formalizasyon görevleri ve matematiksel araştırmalar için yeniden kullanılabilir hale getirmeyi açıkça amaçlamış olması olduğunu söylüyor.