Süni intellekt riyaziyyatçıları əvəz edə bilirmi?
İsbat etməyi bacaran maşınların yüksəlişi
Riyaziyyat uzun müddət insan zəkasının ən yüksək sahələrindən biri sayılıb. Kömpüter çox sahədə insanı üstələməyə başlasa da ( məsələn, çətin şahmat oyununda), riyazi isbatı bacarmaq başqa səviyyə hesab olunurdu. Çünki burada yalnız hesablamalar deyil, məntiqi quruluş, struktur hissiyyatı və yaradıcı yanaşma tələb olunur.
Son illərdə isə vəziyyət dəyişməyə başlayıb.
İsbat nədir və niyə çətindir?
Riyaziyyatda isbat – müəyyən mülahizənin (teorem və ya lemma) doğruluğunu aksiomlara və əvvəlcədən isbat olunmuş nəticələrə əsaslanaraq məntiqi ardıcıllıqla göstərməkdir.
Bu, sadəcə nəticəni hesablamaq deyil. İsbat düzgün istiqaməti seçməyi, uyğun aralıq nəticələri tapmağı, məntiqi boşluq buraxmamağı tələb edir.
Məsələn, “sonsuz sayda sadə ədəd var” ifadəsi intuitiv görünsə də, onun isbatı yaradıcı konstruksiya tələb edir. Bu səbəbdən uzun müddət düşünülürdü ki, isbat qurmaq insan düşüncəsinə məxsus fəaliyyət olaraq qalacaq.
Formal isbat sistemləri
Son onillikdə əsas dönüş formal isbat sistemlərinin inkişafı ilə baş verdi. Bu sistemlər riyaziyyatı tam formal dilə çevirir və hər məntiqi addımı kompüter tərəfindən yoxlanıla bilən hala gətirir.
Məsələn, Lean və Coq kimi sistemlərdə:
Teoremlər formal sintaksis ilə yazılır,
Hər addım məntiq qaydalarına görə yoxlanılır,
Qeyri-dəqiq “intuitiv keçidlər” mümkün olmur.
Əvvəlcə bu sistemlər yalnız isbatları yoxlamaq üçün istifadə edilirdi. İndi isə onlar isbatın qurulmasında da aktiv rol almağa başlayıb.
Süni intellektin rolu
Burada əsas sıçrayış böyük dil modellərinin və maşın öyrənməsinin tətbiqi ilə baş verdi. Xüsusilə DeepMind tərəfindən hazırlanan sistemlər formal riyazi mühitlərdə öyrədilərək isbat strategiyalarını mənimsədi.
Bu sistemlər:
- Hansı lemmanın tətbiq ediləcəyini proqnozlaşdırır,
- Növbəti məntiqi addımı təklif edir,
- Bəzən ispatın ümumi strukturunu qurur.
Artıq müəyyən səviyyəli məsələlər tam avtomatik şəkildə isbat edilə bilir.
Bu, sadəcə sürətli hesablama deyil – bu, məntiqi qərarvermənin avtomatlaşdırılmasıdır.
İnsan və maşın əməkdaşlığı
Vacib məqam ondan ibarətdir ki, süni intellekt hələ müstəqil riyaziyyatçı deyil. O, yeni nəzəri çərçivə yaratmır, problemin fəlsəfi istiqamətini seçmir, konseptual sıçrayış etmir.
Amma o, çox güclü texniki tərəfdaşdır.
Riyaziyyatçı ideyanı və strategiyanı qurur. Süni intellekt isə, uzun formal detalları işləyir, alternativ yollar sınayır, səhvləri aşkar edir, böyük isbatları formal şəkildə təsdiqləyir.
Bu model artıq real tədqiqat mühitində tətbiq olunur.
Bu nəyi dəyişir?
Böyük və mürəkkəb nəticələrin səhvsiz formal təsdiqi mümkün olur.
İsbatın texniki hissəsi avtomatlaşır.
Riyaziyyatın iş tempi arta bilər.
Təhsildə formal məntiqə diqqət güclənir.
Bəzi alimlər bunu riyaziyyatın yeni mərhələsi kimi qiymətləndirirlər.
Ən maraqlı sual budur: süni intellekt gələcəkdə özü yeni fərziyyə irəli sürə bilərmi?
Hazırda sistemlər mövcud strukturlar daxilində işləyir. Lakin məlumat və formal baza böyüdükcə, struktur analizi yolu ilə yeni qanunauyğunluqlar aşkar etmək ehtimalı artır.
Bununla belə, konseptual yaradıcılıq hələ də insanın əsas üstünlüyü olaraq qalır.
Süni intellekt riyaziyyatçını əvəz etmir, lakin riyaziyyatın aparılma üsulunu dəyişir. Əgər XX əsr abstraksiyanın dərinləşməsi ilə xarakterizə olunurdusa, XXI əsr insan və maşının birgə intellektual əməkdaşlığı ilə yadda qala bilər.
Bu artıq nəzəri ehtimal deyil – proses başlayıb.