Beş yıl önce matematikçiler Dawei Chen ve Quentin Gendron, eğri yüzeyler boyunca mesafeyi ölçmek için kullanılan kalkülüs unsurları olan diferansiyelleri içeren cebirsel geometrinin zor bir alanını çözmeye çalışıyordu. Bir teorem üzerinde çalışırken beklenmedik bir engelle karşılaştılar: Argümanları sayı teorisinden gelen tuhaf bir formüle dayanıyordu ancak bunu ne çözebildiler ne de gerekçelendirebildiler. Sonunda Chen ve Gendron fikirlerini bir teorem yerine varsayım olarak sunan bir makale yazdı.
Chen kısa süre önce hâlâ çözülmemiş probleme çözüm bulması umuduyla ChatGPT’ye saatlerce komut verdi ancak sonuç alamadı.
Geçen ay Washington, DC’de düzenlenen bir matematik konferansındaki resepsiyonda Chen, yakın zamanda Virginia Üniversitesi’ndeki görevinden ayrılarak öğrencilerinden Carina Hong’un kurucu ortaklarından olduğu yapay zeka girişimi Axiom’a katılan tanınmış matematikçi Ken Ono ile karşılaştı.
Chen problemi Ono’ya anlattı ve ertesi sabah Ono, girişimin matematik çözen yapay zekası AxiomProver’ın sağladığı bir ispatı ona sundu. İspatı kaleme almak için Axiom ile birlikte çalışan Chen, çalışmanın akademik makaleler için halka açık bir arşiv olan arXiv’e yüklendiğini belirtiyor. “Ondan sonra her şey doğal bir şekilde yerine oturdu.” diyor.
Axiom’un yapay zeka aracı, problem ile ilk kez 19. yüzyılda incelenen sayısal bir fenomen arasında bağlantı buldu. Ardından ispat geliştirdi ve bunu kendi kendine doğruladı. Ono, WIRED’a “AxiomProver’ın bulduğu şey, insanların kaçırdığı bir şeydi.” dedi.
Söz konus ispat, Axiom’un sisteminin son haftalarda ortaya koyduğunu söylediği çözüm serisinin yalnızca biri. Yapay zeka henüz matematiğin en ünlü (ya da en kazançlı) problemlerini çözmedi ancak farklı alanlarında uzman kişileri yıllardır zorlayan sorulara yanıtlar buldu. İspatlar, yapay zekanın giderek gelişen matematik yeteneklerinin kanıtı niteliğinde. Son aylarda başka matematikçiler de yeni fikirleri keşfetmek ve mevcut problemleri çözmek için yapay zeka araçlarını kullandıklarını bildirdi.
Axiom tarafından geliştirilen teknikler, ileri matematik dünyasının dışında da yararlı olabilir. Örneğin aynı yaklaşımlar, belirli tür siber güvenlik saldırılarına karşı daha dayanıklı yazılımlar geliştirmek için kullanılabilir. Bu, kodun kanıtlanabilir biçimde güvenilir ve güvene değer olduğunu doğrulamak için yapay zekanın kullanılmasını içerir.
Axiom’un CEO’su Hong, “Matematik gerçekten gerçekliğin büyük test alanı ve oyun sahasıdır. Yüksek ticari değere sahip oldukça önemli birçok kullanım alanı olduğuna inanıyoruz.” diyor.
Axiom’un yaklaşımı, büyük dil modellerini, matematik problemleri üzerinde mantık yürüterek kanıtlanabilir biçimde doğru çözümlere ulaşmak üzere eğitilmiş özel bir yapay zeka sistemi olan AxiomProver ile birleştirmeyi içeriyor. Google da, 2024’te AlphaProof adlı bir sistemle benzer bir fikri göstermişti. Hong, AxiomProver’ın Google’dan birkaç önemli ilerleme ve daha yeni teknik içerdiğini söylüyor.
Ono, Chen-Gendron varsayımı için üretilen yapay zeka kaynaklı ispatın, yapay zekanın artık profesyonel matematikçilere anlamlı biçimde yardımcı olabildiğini gösterdiğini söylüyor.
Axiom’un sistemi, Lean adı verilen özel bir matematik dili kullanarak ispatları doğrulayabildiği için sıradan bir yapay zeka modelinden daha fazlası. Böylelikle AxiomProver yalnızca literatürde arama yapmak yerine problemlere gerçekten yeni çözüm yolları geliştirebiliyor.
AxiomProver tarafından üretilen yeni ispatlardan bir diğeri, yapay zekanın matematik problemlerini tamamen kendi başına çözebildiğini gösteriyor. Yine arXiv’e yüklenen bir makalede açıklanan ispat, cebirde sayıların hizalandığı matematiksel ifadeler olan sizijilerle ilgili Fel Varsayımı’na çözüm sunuyor. Dikkat çekici şekilde söz konusu varsayım, 100 yılı aşkın süre önce efsanevi Hintli matematikçi Srinivasa Ramanujan’ın defterinde bulunan formülleri içeriyor. Bu durumda AxiomProver yalnızca eksik bir parçayı tamamlamadı, ispatı baştan sona geliştirdi.
Harvard Business School’da profesör olan ve hem Fel Varsayımı’nı hem de Axiom’un teknolojisini bilen Scott Kominers, “Yıllardır yapay zeka matematik araçlarının evrimini yakından izleyen ve onlarla çalışan biri olarak bunu oldukça şaşırtıcı buluyorum. AxiomProver’ın böyle bir problemi tamamen otomatik ve anında doğrulanmış şekilde çözmesi tek başına etkileyici; ayrıca ürettiği matematiğin zarafeti ve güzelliği de öyle.” diyor.
Axiom’un yapay zekası tarafından üretilen üçüncü ispat, sayı teorisindeki sözde “çıkmazlar”ın olasılıksal bir modelini içeriyor. Dördüncü ispat ise başlangıçta Fermat’nın Son Teoremi’ni çözmek için geliştirilen matematiksel araçlara dayanıyor.
Ono, AxiomProver’ın yalnızca matematikçilere yardımcı olmakla kalmayıp, yeni keşiflerin nasıl yapıldığına dair daha temel bir şeyi de ortaya koymasını umduğunu söylüyor.
Kaynak: https://www.wired.com/story/a-new-ai-math-ai-startup-just-cracked-4-previously-unsolved-problems/
