Keret probléma - Frame problem

A mesterséges intelligencia esetében a keretprobléma egy olyan problémát ír le, amely az elsőrendű logika (FOL) használatával valósítja meg a tényeket egy robotról a világon. A robot állapotának hagyományos FOL -val való ábrázolásához sok axióma használatára van szükség, amelyek egyszerűen azt sugallják, hogy a környezetben lévő dolgok nem változnak önkényesen. Például Hayes leír egy " blokkvilágot ", amely szabályozza a blokkok egymásra rakását. A FOL rendszerben további axiómákra van szükség a környezetre vonatkozó következtetések levonásához (például, hogy egy blokk nem változtathatja meg a pozícióját, hacsak fizikailag nem mozgatják). A keretprobléma az a probléma, hogy megfelelő axiómagyűjteményeket találunk a robotkörnyezet életképes leírásához.

John McCarthy és Patrick J. Hayes ezt a problémát 1969 -ben, Néhány filozófiai probléma a mesterséges intelligencia szempontjából című cikkében határozta meg . Ebben a cikkben és sok későbbi cikkben a formális matematikai probléma kiindulópont volt a mesterséges intelligencia tudásábrázolásának nehézségeivel kapcsolatos általánosabb vitákhoz. Olyan kérdések, mint például a racionális alapértelmezett feltevések megadása, és az, hogy az emberek mit tartanak józan észnek egy virtuális környezetben. Később a kifejezés szélesebb értelmet nyert a filozófiában , ahol úgy fogalmazták meg, hogy korlátozzák azokat a hiedelmeket, amelyeket a tettekre válaszul frissíteni kell. Logikai kontextusban a műveleteket jellemzően az határozza meg, hogy mit változtatnak, azzal az implicit feltételezéssel, hogy minden más (a keret) változatlan marad.

Leírás

A keretprobléma még nagyon egyszerű tartományokban is előfordul. A forgatókönyvet ajtóval, amely nyitható vagy csukható, valamint fényt kapcsolhat be vagy ki, statikusan két javaslat és . Ha ezek a feltételek megváltozhatnak, akkor két predikátum jobban reprezentálja őket, és ez az idő függvénye; az ilyen predikátumokat fluentnek nevezik . Az a tartomány, amelyben az ajtó zárva van, és a fény kikapcsol a 0. időpontban, és az ajtó kinyílik az 1. időpontban, közvetlenül ábrázolható a logikában a következő képletekkel:

Az első két képlet a kezdeti helyzetet reprezentálja; a harmadik képlet az ajtó nyitási művelet végrehajtásának hatását jelzi az 1. időpontban. Ha egy ilyen műveletnek előfeltételei lennének, például az ajtó kinyitása, akkor a következő lenne . A gyakorlatban lenne egy predikátusa annak meghatározására, hogy egy művelet mikor kerül végrehajtásra, és egy szabály a műveletek hatásainak megadására. A cikket a helyzet fogkő ad további részletekért.

Bár a fenti három képlet az ismert logika közvetlen kifejezése, nem elegendő a következmények helyes levonásához. Bár a következő feltételek (amelyek a várt helyzetet képviselik) összhangban vannak a fenti három képlettel, nem csak ezek.

   

Valójában egy másik feltételrendszer, amely megfelel a fenti három képletnek:

   

A keretprobléma az, hogy csak annak megadása, hogy mely feltételeket változtatják meg a műveletek, nem vonja maga után azt, hogy az összes többi feltétel nem változik. Ez a probléma megoldható az úgynevezett „keret-axiómák” hozzáadásával, amelyek kifejezetten meghatározzák, hogy a műveletek végrehajtása közben nem változnak minden olyan feltétel, amelyet a műveletek nem érintenek. Például, mivel a 0 időpontban végrehajtott művelet az ajtó kinyitása, egy keret axióma azt állítja, hogy a fény állapota nem változik a 0 -tól az 1 -ig:

A keretprobléma az, hogy minden keret- és feltételpárhoz szükség van egy ilyen keret axiómára, hogy a művelet ne befolyásolja az állapotot. Más szóval a probléma az, hogy egy dinamikus tartományt formalizálunk anélkül, hogy kifejezetten megadnánk a keret axiómáit.

