Жасанды интеллект және санаттық алгебрадағы «қаңқа» проблемасы

Кіріспе

Жасанды интеллект және категориялық алгебрадағы мәселе. Жасанды интеллектте, когнитивтік ғылымға әсер ете отырып, кадр мәселесі әлемдегі робот туралы фактілерді білдіру үшін бірінші реттік логиканы қолданумен байланысты мәселені сипаттайды. Роботтың күйін дәстүрлі бірінші реттік логикамен көрсету үшін көптеген аксиомаларды пайдалану қажет, олар қоршаған ортадағы нәрселердің кездейсоқ түрде өзгеретінін білдіреді. Мысалы, Хейз «блоктар әлемін» блоктарды біріктіру ережелерімен сипаттады. Бірінші реттік логикалық жүйеде, қоршаған орта туралы қорытындылар жасау үшін қосымша аксиомалар қажет (мысалы, блок физикалық түрде жылжытылмаса, орнын өзгерте алмайды). Кадр мәселесі – робот ортасын тиімді сипаттау үшін аксиомалардың жеткілікті жиынтығын табу мәселесі. Джон Маккарти және Патрик Хейс бұл мәселені 1969 жылғы «Жасанды интеллект тұрғысынан кейбір философиялық мәселелер» атты мақаласында анықтады. Осы және одан кейінгі көптеген мақалаларда, формалды математикалық мәселе жасанды интеллект үшін білімді көрсетудің қиындықтары туралы кеңірек талқылаудың бастапқы нүктесі болды. Рационалды дефолттық болжамдарды қалай ұсыну және адамдар виртуалды ортада ақылдылық деп санайтын мәселелер де қарастырылды. Философияда кадр мәселесі, іс-әрекеттерге жауап ретінде жаңартылуы тиіс сенімдерді шектеу мәселесімен байланысты, кеңірек түсіндірілді. Логикалық контексте, әрекеттер әдетте олар қандай өзгерістер жасайтынымен анықталады, сонымен бірге қалған барлық нәрсе (кадр) өзгермейді деп есептеледі.

Шешімдер

Келесі шешімдер әртүрлі формализмдерде кадрлық мәселенің қалай шешілетінін көрсетеді. Формализмдердің өзі толық түрде келтірілмейді: толық шешімді түсіндіру үшін жеткілікті ең қарапайым нұсқалары ғана ұсынылған.

Сұйық окклюзия ерітіндісі

Бұл шешімді Эрик Сандуолл ұсынды, ол сондай-ақ динамикалық домендерді сипаттау үшін формальді тілді анықтады; сондықтан, мұндай доменді алдымен осы тілде көрсетуге болады, содан кейін автоматты түрде логикаға аударуға болады. Бұл мақалада тек логикалық өрнегі көрсетілген, және тек аттары жоқ қарапайым тілде. Бұл шешімнің негізі – уақыт өте келе жағдайлардың мәнін ғана емес, сонымен қатар соңғы орындалған әрекет оларға әсер етуі мүмкін екенін көрсету болып табылады. Бұл соңғысы басқа бір жағдаймен бейнеленеді, ол – тұйықталу. Егер бір жағдайға әсер ететін әрекет орындалса, ол сол жағдайды шын немесе жалған етеді, онда ол жағдай белгілі бір уақыт мезгілінде тұйықталған болып есептеледі. Тұйықталуды «өзгертуге рұқсат» ретінде қарастыруға болады: егер жағдай тұйықталған болса, ол инерция заңынан босатылады. Есік пен шамның қарапайым мысалында тұйықталу екі предикат арқылы формальдануы мүмкін, және оның негізі мынада: жағдай тек қана сәйкес тұйықталу предикаты келесі уақыт мезгілінде дұрыс болса ғана мәнін өзгерте алады. Ал тұйықталу предикаты тек жағдайға әсер ететін әрекет орындалғанда ғана дұрыс болады. Жалпы, жағдайды шын немесе жалған ететін әрбір әрекет сонымен қатар сәйкес тұйықталу предикатын да шын етеді. Бұл жағдайда, true, жоғарыдағы төртінші формуланың алшақтығын үшін жалған етеді; сондықтан, үшін шектеу қолданылмайды; сондықтан, мәнін өзгерте алады, бұл үшінші формуламен де расталады. Бұл шарттың жұмыс істеуі үшін тұйықталу предикаттары тек әрекеттің нәтижесінде ғана шын болуы керек. Бұл циркумскрипция немесе предикатты толықтыру арқылы жүзеге асырылуы мүмкін. Бір қызығы, тұйықталу міндетті түрде өзгерісті білдірмейді: мысалы, есік бұрыннан ашық болғанда оны ашу әрекеті (жоғарыдағы формальдануда) предикатты шын етеді және предикатты шын етеді; алайда, мәні өзгермеді, өйткені ол бұрыннан шын болған.

