Ramme problem - Frame problem

I kunstig intelligens beskriver rammeproblemet et problem med bruk av første ordens logikk (FOL) for å uttrykke fakta om en robot i verden. Å representere tilstanden til en robot med tradisjonell FOL krever bruk av mange aksiomer som ganske enkelt antyder at ting i miljøet ikke endres vilkårlig. For eksempel beskriver Hayes en " blokkverden " med regler om å stable blokker sammen. I et FOL -system kreves ytterligere aksiomer for å gjøre slutninger om miljøet (for eksempel at en blokk ikke kan endre posisjon med mindre den er fysisk flyttet). Rammeproblemet er problemet med å finne tilstrekkelige samlinger av aksiomer for en levedyktig beskrivelse av et robotmiljø.

John McCarthy og Patrick J. Hayes definerte dette problemet i artikkelen fra 1969, Some Philosophical Problems from the Standpoint of Artificial Intelligence . I denne artikkelen, og mange som kom etter, var det formelle matematiske problemet et utgangspunkt for mer generelle diskusjoner om vanskeligheten med kunnskapsrepresentasjon for kunstig intelligens. Spørsmål som hvordan man gir rasjonelle standardantagelser og hva mennesker anser som sunn fornuft i et virtuelt miljø. Senere fikk begrepet en bredere mening i filosofien , der det er formulert som problemet med å begrense troen som må oppdateres som svar på handlinger. I den logiske konteksten spesifiseres handlinger vanligvis av det de endrer, med den implisitte antagelsen at alt annet (rammen) forblir uendret.

Beskrivelse

Rammeproblemet oppstår selv i veldig enkle domener. Et scenario med en dør, som kan være åpen eller lukket, og et lys, som kan være på eller av, er statisk representert av to forslag og . Hvis disse forholdene kan endres, blir de bedre representert av to predikater, og det er avhengig av tid; slike predikater kalles flytende . Et domene der døren er lukket og lyset slukket på tidspunkt 0, og døren åpnet på tid 1, kan representeres direkte i logikk av følgende formler:

De to første formlene representerer utgangssituasjonen; den tredje formelen representerer effekten av å utføre handlingen med å åpne døren på et tidspunkt 1. Hvis en slik handling hadde forutsetninger, for eksempel at døren låses opp, ville den ha blitt representert av . I praksis ville man ha et predikat for å spesifisere når en handling utføres og en regel for å spesifisere effekten av handlinger. Artikkelen om situasjonsberegningen gir flere detaljer.

Selv om de tre formlene ovenfor er et direkte uttrykk i logikken til det som er kjent, er det ikke nok å trekke konsekvenser på riktig måte. Selv om følgende betingelser (som representerer den forventede situasjonen) er i samsvar med de tre formlene ovenfor, er de ikke de eneste.

   

Et annet sett med betingelser som er i samsvar med de tre formlene ovenfor er faktisk:

   

Rammeproblemet er at det å spesifisere bare hvilke betingelser som er endret av handlingene ikke innebærer at alle andre forhold ikke blir endret. Dette problemet kan løses ved å legge til de såkalte "rammeaksiomene", som eksplisitt angir at alle forholdene som ikke påvirkes av handlinger ikke endres mens handlingen utføres. For eksempel, siden handlingen som utføres på tidspunkt 0 er den for å åpne døren, vil et rammeaksiom opplyse at lysets status ikke endres fra tid 0 til tid 1:

Rammeproblemet er at ett slikt rammeaksiom er nødvendig for hvert handlingspar og tilstand slik at handlingen ikke påvirker tilstanden. Med andre ord er problemet å formalisere et dynamisk domene uten å spesifisere rammeaksionene eksplisitt.

Løsningen foreslått av McCarthy for å løse dette problemet innebærer å anta at en minimal mengde tilstandsendringer har skjedd; denne løsningen er formalisert ved hjelp av rammen for omskrift . The Yale skyting problem , viser imidlertid at denne løsningen er ikke alltid riktig. Alternative løsninger ble deretter foreslått, som involverer predikat -ferdigstillelse, flytende okklusjon, aksiomer for etterfølgerstatus , etc.; de er forklart nedenfor. På slutten av 1980 -tallet ble rammeproblemet som definert av McCarthy og Hayes løst. Selv etter det ble imidlertid begrepet "rammeproblem" fortsatt brukt, delvis for å referere til det samme problemet, men under forskjellige innstillinger (f.eks. Samtidige handlinger), og delvis for å referere til det generelle problemet med å representere og resonnere med dynamisk domener.

Løsninger

Følgende løsninger viser hvordan rammeproblemet løses i forskjellige formalismer. Formalismene i seg selv presenteres ikke i sin helhet: det som presenteres er forenklede versjoner som er tilstrekkelige til å forklare den fulle løsningen.

Flytende okklusjonsløsning

Denne løsningen ble foreslått av Erik Sandewall , som også definerte et formelt språk for spesifikasjon av dynamiske domener; Derfor kan et slikt domene først uttrykkes på dette språket og deretter automatisk oversettes til logikk. I denne artikkelen vises bare uttrykket i logikk, og bare på det forenklede språket uten handlingsnavn.