A McCarthy által e probléma megoldására javasolt megoldás feltételezi, hogy minimális mennyiségű állapotváltozás történt; ezt a megoldást a körülírás keretén keresztül formalizálják . A Yale -felvételi probléma azonban azt mutatja, hogy ez a megoldás nem mindig helyes. Ezután alternatív megoldásokat javasoltak, beleértve a predikátum befejezését, a folyékony elzáródást, az utódállapot -axiómákat stb .; az alábbiakban ismertetjük. Az 1980 -as évek végére megoldódott a McCarthy és Hayes által meghatározott keretprobléma. Még ezt követően is továbbra is használták a „keretprobléma” kifejezést, részben ugyanarra a problémára utalva, de különböző körülmények között (pl. Párhuzamos műveletek), részben pedig a dinamikus ábrázolás és érvelés általános problémájára utalva. domainek.

Megoldások

A következő megoldások bemutatják, hogyan oldják meg a keretproblémát különböző formalizmusokban. Magukat a formalizmusokat nem mutatjuk be teljes egészében: a bemutatott egyszerűsített változatok elegendőek a teljes megoldás magyarázatához.

Folyékony elzáródási oldat

Ezt a megoldást Erik Sandewall javasolta , aki egy formális nyelvet is definiált a dinamikus tartományok meghatározásához; ezért egy ilyen tartomány először ezen a nyelven fejezhető ki, majd automatikusan logikába fordítható. Ebben a cikkben csak a logikai kifejezés jelenik meg, és csak az egyszerűsített nyelven, műveletnevek nélkül.

Ennek a megoldásnak az az oka, hogy nemcsak a feltételek időbeli értékét ábrázolja, hanem azt is, hogy befolyásolhatja -e őket az utoljára végrehajtott művelet. Ez utóbbit egy másik feltétel képviseli, az úgynevezett elzáródás. Azt mondják, hogy egy feltétel egy adott időpontban el van zárva , ha egy olyan műveletet hajtottak végre, amely a feltételt igaznak vagy hamisnak teszi hatásként. Az elzáródás tekinthető „változtatási engedélynek”: ha egy feltétel el van zárva, akkor mentesül a tehetetlenségi kényszer betartása alól.

Az ajtó és a fény egyszerűsített példájában az elzáródást két predikátummal és . Az indoklás szerint egy feltétel csak akkor módosíthatja az értéket, ha a megfelelő elzáródási predikátum igaz a következő időpontban. Az elzáródási predikátum viszont csak akkor igaz, ha a feltételt befolyásoló műveletet hajtják végre.

Általában minden olyan művelet, amely feltételt igaz vagy hamis, a megfelelő elzáródási predikátumot is igazá teszi. Ebben az esetben igaz, így a fenti negyedik képlet előzménye hamis lesz ; ezért a kényszer, amely nem áll fenn . Ezért megváltoztathatja az értéket, amit a harmadik képlet is érvényesít.

Annak érdekében, hogy ez a feltétel működjön, az elzáródási predikátumoknak csak akkor kell igaznak lenniük, ha egy cselekvés hatására valósulnak meg. Ez vagy körülírással, vagy predikátum kitöltéssel érhető el . Érdemes megjegyezni, hogy az elzáródás nem feltétlenül jelent változást: például az ajtó kinyitásának végrehajtása, amikor az már nyitva volt (a fenti formalizációban) igazsá teszi és igazsá teszi az állítást ; azonban nem változtatta meg az értékét, ahogy az már igaz volt.

Predikált befejezési megoldás

Ez a kódolás hasonló a folyékony elzárási megoldáshoz, de a további predikátumok a változást jelölik, nem a változtatás engedélyét. Például jelenti, hogy az állítmány változik időről hogy . Ennek eredményeképpen egy predikátum akkor és csak akkor változik, ha a megfelelő változó predikátum igaz. Egy művelet akkor és csak akkor eredményez változást, ha valóra vált egy korábban hamis feltételt, vagy fordítva.

