Թեորեմների ավտոմատացված ապացուցում

Ավտոմատացված թեորեմների ապացուցումը (որը նաև հայտնի է որպես ATP կամ ավտոմատացված դեդուկցիա) ավտոմատացված հիմնավորման և մաթեմատիկական տրամաբանության ենթածրագիր է, որը վերաբերում է համակարգչային ծրագրերով մաթեմատիկական տեսությունների հաստատմանը։ Մաթեմատիկական ապացույցի վերաբերյալ ավտոմատացված հիմնավորումը խթան հանդիսացավ համակարգչային գիտության զարգացման համար։

Առաջին իրականացումներ

Երկրորդ համաշխարհային պատերազմից կարճ ժամանակ անց առաջին համակարգիչները հասանելի դարձան։ 1954 թ.-ին Մարտին Դևիսը ծրագրում էր Պրովսբերգերի ալգորիթմը, JOHNNIAC վակուումային համակարգչի համար, Պրինսետոնի ինստիտուտի խորացված ուսումնասիրության ինստիտուտում։ Դևիսի խոսքերով, «Նրա մեծ հաղթանակը պետք է ապացուցի, որ երկու զույգ թվերի գումարը կրկին զույգ թիվ է»։ Ավելի հավակնոտ էր Logic Theory Machine-ը 1956 թ.-ին, Allia Newell-ի կողմից մշակված Principia Mathematica-ի պնդման տրամաբանության դեդուկցիոն համակարգը:Այս ծրագիրը՝, տրամաբանության տեսության մեքենան (Logic Theory Machine-ը), որը նաև աշխատում էր JOHNNIAC-ում, կառուցում էր ապացույցներ փոքրիկ պնդում աքսիոմներից և երեք դեդուկցիոն կանոններից. Modus ponens, (propositional) փոփոխականի փոխարինում և բանաձևերի փոխարինում դրանց սահմանմամբ։ Համակարգը օգտագործեց էվիրիական ուղեցույց և հաջողեց ապացուցել Principia-ի առաջին 52 տեսության 38-ը։

Տրամաբանության տեսության մեքենայի «էվիրիստական» մոտեցումը փորձել է մրցել մաթեմատիկոսների հետ, սակայն չի կարող երաշխավորել, որ ապացույց կարելի է գտնել կամայական հիմնավոր թեորեմի համար։ Ի տարբերություն մյուս, ավելի համակարգված ալգորիթմների, առնվազն տեսականորեն, ամբողջականությունն առաջին կարգի տրամաբանության համար է։ Նախնական մոտեցումները հիմնված էին Հերբրանդի և Սքոեմի արդյունքների վրա, որպեսզի առաջին կարգի բանաձևը դառնան առաջադեմ բանաձևերի ավելի մեծ հավաքածուներ, դարձնելով փոփոխականները Հերբրեն տիեզերքի տերմիններով։ Այնուհետև առաջարկվող բանաձևերը կարող են ստուգվել մի քանի մեթոդների կիրառմամբ անբավարարելիության համար։ Gilmore-ի ծրագիրն օգտագործեց ձևափոխման նորմալ ձևը, որում ձևակերպված է բանաձևի բավարարելիությունը։

Մաթեմատիկական արտահայտությունների ապացույցներ գտնող համակարգչային ծրագրերից է Ռոբինի վարկածի (Robbin’s conjecture) ապացույցը 1997 թվականին։

¬ (¬ (a ∨ b) ∨ ¬ (a ∨ ¬b)) = a^[1]

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

Պատմություն

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

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

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

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

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

Խնդրի լուծելիությունը

Կախված հիմքում ընկած տրամաբանությունից, բանաձևի վավերականության որոշման խնդիրը տատանվում է պարզագույնից մինչ անհնարին։ Առաջարկվող տրամաբանության հաճախակի դեպքի համար խնդիրը վճռական է, սակայն համահունչ NP-ը ամբողջական է, և հետևաբար, ընդհանուր ապացույցների առաջադրանքների համար ենթադրվում է միայն ժամանակային ժամանակի ալգորիթմներ։ Առաջին պատվին նախորդ հաշվարկի համար Գեելի ամբողջականության տեսությունը նշում է, որ թեորեմները (ապացուցելի պնդումները) հենց տրամաբանորեն վավեր են լավ ձևավորված բանաձևերը, ուստի վավեր բանաձևերը նույնականացնող թվացյալ են. Հաշվի առնելով անսահման ռեսուրսները, ցանկացած վավեր բանաձև, ի վերջո, կարող է ապացուցել։ Այնուամենայնիվ, անվավեր ձևակերպումները (որոնք չեն ենթարկվում տվյալ տեսության մեջ), չեն կարող միշտ ճանաչվել։

Ծանոթագրություններ

↑ Weisstein, Eric W. «Robbins Conjecture». mathworld.wolfram.com (անգլերեն). Վերցված է 2019 թ․ հոկտեմբերի 17-ին.
↑ Prolog Tutorial, Վերցված է 2019-10-17-ին
↑ «Note (c) for Implications for Mathematics and Its Foundations: A New Kind of Science | Online by Stephen Wolfram [Page 1157]». www.wolframscience.com (անգլերեն). Վերցված է 2019 թ․ հոկտեմբերի 17-ին.

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

Արտաքին հղումներ

[1] Weisstein, Eric W. «Robbins Conjecture». mathworld.wolfram.com (անգլերեն). Վերցված է 2019 թ․ հոկտեմբերի 17-ին.

[2] Prolog Tutorial, Վերցված է 2019-10-17-ին

[3] «Note (c) for Implications for Mathematics and Its Foundations: A New Kind of Science | Online by Stephen Wolfram [Page 1157]». www.wolframscience.com (անգլերեն). Վերցված է 2019 թ․ հոկտեմբերի 17-ին.

[1]

[2]

[3]