Begrunnelsen for denne løsningen er å representere ikke bare verdien av forhold over tid, men også om de kan påvirkes av den siste utførte handlingen. Sistnevnte er representert av en annen tilstand, kalt okklusjon. En tilstand sies å være tilstoppet på et gitt tidspunkt hvis en handling nettopp har blitt utført som gjør tilstanden sann eller usann som en effekt. Okklusjon kan sees på som "tillatelse til å endre": hvis en tilstand er okkludert, blir den lettet fra å adlyde treghetsbegrensningen.

I det forenklede eksempelet på døren og lyset kan okklusjon formaliseres av to predikater og . Begrunnelsen er at en betingelse bare kan endre verdi hvis det tilhørende okklusjonspredikatet er sant ved neste tidspunkt. På sin side er okklusjonspredikatet bare sant når en handling som påvirker tilstanden utføres.

Generelt gjør hver handling som gjør en betingelse sann eller usann også det tilsvarende okklusjonspredikatet sant. I dette tilfellet er det sant, noe som gjør forløpet til den fjerde formelen ovenfor usant for ; derfor begrensningen som ikke holder for . Derfor kan du endre verdi, som også er det som håndheves av den tredje formelen.

For at denne tilstanden skal fungere, må okklusjonspredikater bare være sanne når de blir oppfylt som en effekt av en handling. Dette kan oppnås enten ved omskrift eller ved predikatavslutning. Det er verdt å legge merke til at okklusjon ikke nødvendigvis innebærer en endring: for eksempel gjør utførelsen av handlingen med å åpne døren når den allerede var åpen (i formaliseringen ovenfor) predikatet sant og sant; har imidlertid ikke endret verdi, slik det var sant allerede.

Predikat ferdigstillingsløsning

Denne kodingen ligner den flytende okklusjonsløsningen, men de ekstra predikatene angir endring, ikke tillatelse til å endre. For eksempel representerer det faktum at predikatet vil endres fra tid til . Som et resultat endres et predikat hvis og bare hvis det tilsvarende endringspredikatet er sant. En handling resulterer i en endring hvis og bare hvis den gjør en tilstand som tidligere var falsk eller omvendt.

Den tredje formelen er en annen måte å si at åpning av døren fører til at døren åpnes. Nettopp det står at åpning av døren endrer tilstanden til døren hvis den hadde vært lukket tidligere. De to siste betingelsene sier at en betingelse endrer verdi til enhver tid hvis og bare hvis det tilsvarende endringspredikatet er sant til enhver tid . For å fullføre løsningen må tidspunktene der endringspredikatene er sanne, være så få som mulig, og dette kan gjøres ved å bruke predikatfylling på reglene som angir virkningene av handlinger.

Etterfølgerstatens aksiomer løsning

Verdien av en betingelse etter utførelsen av en handling kan bestemmes av det faktum at betingelsen er sann hvis og bare hvis:

  1. handlingen gjør tilstanden sann; eller
  2. tilstanden var tidligere sann, og handlingen gjør den ikke falsk.

Et etterfølgerstataksiom er en formalisering i logikken til disse to faktaene. For eksempel, hvis og er to betingelser som brukes for å angi at handlingen som ble utført på et tidspunkt var henholdsvis å åpne eller lukke døren, er det kjørende eksempelet kodet som følger.

Denne løsningen er sentrert rundt verdien av forhold, snarere enn effekten av handlinger. Med andre ord er det et aksiom for hver tilstand, snarere enn en formel for hver handling. Forutsetninger for handlinger (som ikke er tilstede i dette eksemplet) formaliseres av andre formler. Etterfølgerstaten aksiomer brukes i varianten til situasjonsberegningen foreslått av Ray Reiter .

Flytende beregningsløsning

Den flytende beregningen er en variant av situasjonsberegningen. Det løser rammeproblemet ved å bruke første ordens logiske termer , i stedet for predikater, for å representere statene. Å konvertere predikater til termer i første ordens logikk kalles reifikasjon ; den flytende beregningen kan sees på som en logikk der predikater som representerer tilstanden blir reifisert.

Forskjellen mellom et predikat og et begrep i første ordens logikk er at et begrep er en representasjon av et objekt (muligens et komplekst objekt sammensatt av andre objekter), mens et predikat representerer en tilstand som kan være sann eller usann når den evalueres over en gitt sett med vilkår.

I den flytende beregningen er hver mulig tilstand representert ved et begrep oppnådd ved sammensetning av andre termer, hver representerer betingelsene som er sanne i tilstanden. For eksempel representerer tilstanden der døren er åpen og lyset er på, begrepet . Det er viktig å legge merke til at et begrep ikke er sant eller usant i seg selv, ettersom det er et objekt og ikke en betingelse. Med andre ord representerer begrepet en mulig tilstand, og betyr ikke i seg selv at dette er den nåværende tilstanden. En egen betingelse kan angis for å spesifisere at dette faktisk er staten på et gitt tidspunkt, f.eks. Betyr at dette er staten til enhver tid .