A harmadik képlet egy másik módja annak, hogy az ajtó kinyitásával az ajtó kinyílik. Pontosan azt állítja, hogy az ajtó kinyitása megváltoztatja az ajtó állapotát, ha korábban bezárták. Az utolsó két feltétel azt állítja, hogy egy feltétel akkor és csak akkor módosítja az értéket, ha a megfelelő változási predikátum igaz . A megoldás befejezéséhez a változási predikátumok valós idejének a lehető legrövidebbnek kell lennie, és ezt úgy lehet megtenni, hogy predikátum -kitöltést alkalmazunk a műveletek hatásait meghatározó szabályokra.

Utódállapot -axióma megoldás

Egy feltétel értékét egy művelet végrehajtása után az határozza meg, hogy a feltétel akkor és csak akkor igaz, ha:

  1. a cselekvés igazolja a feltételt; vagy
  2. a feltétel korábban igaz volt, és a művelet nem teszi hamissá.

Az utódállapot -axióma e két tény logikai formalizálása. Például, ha a és két feltételnek jelölésére használjuk, hogy a kereset végrehajtott időpontban volt, hogy nyissa vagy zárja a kaput, illetve a futó például van kódolva a következőképpen.

Ez a megoldás a feltételek értéke, nem pedig a cselekvések hatása köré összpontosul. Más szóval, minden feltételhez van egy axióma, nem pedig minden cselekvésre vonatkozó képlet. A cselekvések előfeltételeit (amelyek ebben a példában nem szerepelnek) más képletek formalizálják. Az utódállapot -axiómákat a Ray Reiter által javasolt helyzetszámítás változatában használjuk .

Folyékony vízkőoldat

A folyékony számítás a helyzetszámítás egyik változata. Megoldja a keretproblémát azáltal , hogy predikátumok helyett elsőrendű logikai kifejezéseket használ az állapotok ábrázolására. A predikátumok terminusokká alakítását az elsőrendű logikában reification-nek nevezzük ; a folyékony számítás logikának tekinthető, amelyben a feltételek állapotát reprezentáló predikátumok megerősülnek.

A különbség a predikátum és a kifejezés között az elsőrendű logikában az, hogy a kifejezés egy objektum (esetleg más objektumokból álló összetett objektum) ábrázolása, míg a predikátum olyan feltételt jelent, amely igaz vagy hamis lehet, ha egy adott feltételrendszer.

A folyékony számításban minden lehetséges állapotot más kifejezések összetételével kapott kifejezés reprezentál, amelyek mindegyike az állapotra vonatkozó feltételeket jelenti. Például azt az állapotot, amelyben az ajtó nyitva van, és a fény világít, a kifejezés jelöli . Fontos megjegyezni, hogy egy kifejezés önmagában nem igaz vagy hamis, mivel tárgy és nem feltétel. Más szóval, a kifejezés egy lehetséges állapotot jelent, és önmagában nem jelenti azt, hogy ez a jelenlegi állapot. Külön feltétel adható meg annak meghatározására, hogy ez valójában egy adott időpont állapota, pl. Azt jelenti, hogy ez az állapot az adott időben .

A folyékony számításban megadott keretprobléma megoldása az, hogy meghatározzuk a műveletek hatásait azáltal, hogy megadjuk, hogyan változik az állapotot reprezentáló kifejezés a művelet végrehajtásakor. Például az ajtó nyitásának műveletét a 0 időpontban a következő képlet képviseli:

Az ajtó bezárásának művelete, amely egy feltételt hamissá tesz az igaz helyett, kissé másképpen ábrázolható:

Ez a képlet működik, feltéve, hogy megfelelő axiómákat adunk meg, és például, ha ugyanazt a feltételt kétszer tartalmazó kifejezés nem érvényes állapot (például mindig hamis minden és esetén ).

Eseményszámítási megoldás

Az eseményszámítás olyan kifejezéseket használ a folyékonyak képviseletére, mint a folyékony számítás, de olyan axiómákkal is rendelkezik, amelyek korlátozzák a folyékonyak értékét, mint például az utódállapot -axiómák. Az eseményszámításnál a tehetetlenséget olyan képletek erőltetik, amelyek kijelentik, hogy a fluent igaz, ha igaz volt egy adott előző időpontban, és közben nem hajtottak végre műveletet hamisra. A predikátum befejezésére akkor is szükség van az eseményszámítás során, hogy meggyőződjünk arról, hogy a fluent csak akkor válik valóra, ha az azt igazoló műveletet végrehajtották, de ahhoz is, hogy a műveletet csak akkor hajtották végre, ha ezt kifejezetten kimondják.

