Ավտոմատ թեորեմների ապացուցում

Մի քանի տասնամյակ առաջ 1950 թվականից սկսած՝ մարդիկ փորձել են գրել համակարգչային ծրագրեր, որոնք կարող են գտնել մաթեմատիկական արտահայտությունների ապացույցներ։ Եղել են որոշ ուշագրավ հաջողություններ ինչպիսին է եղել՝ Ռոբինի վարկածի (Robbin’s conjecture) ապացույցը 1997 թվականին համակարգչի միջոցով։

¬ (¬ (a ∨ b) ∨ ¬ (a ∨ ¬b)) = a

Ընդհանուր առմամբ առաջընթացը հիասթափեցնող է։ Խնդիրների որոշակի դասի համար մենք կարծես փակուղու մեջ լինենք, որոնք լուծելի են թվում միայն մարդկանց սրամտության շնորհիվ։ Ավտոմատ թեորեմների ապացուցման երկու հիմնական ձև կա։ Մարդկային ուղղվածություն (human-oriented approach) ունեցող մոտեցում, որը համակարգիչը սերտորեն փորձում է ըդնօրինակել՝ այն ճանապարհը, որով մարդը ապացույց կգտնի, և մեքենայական մոտեցումը (machine-oriented approach), որը նպատակ ունի գերազանցել այն, ինչ մարդիկ կարող են անել՝ օգտագործելով համակարգիչների հսկայական գերազանցությունը և հիշողությունը։ Ներկայումս մեքենայական մոտեցումը ավելի նորաձև է և գրավիչ, բայց դե փակուղուց դուրս գալու համար պետք է վերադառնալ մարդկային ուղղվածության (human-oriented approach)։

Այսօր մարդիկ ձգտում են փակուղուց դուրս գալ մեքենայական ուղղվածությունը (machine-oriented approach) զարգացնելու և այնուհետև նրանով դուրս գալու վրա։

Այնուամենայնիվ, վերջին եզրակացությունն այն է, որ մարդկային ստեղծագործությունը դեռևս հիմնականում խորհրդավոր է, և չի հաջողվել մեծ հաջողություն ունենալ մեքենայության մեջ։

Պատմություն

Կարելի է ասել, որ թեորեմների ավտոմատ ապացուցումը արհեստական բանականության ամենահին ճյուղերից մեկն է։ Թեորեմների ավտոմատ ապացույցների բնագավառում կատարված հետազոտությունների շնորհիվ ձևակերպվել են որոնման ալգորիթմները(Օրինակ Binary Search Tree) և ձևավորվել են պաշտոնական լեզուներ, ինչպիսին է օրինակ՝ տրամաբանական ծրագրավորման լեզուն PROLOG-ը։

Ավտոմատ թեորեմի ապացուցման առաջին փորձը եղել է Ալեն Նյուելի և Հերբերտ Սայմոնի տրամաբանության տեսության մեքենան` 1956 թվականին։ Ծրագիր, որը փորձում էր ապացույցներ գտնել հիմնական տրամաբանության մեջ` կիրառելով հնարավոր աքսիոմների շղթաները։ Այն ժամանակ դեռ տեխնոլոգիաները զարգացած չէին, մեքենան չէր կարոողանում կատարել բոլոր որոնումները արագ, այն շատ դանդաղ էր աշխատում։ Երբ արհեստական բանականությունը զարգացավ ժամանակի խնդիրը՝ արագագործությունը, ինչ որ չափով կարգավորվեց և մինչ օրս այդ գործընթացները շարունակվում են։

Այժմ համակարգիչը հիմնականում իր արագագործության հաշվին քննարկում է բոլոր հնարավոր դեպքերը, ասենք օրինակ՝ թերի ինդուկցիայի մեթոդով և այլն, բայց վերջում երկար աշխատանքից հետո ընտրում է ամենակարճ լուծումը։ Օրինակ ծրագրավորված մեքենային տրվել է հետևյալ խնդիրը՝

Գտնել այնպիսի 100 անընդմեջ թվերի հաջորդականություն, որոնցից ոչ մեկը պարզ թիվ չէ։

Այս դեպքում մարդիկ ավելի հեշտ են գտել լուծումը քան համակարգիչը։

Եթե ուզում ենք ստեղծել մի մեքենա, որը մտածի մարդու պես, ապա այն պետք է որոշ խնդիրներ լուծի մարդու պես, առանց մշտապես տեղադրման կամ որոնողական մեթոդների օգնությամբ՝ այսինքն երբեմն սրամիտ գտնվի։

Այնուամենայնիվ որոշ լուրջ տեղերում համակարգը տվել է իր արդյունքը։ Նկարում պատկերված խնդիրը օգտագործվել է 2016 թվականին կատարված Turing Test-ի Ժամանակ, որում հարցվածների 60%-ը սխալվել է ընտրելով համակարգչի տված լուծումը՝ դա նշանակում է, որ հարցվածների գերակշռող մասի կարծիքով համակարգչի տված լուծումը ավելի նման է եղել մարդու բանականությանը մոտ լուծմանը։

Սա վերջերս կատարված Mini Turing Test է

Գրականություն

• Machine learning and automated theorem proving
• Logic and Proof Computer Science Tripos Part IB Michaelmas Term
• Automated theorem proving: theory and practice
• Logic for Computer Science: Foundations of Automatic Theorem Proving, Second Edition Jean Gallier