Løsningen på rammeproblemet gitt i flytende beregning er å spesifisere virkningene av handlinger ved å angi hvordan et begrep som representerer staten endres når handlingen utføres. For eksempel er handlingen med å åpne døren på tidspunkt 0 representert av formelen:

Handlingen med å lukke døren, noe som gjør en betingelse falsk i stedet for sann, er representert på en litt annen måte:

Denne formelen fungerer forutsatt at egnede aksiomer er gitt om, og for eksempel er et begrep som inneholder samme betingelse to ganger ikke en gyldig tilstand (for eksempel er det alltid usant for hver og ).

Hendelsesberegningsløsning

Den hendelsen kalkulus bruker ord for å representere fluents, som flytende kalkulus, men har også aksiomer begrensende verdien av fluents, som etterfølger statlige aksiomer. I hendelsesberegningen håndheves treghet med formler som sier at flytende er sant hvis det har vært sant på et gitt tidligere tidspunkt og ingen handling som endret det til falsk har blitt utført i mellomtiden. Predikat ferdigstillelse er fortsatt nødvendig i hendelsesberegningen for å oppnå at en flytende blir sant bare hvis en handling som gjør den sann er utført, men også for å oppnå at en handling bare hadde blitt utført hvis det er eksplisitt angitt.

Standard logisk løsning

Rammeproblemet kan betraktes som problemet med å formalisere prinsippet om at "alt som standard antas å forbli i den tilstanden det er i" ( Leibniz , "En introduksjon til et hemmelig encyklopædia", c . 1679). Denne standarden, noen ganger kalt commonsense law of inertia , ble uttrykt av Raymond Reiter i standardlogikk :

(hvis det er sant i situasjonen , og det kan antas at det forblir sant etter at handling er utført , kan vi konkludere med at det forblir sant).

Steve Hanks og Drew McDermott hevdet, på grunnlag av deres Yale -skyteeksempel , at denne løsningen på rammeproblemet er utilfredsstillende. Hudson Turner viste imidlertid at det fungerer riktig i nærvær av passende ytterligere postulater.

Svarssett programmeringsløsning

Motstykket til standardlogikkløsningen på språket i svarprogrammering er en regel med sterk negasjon :

(hvis det er sant til tider , og det kan antas at det forblir sant til tider , så kan vi konkludere med at det forblir sant).

Separasjonslogikkløsning

Separasjonslogikk er en formalisme for resonnement om dataprogrammer som bruker pre/post spesifikasjoner av skjemaet . Separasjonslogikk er en forlengelse av Hoare -logikk orientert mot resonnement om mutable datastrukturer i dataminne og andre dynamiske ressurser, og den har en spesiell forbindelse *, uttales "og separat", for å støtte uavhengig resonnement om usammenhengende minneområder.

Separasjonslogikk bruker en tett tolkning av spesifikasjoner før/etter, som sier at koden bare kan få tilgang til minnesteder som garantert eksisterer av forutsetningen. Dette fører til at den viktigste slutningsregelen for logikken, ramme -regelen, er forsvarlig

Rammeregelen tillater at beskrivelser av vilkårlig minne utenfor kodens fotavtrykk (tilgang til minne) legges til i en spesifikasjon: dette gjør at den første spesifikasjonen bare kan konsentrere seg om fotavtrykket. For eksempel slutningen

fanger den koden som sorterer en liste x , ikke sorterer en egen liste y, og den gjør dette uten å nevne y i det hele tatt i den første spesifikasjonen over linjen.

Automatisering av ramme -regelen har ført til betydelige økninger i skalerbarheten til automatiserte resonnementsteknikker for kode, og til slutt distribuert industrielt til kodebaser med 10s av millioner linjer.

Det ser ut til å være en viss likhet mellom separasjonslogikkløsningen til rammeproblemet og den flytende beregningen som er nevnt ovenfor.

Handlingsbeskrivelsesspråk

Handlingsbeskrivelsesspråk unngår rammeproblemet i stedet for å løse det. Et handlingsbeskrivelsesspråk er et formelt språk med en syntaks som er spesifikk for å beskrive situasjoner og handlinger. For eksempel at handlingen får døren til å åpne hvis den ikke er låst, uttrykkes av:

årsaker hvis

Semantikken til et handlingsbeskrivelsesspråk avhenger av hva språket kan uttrykke (samtidige handlinger, forsinkede effekter, etc.) og er vanligvis basert på overgangssystemer .

Siden domener uttrykkes på disse språkene i stedet for direkte i logikk, oppstår rammeproblemet bare når en spesifikasjon gitt i en handlingsbeskrivelseslogikk skal oversettes til logikk. Vanligvis gis imidlertid en oversettelse fra disse språkene for å svare på settprogrammering i stedet for første ordens logikk.

Se også

Merknader

Referanser

Eksterne linker