Alapértelmezett logikai megoldás

A keret probléma lehet elképzelni, mint a probléma hivatalossá az elvet, hogy alapértelmezés szerint „minden feltételezhető, hogy ugyanabban az állapotban marad, ahol van” ( Leibniz , „An Introduction to a titkos Encyclopædia” c . 1679). Ez az alapértelmezett, néha a józan törvénye tehetetlensége , fejezte ki Raymond Reiter in alapértelmezett logika :

(ha a helyzetben igaz , és feltételezhető, hogy a művelet végrehajtása után is igaz marad , akkor arra következtethetünk, hogy igaz marad).

Steve Hanks és Drew McDermott a Yale -felvételi példájuk alapján azzal érveltek, hogy ez a megoldás a keretproblémára nem kielégítő. Hudson Turner azonban megmutatta, hogy megfelelő kiegészítő posztulátumok jelenlétében megfelelően működik.

Válaszkészlet programozási megoldás

Az alapértelmezett logikai megoldás párja a válaszhalmaz programozás nyelvén egy erős tagadással rendelkező szabály :

(ha igaz az adott időben , és feltételezhető, hogy az adott időben igaz marad , akkor arra a következtetésre juthatunk, hogy igaz marad).

Elválasztási logikai megoldás

A szétválasztási logika formalizmus a számítógépes programokról való érveléshez, az űrlap elő/utáni specifikációinak felhasználásával . A szétválasztási logika a Hoare logika kiterjesztése, amely a számítógép memóriájában és más dinamikus erőforrásokban előforduló változékony adatstruktúrákról való gondolkodásra irányul, és rendelkezik egy speciális összekötő *-vel, amelyet "és külön" ejtünk, hogy támogassa a független érvelést a szétválasztott memóriarégiókról.

A szétválasztási logika a pre/post specifikációk szűk értelmezését alkalmazza , amelyek szerint a kód csak az előfeltétel által garantáltan létező memóriahelyeket érheti el. Ez a logika legfontosabb következtetési szabályának, a keretszabálynak a megalapozottságához vezet

A keretszabály lehetővé teszi, hogy tetszőleges, a lábnyomon kívüli memória leírásait (memóriahozzáférés) adjuk hozzá a specifikációhoz: ez lehetővé teszi, hogy a kezdeti specifikáció csak a lábnyomra koncentráljon. Például a következtetés

rögzíti azt a kódot, amely x listát rendez, nem szünteti meg az y külön listát , és ezt anélkül teszi , hogy egyáltalán megemlítené az y -t a sor feletti kezdeti specifikációban.

A keretszabály automatizálása jelentősen megnövelte a kód automatizált érvelési technikáinak skálázhatóságát, amelyeket végül iparilag telepítettek a 10 millió millió soros kódbázisokba.

Úgy tűnik, hogy van némi hasonlóság a keretprobléma elválasztási logikai megoldása és a fent említett folyékony számítás között.

Műveletleíró nyelvek

A cselekvésleíró nyelvek inkább elkerülik a keretproblémát, mintsem megoldják. A cselekvésleíró nyelv egy formális nyelv, amelynek szintaxisa specifikus a helyzetek és műveletek leírására. Például azt, hogy a művelet kinyitja az ajtót, ha nincs bezárva, a következőképpen fejezi ki:

okozza, ha

A cselekvésleíró nyelv szemantikája attól függ, hogy mit tud kifejezni a nyelv (párhuzamos műveletek, késleltetett hatások stb.), És általában átmeneti rendszereken alapul .

Mivel a tartományokat ezeken a nyelveken fejezik ki, nem pedig közvetlenül a logikában, a keretprobléma csak akkor merül fel, amikor egy műveleti leírási logikában megadott specifikációt logikába kell fordítani. Általában azonban ezekből a nyelvekből adnak fordítást, hogy válaszoljanak a halmazprogramozásra, és ne az elsőrendű logikára.

Lásd még

Megjegyzések

Hivatkozások

Külső linkek