Axiom Math sun'iy intellekt xatolarini oldini olish uchun insoniyatning eng yirik matematik manbasini raqamlashtirdi

Sun'iy intellekt modellari murakkab ilmiy masalalarni yechishda faollashib borayotgan bir paytda, ularning xatolari va mantiqsiz xulosalari ilm-fan sohasiga ham kirib kelishi xavfi ortmoqda. Ushbu muammoni bartaraf etish maqsadida tashkil etilgan Axiom Math startapi insoniyat tarixidagi eng yirik matematik manbalardan biri hisoblangan Stacks Project to'plamini to'liq kompyuter orqali tekshiriladigan kod ko'rinishiga o'tkazganini ma'lum qildi.

Kolumbiya universiteti olimi Yoxan de Yong tomonidan 2005-yilda ochiq manbali ma'lumotnoma sifatida boshlangan Stacks Project algebraik geometriya, sonlar nazariyasi va yuqori algebrani o'z ichiga olgan 7 654 sahifalik ulkan ilmiy merosdir. Axiom Math o'zining mustaqil ishlovchi AI agentlari tarmog'i yordamida ushbu butun to'plamni Lean dasturlash tilidagi 16 million qatorlik qat'iy mantiqiy kodga aylantirdi va uning har bir isbotini xatolardan xoli ekanini tasdiqladi.

Matematikani formalizatsiya qilish — teoremalar va ularning isbotlarini Lean kabi maxsus dasturlash tillarida yozib, ularni kompyuter dasturi orqali qatorma-qator mantiqiy to'g'riligini tekshirish jarayonidir. Stacks loyihasining murakkabligi shundaki, uning barcha tushuncha va teoremalari bir-biri bilan uzviy bog'langan bo'lib, xuddi shajara daraxti kabi bir-biriga tayanadi. Bitta xato butun zanjirni buzishi mumkin edi, ammo kompaniya agentlari barcha bog'lanishlarni to'liq saqlab qolishga muvaffaq bo'ldi.

25 yoshli Stenford aspiranti Karina Xon tomonidan 2025-yil mart oyida asos solingan Axiom Math Menlo Ventures boshchiligidagi Series A bosqichida 200 million dollar jalb qilgan edi. Kompaniya o'z modellarini maxsus matematika yo'nalishida o'qitgan bo'lib, agentlar vazifalarni avtonom tarzda parallel ravishda bajargan. Bu yutuq, ayniqsa, matematika formalizatsiyasida uzoq vaqt bo'shliq bo'lib kelgan algebraik geometriya sohasini mustahkam poydevor bilan ta'minladi.

Ushbu loyiha nafaqat akademik matematiklar, balki dasturiy ta'minot xavfsizligi sohasi uchun ham katta ahamiyatga ega. Kelajakda kodlarning katta qismini sun'iy intellekt yozishi kutilayotgan bir paytda, dasturlarning xatosiz va zaifliklardan xoli bo'lishini ta'minlashda qat'iy tekshirilgan matematik bazalar hal qiluvchi rol o'ynaydi.