Yapay zeka girişim şirketi «Axiom Math», bağımsız ajanlardan oluşan sisteminin, matematikçiler tarafından tarih boyunca yazılmış en büyük açık matematik referanslarından biri olan «Stacks Project»'in (Stacks Projesi) tüm içeriğini resmi ve yazılımsal olarak (Formal Verification) başarıyla doğruladığını açıkladı.
Matematiksel Bilginin Denetlenebilir Koda Dönüştürülmesi
Columbia Üniversitesi matematik profesörü Johan de Jong tarafından 2005 yılında başlatılan Stacks Project, cebir ve cebirsel geometri ilkelerinden sayı teorisindeki gelişmiş teorilere kadar yaklaşık 7.654 sayfa içermektedir. Axiom Math'ın ajan sürüleri, bu karmaşık ve birbirine bağlı metinleri, denetim yazılımlarının katı mantıksal güvenilirliği sağlamak için her bir matematiksel kanıtı satır satır incelemesine olanak tanıyan özel bir programlama dili olan «Lean» dilinde yaklaşık 16 milyon satırlık kod halinde çevirmeyi başardı.
Menlo Ventures liderliğinde ilk tur finansmanda 200 milyon dolar toplayarak 1,6 milyar dolar piyasa değerine ulaşan şirket, yapay zeka sistemlerinin gelecekte yazılım geliştirme ve bilimsel araştırmalarda güvenle dayanabileceği, «AI slop» (yapay zeka döküntüsü) olarak bilinen yanıltıcı veya yanlış çıkarımlar üretmekten kaçınan güvenilir ve yazılımsal olarak kanıtlanmış bir bilgi tabanı oluşturmayı hedefliyor.
Axiom'u Mart 2025'te kurmak için Stanford Üniversitesi'ndeki matematik doktora programından ayrılan 25 yaşındaki kurucu ve CEO Karina Hong, en büyük zorluğun binlerce teorinin birbirine bağlılığını korumak ve herhangi bir kavramsal çelişkiden kaçınmak olduğunu belirtti. Şirketin teknik ekip üyesi Ashvin Swaminathan ise yapay zeka ajanlarının her adım için doğrudan rehberlikle çalışmadığını, bunun yerine görevleri paralel olarak dağıtmalarına ve genel kod üretme modellerine güvenmek yerine doğru matematiksel akıl yürütme konusunda eğitilmiş özel modellerden yararlanmalarına olanak tanıyan esnek bir hiyerarşik yapı verildiğini belirtti.
Bu Başarı Teknoloji Sektörü İçin Ne Anlama Geliyor?
Bu gelişme, özellikle cebirsel geometri gibi alanlarda matematiğin bilgisayar aracılığıyla kanıtlanmasındaki büyük bir boşluğu kapatmak için pratik bir adım teşkil etmektedir. Biçimsel doğrulamanın faydası akademisyenlerle sınırlı değildir; kanıtların bilgisayar kodları aracılığıyla belgelenmesi, yeniden kullanılabilir temel bir ortam sağlar. Şirket, geliştiricilerin ve çip tasarımı ile kritik sistemlerin hesaplanması gibi hassas yazılımların geliştiricilerinin, yazılım yazmada ajanlara artan güvenin neden olduğu güvenlik açıklarını ve gizli hataları önlemek için bu doğrulanmış kurallara ihtiyaç duyacağına bahse giriyor.