Axiom Math, Stacks Project kütüphanesini doğrulamak için yapay zeka ajanlarını kullandı

Girişim şirketi Axiom Math, matematiksel kanıtları otomatik olarak doğrulamak için tasarlanmış bir yapay zeka ajanı sistemi tanıttı. Geliştiriciler, binlerce sayfalık teorik hesaplama içeren dünyanın en büyük cebirsel geometri kütüphanelerinden biri olan Stacks Project'in biçimsel doğrulamasını başarıyla tamamladı.

Şirketin teknolojisi, modern dil modellerinin ürettiği "matematiksel çöpler" sorununu çözmeyi hedefliyor. Standart LLM'lerin aksine, Axiom Math ajanları, bir kanıttaki her adımın doğruluğunu matematiksel olarak teyit etmeye olanak tanıyan biçimsel doğrulama yöntemlerini kullanıyor. Bu, olasılıksal modellere özgü mantıksal hataların veya halüsinasyonların ortaya çıkma olasılığını ortadan kaldırıyor.

Matematikte biçimsel yöntemlerin kullanımı, Lean veya Coq gibi kanıt doğrulama sistemleri için kod yazmanın zahmetli bir süreç olması nedeniyle geleneksel olarak bilim insanlarından büyük miktarda zaman talep ediyordu. Girişimin ajanları, doğal matematik dilini katı bir doğrulama için uygun, makine tarafından okunabilir bir formata dönüştürerek bu aşamayı otomatikleştiriyor.

Matematik topluluğu için bu, yeni hipotezlerin hızlı bir şekilde doğrulanması ve mevcut çalışmaların gizli hatalar açısından kontrol edilmesi anlamına geliyor. Bu tür araçların benimsenmesi, araştırmacıların akademik titizliği ve sonuçların güvenilirliğini korurken keşifleri hızlandırmak için yapay zekanın gücünden yararlanmalarına olanak tanıyor.