Ustozlar uchun
pedagoglar.org
74-son 1–to’plam Iyun-2025
Sahifa: 132
“INFORMATIKADA SUN’IY INTELLEKT YORDAMIDA
MATEMATIK TEOREMALARNI AVTOMATIK ISBOTLASH”
Parpiyeva Dilorom Toirboyevna
Namangan viloyati Pop tumanidagi
63-sonli maktabning matematika va informatika fani o'qituvchisi
Annotatsiya
: Mazkur maqola informatika va sun’iy intellekt (SI) sohalarining
kesishgan nuqtasida joylashgan dolzarb muammoni — matematik teoremalarni avtomatik
isbotlash masalasini yoritadi. Unda avtomatik teorem isbotlash tizimlarining mantiqiy
asoslari, ishlash prinsiplari hamda mashinali o‘rganish, evristik algoritmlar va formal
tizimlar kabi SI yondashuvlari orqali qanday amalga oshirilishi tahlil qilinadi. Shuningdek,
Coq, Lean, HOL Light kabi zamonaviy platformalarning amaliy ahamiyati va ularning
ilmiy-tadqiqotda qo‘llanilishi ko‘rsatib o‘tiladi. Maqolada sun’iy intellekt yordamida
matematik tafakkurni avtomatlashtirish imkoniyatlari, bu yo‘nalishdagi so‘nggi
tadqiqotlar va istiqbolli yo‘nalishlar haqida ham fikr yuritiladi.
Kalit so’zlar:
Sun’iy intellekt, avtomatik teorem isbotlash, formal mantiq, mashinali
o‘rganish, informatika, evristik algoritmlar, matematik isbotlash, Coq, Lean,
Isabelle/HOL, AlphaTensor, kompyuter matematikasi.
Zamonaviy informatika va sun’iy intellekt sohalarining tez sur’atlar bilan rivojlanishi
matematik isbotlash jarayonlariga ham o‘z ta’sirini ko‘rsatmoqda. An’anaviy tarzda
matematik teoremalarni isbotlash — bu murakkab va ko‘p vaqt talab qiladigan jarayon
bo‘lib, yuqori darajadagi mantiqiy tafakkurni talab etadi. Biroq, sun’iy intellekt (SI) va
avtomatik isbotlash tizimlari bu sohada inqilobiy o‘zgarishlar qilishga kirishmoqda.
Avvalo "sun'iy intellekt" tushunchasining o‘zi haqida. "Sun'iy" so‘zining ma'nosi
ayon: u kelib chiqishiga ko‘ra tabiiy bo‘lmagan narsani, ya'ni, inson qo‘li bilan yaratilgan
narsalarni nazarda tutadi. "Intellekt" so‘zini esa bundayin oson ta'riflashning imkoni yo‘q.
Lug‘atlarda uning ma'nosi juda xilma-xil beriladi. Masalan, intellektni "qaror qabul qila
olish qobiliyati", "anglash qobiliyati" kabi qisqa va lo‘nda ta'riflaridan tashqari, "bilish,
idrok qilish va tahlil asosida, hamda, yig‘ilgan tajriba hamda ko‘nikmalar vositasida yangi
vaziyatlarga moslasha olish" kabi uzundan uzoq ta'riflari ham bor. Ilmiy atama holidagi
"sun'iy intellekt" tushunchasi esa ilk bora 1956-yilda, Stenford universitetida o‘tkazilgan
ilmiy anjumanda inglizcha "artificial intelligence" (AI) tarzida ilm-fanga taklif qilingan
edi. Shundan buyon mazkur tushuncha ilmiy jamoatchilik orasida mustahkam o‘rnashib
qoldi.
Sun’iy intellekt 1956-yilda akademik intizom sifatida asos solingan. Soha koʻp
optimizm davrlarini bosib oʻtdi, soʻngra umidsizlik va mablagʻ yoʻqotildi, biroq 2012-
yildan keyin chuqur oʻrganish barcha oldingi sun’iy intellekt usullaridan oshib ketganidan
Ustozlar uchun
pedagoglar.org
74-son 1–to’plam Iyun-2025
Sahifa: 133
soʻng, moliyalashtirish va qiziqishda katta oʻsish kuzatildi. Sunʼiy intellekt tadqiqotining
turli kichik sohalari ma’lum maqsadlar va muayyan vositalardan foydalanishga qaratilgan.
Sunʼiy intellekt tadqiqotlarining an’anaviy maqsadlariga fikrlash, bilimlarni taqdim etish,
rejalashtirish, oʻrganish, tabiiy tilni qayta ishlash, idrok etish va robototexnikani qoʻllab-
quvvatlash kiradi.
Sun'iy intellektning asosiy yo`nalishlari yo'nalishlari Teoremalarni isbotlash.
Teoremalarni isbotlash usullarini o'rganish sun'iy intellektni rivojlantirishda muhim rol
o'ynadi. Ko'pgina norasmiy vazifalar, masalan, tibbiy diagnostika, teoremalarni isbotlashni
avtomatlashtirish uchun ishlatilgan muammolarni echishda uslubiy yondoshuvlarni
qo'llaydi. Matematik teoremaning isbotini izlash nafaqat gipotezalarga asoslangan
chegirishni, balki asosiy teoremani umumiy isbotlash uchun oraliq bayonotlarni isbotlash
kerak bo'lgan intuitiv taxminlarni yaratishni ham talab qiladi.
Teoremalarning avtomatik isbotlari jozibador bo'lib, ular mantiqning umumiyligi va
qat'iyligiga asoslanadi. Rasmiy tizimdagi mantiq avtomatlashtirish imkoniyatini anglatadi,
ya'ni agar biz muammoni va u bilan bog'liq qo'shimcha ma'lumotlarni mantiqiy aksiomalar
to'plami shaklida taqdim etsak va muammoning maxsus holatlarini isbot talab qiladigan
teoremalar sifatida taqdim etsak, ko'pgina muammolarni hal qilishimiz mumkin.
Matematik asoslash tizimlari va teoremalarni avtomatik tasdiqlash tizimlari ushbu
printsipga asoslanadi.
O'tgan yillarda teoremalarni avtomatik isbotlash uchun dastur yozishga bir necha bor
urinish bo'lgan, ammo bitta usul yordamida muammolarni echishga imkon beradigan
tizimni yaratish mumkin emas edi. Har qanday nisbatan murakkab evristik tizim
ahamiyatsiz bo'lgan juda ko'p isbotlangan teoremalarni keltirib chiqarishi mumkin edi,
natijada dasturlar zaruriyat topilgunga qadar ularni isbotlashi kerak edi. Shu sababli, katta
bo'shliqlar bilan faqat muayyan holatlar uchun maxsus ishlab chiqilgan norasmiy
strategiyalar yordamida ishlashingiz mumkin degan fikr paydo bo'ldi. Amalda, bu
yondashuv juda samarali bo'lib chiqdi va boshqalar qatori ekspert tizimlari asosiga qo'yildi.
Ammo rasmiy mantiqqa asoslangan mulohazalarni e'tiborsiz qoldirib bo'lmaydi.
Rasmiy yondoshish ko'plab muammolarni hal qilishga imkon beradi. Xususan, undan
foydalangan holda murakkab tizimlarni boshqarish, kompyuter dasturlarining to'g'riligini
tekshirish, mantiqiy zanjirlarni loyihalash va tekshirish mumkin. Bundan tashqari,
teoremalarni avtomatik isbotlash tadqiqotchilari mantiqiy ifodalarning sintaktik shaklini
baholashga asoslangan kuchli evristikani ishlab chiqdilar. Natijada, maxsus strategiyalarni
ishlab chiqishga murojaat qilmasdan qidirish maydonining murakkabligini kamaytirish
mumkin bo'ldi.
Teoremalarning avtomatik isbotlanishi olimlarni qiziqtiradi, shuning uchun juda
murakkab muammolar uchun odamning aralashuvisiz ham tizimdan foydalanish mumkin.
Hozirgi vaqtda dasturlar ko'pincha yordamchilar sifatida ishlaydi. Mutaxassislar vazifani
bir nechta pastki qismlarga ajratishadi, so'ngra evristik nuqtai nazardan yuzaga keladigan
Ustozlar uchun
pedagoglar.org
74-son 1–to’plam Iyun-2025
Sahifa: 134
sabablarni aniqlashga harakat qilinadi. Bundan tashqari, dastur lemmani isbotlaydi,
unchalik muhim bo'lmagan taxminlarni tasdiqlaydi va inson tomonidan tasdiqlangan
dalillarning rasmiy jihatlariga qo'shimchalar kiritadi.
Avtomatik teorem isbotlash (ATP) — bu kompyuter dasturlari yordamida matematik
teoremalarni formal mantiq asosida avtomatik tarzda isbotlash jarayonidir. Bu tizimlar
inson aralashuvisiz yoki minimal ishtirokida, mantiqiy qoidalarga tayangan holda isbot
chiqarish qobiliyatiga ega.
ATP ning Asosiy Elementlari
Formal til: Teoremalar va isbotlar qat’iy formal tillarda (masalan, birinchi tartibli
mantiq) yoziladi.
Qoidalar majmuasi: Mantiqiy inferensiya qoidalari asosida isbot hosil qilinadi.
Qidiruv strategiyalari: Isbot topish uchun evristik yoki algoritmik yondashuvlar
qo‘llaniladi.
SI va ML algoritmlari: Oxirgi yillarda sun’iy intellekt elementlari isbotlash
samaradorligini oshirish uchun integratsiya qilinmoqda.
Bugungi kunda ATP sistemalari fizika, informatika, kriptografiya va hatto
farmatsevtikani o‘rganishda muhim rol o‘ynamoqda. Masalan
, Lean
va
Metamath
kabi
platformalar ko‘plab klassik teoremalarni SI yordamida avtomatik isbotlay oldi. 2020-
yilda Google DeepMind tomonidan ishlab chiqilgan
"AlphaTensor"
loyihasi esa SI
asosidagi matematik optimallashtirishga yangi yondashuvni taklif qildi.
Quyida sun’iy intellekt yordamida matematik teoremalarni isbotlashga oid bir
nechta mashhur misollarni keltiraman:
1.
Four Color Theorem (To‘rt rang teoremasi) Bu teorema har qanday tekis
xaritani atigi to‘rt xil rang bilan bo‘yash mumkinligini isbotlaydi. 1976-yilda Kenneth
Appel va Wolfgang Haken bu teoremaga kompyuter yordamida isbot keltirishdi. Bu
tarixda birinchi marta kompyuter yordamida isbotlangan mashhur teorema bo‘lib, sun’iy
intellektning ilk amaliy yutuqlaridan biri hisoblanadi.
2.
Kepler Conjecture (Kepler taxmini) Bu taxmin eng zich sharlar joylashuvi
haqida bo‘lib, 1998-yilda Thomas Hales tomonidan isbotlandi. Biroq, isbot juda murakkab
bo‘lgani uchun 2014-yilda HOL Light va Isabelle kabi formal tizimlar yordamida sun’iy
intellekt asosida isbot to‘liq formalizatsiya qilindi.
3.
Lean Prover va Perfectoid Spaces Matematik Peter Scholze va Kevin Buzzard
2020-yilda Lean formal tizimi yordamida algebraik geometriyadagi murakkab
tushunchalarni formal isbotlashga kirishishdi. Bu loyiha sun’iy intellekt yordamida
zamonaviy matematikani formalizatsiya qilish yo‘lida muhim qadam bo‘ldi.
4.
DeepMind’ning AlphaTensor loyihasi 2022-yilda DeepMind kompaniyasi
AlphaTensor nomli sun’iy intellekt tizimini yaratdi. Bu tizim chiziqli algebra
Ustozlar uchun
pedagoglar.org
74-son 1–to’plam Iyun-2025
Sahifa: 135
muammolarini, xususan, matritsalarni ko‘paytirish algoritmlarini optimallashtirish orqali
matematik isbotlashga yangi yondashuv taklif qildi.
Sun’iy intellekt yordamida matematik teoremalarni avtomatik isbotlash
informatikaning eng istiqbolli yo‘nalishlaridan biri bo‘lib, u matematik tafakkur jarayonini
chuqur formal tahlil qilish imkonini yaratmoqda. Avtomatik teorem isbotlash (ATP)
tizimlari formal mantiq asosida ishlash bilan birga, mashinali o‘rganish, evristik izlash va
boshqa ilg‘or SI yondashuvlari bilan boyitilmoqda. Coq, Lean, Isabelle/HOL, HOL Light
kabi platformalar matematik isbotlarni nafaqat avtomatlashtiradi, balki ularning aniqligi
va ishonchliligini ham oshiradi. Bu texnologiyalar nafaqat akademik doirada, balki sanoat,
kriptografiya va dasturiy ta'minot xavfsizligi kabi real sohalarda keng qo‘llanilmoqda.
Xulosa qilib aytganda, sun’iy intellekt bilan integratsiyalashgan matematik isbotlash
texnologiyalari kelajakda ilm-fan taraqqiyotining muhim omillaridan biriga aylanishi
kutilmoqda.
Foydalanilgan adabiyotlar:
1.
Russell, S., & Norvig, P. (2020). Artificial Intelligence: A Modern Approach (4th
ed.). Pearson.
2.
Harrison, J. (2009). Handbook of Practical Logic and Automated Reasoning.
Cambridge University Press.
3.
Nipkow, T., Paulson, L. C., & Wenzel, M. (2002). Isabelle/HOL: A Proof Assistant
for Higher-Order Logic. Springer.
4.
Avigad, J., & Harrison, J. (2014). Formally Verified Mathematics. Communications
of the ACM, 57(4), 66–75.
5.
Hales, T. C. et al. (2017). A Formal Proof of the Kepler Conjecture. Forum of
Mathematics, Pi, 5, e2
6.
Gonthier, G. (2008). Formal Proof—The Four-Color Theorem. Notices of the AMS,
55(11), 1382–1393.
7.
Geuvers, H. (2009). Proof Assistants: History, Ideas and Future. Sadhana, 34(1), 3–
25.
8.
DeepMind’s AlphaTensor project — sun’iy intellekt yordamida matematik
algoritmlarni optimallashtirish bo‘yicha zamonaviy tadqiqot.
9.
O‘zbekiston axborot texnologiyalari va kommunikatsiyalarini rivojlantirish vazirligi:
Sun’iy intellekt va teoremalarni isbotlash — mahalliy kontekstda sun’iy intellektning
qo‘llanilishi haqida.
