Yapay zekâ, her hafta yeni bir matematik problemini çözme konusunda ilerlemeler kaydediyor. Geçtiğimiz ay OpenAI, alanın en zor problemlerine çözüm iddia eden 719 el yazması yayınladı. Ancak bu sonuçları onaylamaya yönelik bilgisayar kontrolleri bile bazen hatalı çıkabiliyor. Yıllardır süregelen 'doğrulanmamış yapay zekâ içeriği' sorununun matematiğe sıçrayıp sıçramayacağı merak konusu olurken, Axiom Math şirketi bu duruma karşı farklı bir yol izliyor. Şirket, ilerlemeyi durdurmak yerine, yapay zekâ ajanlarının güvenle yazılım yazabilmesi ve nihayetinde bilim yapması için dayanak noktaları olan, doğrulanabilir bir temel inşa etmeye odaklanıyor.
Projeyi tamamlamak için ekip, ajanlara gevşek bir yapı vererek çalışmalarını paralel yürütmelerine izin verdi. Axiom'un teknik personeli Ashvin Swaminathan, hiyerarşik bir yapı dayatılmadığını; ajanların kendi kendine görev bulup paralel çalışabilecekleri şeyleri belirlediğini ifade etti. Axiom, matematiksel yetkinlikleri artırmak için kendi modellerini eğittiklerini ve başlangıçta ev içi bir Lean uzmanından 'insan tadı' aldıklarını ancak ajanların zamanla kendi beğenilerini geliştirdiklerini açıkladı. Bu başarı, cebirsel geometri gibi daha önce Lean'de yetersiz temsil edilen alanlar için de sağlam bir zemin oluşturdu.
Stacks Projesi'nin 16 Milyon Satırda Doğrulanması
1,6 milyar dolar değerlemeye sahip Axiom Math, Çarşamba günü insanlık tarafından yazılmış en geniş kapsamlı matematik yapıtlarından biri olan Stacks Projesi'nin resmi doğrulamasını tamamladığını duyurdu. Şirketin yapay zekâ ajan filosu, bu devasa kütüphaneyi yaklaşık 7.654 sayfadan alarak yaklaşık 16 milyon satır, bilgisayar tarafından kontrol edilebilir koda dönüştürdü. Bu süreç, matematiksel yapıların altındaki mantıksal sağlamlığı garanti altına almak için kanıtların Lean programlama dilinde yeniden yazılması ve bir kanıt asistanı programıyla satır satır kontrol edilmesi prensibine dayanıyor.Matematiksel Tutarlılık ve Yapay Zekâ Agentleri
Stacks Projesi'ndeki teoremler ve tanımlar birbirine sıkı sıkıya bağlıdır; her biri kendinden önceki üzerine inşa edilir ve sonuçların birçoğu tarihsel olarak geriye doğru izlenebilir. Axiom ekibi, yaklaşık 16 milyon satır boyunca bu karmaşık bağlantıları koparmadan korumak zorunda kaldı. Şirket CEO'su Carina Hong, projenin hem büyüklüğü hem de hassasiyeti nedeniyle başlangıçta sonuçlarından emin olamadıklarını belirtti. Hong, 2005 yılında Johns de Jong tarafından açık kaynak bir referans olarak başlatılan projenin, Cullen Üniversitesi matematikçisi Peter Woit tarafından 'Bourbaki kitapları' ile karşılaştırıldığını hatırlatarak, teoremlerin tutarlı ve paradokslardan arınması gerektiğine dikkat çekti. Standford Üniversitesi matematik doktorası programından mezun olmadan ayrılıp 2025 Mart'ında şirketi kuran 25 yaşındaki Hong, Mart ayında Menlo Ventures önderliğinde 200 milyon dolarlık A turu finansman aldı.Projeyi tamamlamak için ekip, ajanlara gevşek bir yapı vererek çalışmalarını paralel yürütmelerine izin verdi. Axiom'un teknik personeli Ashvin Swaminathan, hiyerarşik bir yapı dayatılmadığını; ajanların kendi kendine görev bulup paralel çalışabilecekleri şeyleri belirlediğini ifade etti. Axiom, matematiksel yetkinlikleri artırmak için kendi modellerini eğittiklerini ve başlangıçta ev içi bir Lean uzmanından 'insan tadı' aldıklarını ancak ajanların zamanla kendi beğenilerini geliştirdiklerini açıkladı. Bu başarı, cebirsel geometri gibi daha önce Lean'de yetersiz temsil edilen alanlar için de sağlam bir zemin oluşturdu.
Webmaster
Webmaster
Webmaster
Yorumlar (0)
Yorum yapmak için giriş yapmalısınız.