Axiom Math sun'iy intellekt xatolarini oldini olish uchun insoniyatning eng yirik matematik manbasini raqamlashtirdi
Bahosi 1,6 milliard dollarga baholangan Axiom Math startapi insoniyat tarixidagi eng yirik matematik to'plamlardan biri bo'lgan Stacks Project loyihasini to'liq rasmiy tekshiruvdan (formal verification) o'tkazdi. Kompaniyaning AI agentlari 7 654 sahifalik murakkab matematik matnni 16 million qatorli Lean kodiga aylantirib chiqdi. Bu yutuq matematikada sun'iy intellekt tomonidan yaratiladigan xatoliklar va qalbaki ma'lumotlar (AI slop) tarqalishining oldini olishga qaratilgan. Loyiha nafaqat sof fanda, balki kelajakda dasturiy ta'minot xavfsizligini ta'minlashda ham muhim poydevor vazifasini bajaradi.
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.
Dasturchilar va ilmiy tadqiqotchilar Lean orqali to'liq tekshirilgan ushbu ulkan ochiq matematik bazadan ishonchli algoritmlar, xatosiz kodlar va xavfsiz tizimlarni qurishda poydevor sifatida foydalanishlari mumkin.