This solution was proposed by Erik Sandewall, who also defined a formal language for the specification of dynamical domains; therefore, such a domain can be first expressed in this language and then automatically translated into logic. In this article, only the expression in logic is shown, and only in the simplified language with no action names. The rationale of this solution is to represent not only the value of conditions over time, but also whether they can be affected by the last executed action. The latter is represented by another condition, called occlusion. A condition is said to be occluded in a given time point if an action has been just executed that makes the condition true or false as an effect. Occlusion can be viewed as “permission to change”: if a condition is occluded, it is relieved from obeying the constraint of inertia. In the simplified example of the door and the light, occlusion can be formalized by two predicates and The rationale is that a condition can change value only if the corresponding occlusion predicate is true at the next time point. In turn, the occlusion predicate is true only when an action affecting the condition is executed. In general, every action making a condition true or false also makes the corresponding occlusion predicate true. In this case, is true, making the antecedent of the fourth formula above false for ; therefore, the constraint that does not hold for Therefore, can change value, which is also what is enforced by the third formula. In order for this condition to work, occlusion predicates have to be true only when they are made true as an effect of an action. This can be achieved either by circumscription or by predicate completion. It is worth noticing that occlusion does not necessarily imply a change: for example, executing the action of opening the door when it was already open (in the formalization above) makes the predicate true and makes true; however, has not changed value, as it was true already.

Толықтыруды болжау шешімі

Бұл кодтау ағып тұрған тұйықталу шешіміне ұқсас, бірақ қосымша предикаттар өзгерісті көрсетеді, өзгертуге рұқсат емес. Мысалы, предикат уақыттан уақытқа өзгеріп отырады. Нәтижесінде, предикат тек қана тиісті өзгерту предикаты дұрыс болғанда ғана өзгеріске ұшырайды. Әрекет өзгертуге алып келеді, егер ол бұрын жалған болған шартты шындыққа айналдырса немесе керісінше. Үшінші формула есікті ашудың есіктің ашылуына себеп болатынын айтудың тағы бір жолы. Нақтырақ айтқанда, есікті ашу, егер ол бұрын жабық болса, есіктің күйін өзгертеді. Соңғы екі шарт бойынша, жағдай уақытта мәнін өзгертеді, егер және тек қана тиісті өзгерту предикаты сол уақытта дұрыс болса. Шешімді толықтыру үшін, өзгерту предикаттарының дұрыс болатын уақыт нүктелерінің саны ең аз болуы керек, және бұл әрекеттердің әсерін анықтайтын ережелерге предикатты толықтыру қолдану арқылы жүзеге асырылуы мүмкін.

Әдетті логикалық шешім

Фрейм мәселесін "әр нәрсе өз күйінде қала береді" деген қағиданы формалдау мәселесі деп қарастыруға болады (Лейбниц, "Сыр энциклопедиясына кіріспе", 1679 ж.). Бұл әдепкілік, кейде инерцияның жалпыға ортақ заңы деп аталады, Реймонд Райтер әдеттегі логикада былай білдірді:

(Егер жағдайда шын болса және әрекет орындалғаннан кейін де шын болып қала береді деп есептеуге болады, онда ол шын болып қала береді деген қорытынды жасауға болады). Стив Хэнкс және Дрю Макдермот Йельдегі ату мысалының негізінде, фрейм мәселесінің бұл шешімі қанағаттандырмайды деп мәлімдеді. Дегенмен, Хадсон Тернер тиісті қосымша постулаттар болған жағдайда бұл әдістің дұрыс жұмыс істейтінін көрсетті.

Бөлудің логикалық шешімі

Бөлу логикасы – компьютерлік бағдарламаларды есептеудің формализмі, ол pre/post спецификацияларын қолданады. Бөлу логикасы – Хоар логикасының кеңейтілген түрі, компьютерлік жадтағы және басқа да динамикалық ресурстардағы өзгертілетін деректер құрылымдары туралы ойлауға бағытталған. Онда * деп аталатын арнайы байланыстырғыш бар, ол "және бөлек" деп оқылады, бұл жадтың бөлек аймақтары туралы тәуелсіз ойлауға мүмкіндік береді. Бөлу логикасы pre/post спецификацияларды қатаң түсіндіреді, яғни код тек алдын ала шарттармен кепілдендірілген жад орындарына ғана қол жеткізе алады. Бұл логиканың ең маңызды қорытындылау ережесінің – фрейм ережесінің дұрыстығына әкеледі. Фрейм ережесі кодтың қолжеткізілетін жадысынан (аяқ іздерінен) тыс жадтың кездейсоқ сипаттамаларын спецификацияға қосуға мүмкіндік береді, бұл бастапқы спецификацияның тек аяқ іздеріне назар аударуына мүмкіндік береді. Мысалы, мына қорытынды x тізімін сұрыптайтын код y жеке тізімін бұзбайды, және бұл y-ті бастапқы спецификацияда мүлдем атамай-ақ жасалады. Фрейм ережесін автоматтандыру кодты автоматтандырылған есептеу әдістерінің масштабталуын айтарлықтай арттырды, нәтижесінде он миллиондаған жолдардан тұратын код базаларында өнеркәсіптік қолданысқа енгізілді. Фреймдік мәселенің бөлу логикасымен және жоғарыда аталған ағылшын калькуляторымен шешілуінің арасында белгілі бір ұқсастықтар бар сияқты.