Problema de quadro

Na inteligência artificial, o problema do quadro descreve um problema com o uso da lógica de primeira ordem (FOL) para expressar fatos sobre um robô no mundo. Representar o estado de um robô com FOL tradicional requer o uso de muitos axiomas que simplesmente implicam que as coisas no ambiente não mudam arbitrariamente. Por exemplo, Hayes descreve um "mundo de blocos" com regras sobre como empilhar blocos juntos. Em um sistema FOL, axiomas adicionais são necessários para fazer inferências sobre o ambiente (por exemplo, que um bloco não pode mudar de posição a menos que seja movido fisicamente). O problema do quadro é o problema de encontrar coleções adequadas de axiomas para uma descrição viável de um ambiente robótico.

John McCarthy e Patrick J. Hayes definiram esse problema em seu artigo de 1969, Alguns problemas filosóficos do ponto de vista da inteligência artificial. Neste artigo, e em muitos que vieram depois, o problema matemático formal foi um ponto de partida para discussões mais gerais sobre a dificuldade de representação do conhecimento para inteligência artificial. Questões como fornecer suposições padrão racionais e o que os humanos consideram senso comum em um ambiente virtual. Mais tarde, o termo adquiriu um significado mais amplo na filosofia, onde é formulado como o problema de limitar as crenças que devem ser atualizadas em resposta às ações. No contexto lógico, as ações são normalmente especificadas pelo que mudam, com a suposição implícita de que todo o resto (o quadro) permanece inalterado.

Descrição

O problema do quadro ocorre mesmo em domínios muito simples. Um cenário com uma porta, que pode ser aberta ou fechada, e uma luz, que pode estar ligada ou desligada, é representado estaticamente por duas proposições ${displaystyle mathrm {open} }$ e $- Não.$. Se essas condições podem mudar, elas são melhor representadas por dois predicados ${displaystyle mathrm {open} (t)}$ e $(t)}$ que dependem do tempo; tais predicados são chamados fluentes. Um domínio em que a porta é fechada e a luz fora no tempo 0, e a porta aberta no tempo 1, pode ser diretamente representado na lógica pelas seguintes fórmulas:

${displaystyle neg mathrm {open} (0)$

$(0)}$

${displaystyle mathrm {open} (1)$

As duas primeiras fórmulas representam a situação inicial; a terceira fórmula representa o efeito da execução da ação de abertura da porta no momento 1. Se tal ação tivesse pré-condições, como a porta sendo desbloqueada, teria sido representada por ${displaystyle neg mathrm {locked} (0) (1)$. Na prática, um teria um predicado ${displaystyle mathrm {executeopen} (t)}$ para especificar quando uma ação é executada e uma regra ${displaystyle forall t.mathrm {executeopen} (t)implies mathrm {open} (t+1)}$ para especificar os efeitos das ações. O artigo sobre o cálculo da situação dá mais detalhes.

Embora as três fórmulas acima sejam uma expressão direta em lógica do que é conhecido, elas não são suficientes para extrair corretamente as consequências. Embora as seguintes condições (representando a situação esperada) sejam consistentes com as três fórmulas acima, elas não são as únicas.

${displaystyle neg mathrm {open} (0)$	${displaystyle mathrm {open} (1)$
$(0)}$	${displaystyle neg mathrm {on} (1)}$

De fato, outro conjunto de condições consistente com as três fórmulas acima é:

${displaystyle neg mathrm {open} (0)$	${displaystyle mathrm {open} (1)$
$(0)}$	${displaystyle mathrm {on} (1)}$

O problema do quadro é que especificar apenas quais condições são alteradas pelas ações não implica que todas as outras condições não sejam alteradas. Esse problema pode ser resolvido adicionando os chamados “axiomas de quadro”, que especificam explicitamente que todas as condições não afetadas por ações não são alteradas durante a execução dessa ação. Por exemplo, como a ação executada no tempo 0 é a de abrir a porta, um axioma de frame afirmaria que o estado da luz não muda do tempo 0 para o tempo 1:

$(0)iff mathrm {on} (1)}$

O problema do quadro é que um tal axioma do quadro é necessário para cada par de ação e condição de modo que a ação não afete a condição. Em outras palavras, o problema é formalizar um domínio dinâmico sem especificar explicitamente os axiomas do quadro.

A solução proposta por McCarthy para resolver este problema envolve assumir que ocorreu uma quantidade mínima de mudanças de condição; esta solução é formalizada usando o quadro de circunscrição. O problema do tiro em Yale, no entanto, mostra que essa solução nem sempre é correta. Soluções alternativas foram então propostas, envolvendo completação de predicados, oclusão fluente, axiomas de estado sucessor, etc.; eles são explicados abaixo. No final da década de 1980, o problema do quadro definido por McCarthy e Hayes foi resolvido. Mesmo depois disso, entretanto, o termo “frame problem” ainda era usado, em parte para se referir ao mesmo problema, mas sob configurações diferentes (por exemplo, ações simultâneas), e em parte para se referir ao problema geral de representar e raciocinar com dinâmicas. domínios.

Soluções

As soluções a seguir descrevem como o problema do frame é resolvido em vários formalismos. Os formalismos em si não são apresentados na íntegra: o que se apresenta são versões simplificadas que são suficientes para explicar a solução completa.

Solução de oclusão fluente

Esta solução foi proposta por Erik Sandewall, que também definiu uma linguagem formal para a especificação de domínios dinâmicos; portanto, tal domínio pode ser primeiro expresso nessa linguagem e depois traduzido automaticamente para a lógica. Neste artigo, apenas a expressão em lógica é mostrada, e apenas na linguagem simplificada sem nomes de ações.

A lógica desta solução é representar não apenas o valor das condições ao longo do tempo, mas também se elas podem ser afetadas pela última ação executada. Esta última é representada por outra condição, denominada oclusão. Diz-se que uma condição está ocluída em um determinado ponto no tempo se uma ação acabou de ser executada e torna a condição verdadeira ou falsa como um efeito. A oclusão pode ser vista como “permissão para mudar”: se uma condição é ocluída, ela é dispensada de obedecer à restrição de inércia.

No exemplo simplificado da porta e da luz, a oclusão pode ser formalizada por dois predicados ${displaystyle mathrm {occludeopen} (t)}$ e $(t)}$. A racionalidade é que uma condição só pode mudar o valor se o predicado de oclusão correspondente for verdadeiro no ponto seguinte. Por sua vez, o predicado de oclusão é verdadeiro apenas quando uma ação que afeta a condição é executada.

${displaystyle neg mathrm {open} (0)$

$(0)}$

${displaystyle mathrm {open} (1)wedge mathrm {occludeopen}} (1)$

${displaystyle forall t.neg mathrm {occludeopen} (t)implies (mathrm {open} (t-1)iff mathrm {open} (t)})}$

${displaystyle forall t.neg mathrm {occludeon} (t)implies (mathrm {on} (t-1)iff mathrm {on} (t)}$

Em geral, cada ação fazendo uma condição verdadeira ou falsa também torna o oclusão correspondente predicado verdadeiro. Neste caso, ${displaystyle mathrm {occludeopen} (1)$ é verdade, fazendo o antecedente da quarta fórmula acima falsa para $Não.$; portanto, o constrangimento ${displaystyle mathrm {open} (t-1)iff mathrm {open} (t)}$ não segura para $Não.$. Portanto, ${displaystyle mathrm {open} }$ pode mudar o valor, que também é o que é aplicado pela terceira fórmula.

Para que esta condição funcione, os predicados de oclusão têm de ser verdadeiros apenas quando se tornam verdadeiros como um efeito de uma ação. Isso pode ser alcançado por circunscrição ou por conclusão predicada. Vale a pena notar que a oclusão não implica necessariamente uma mudança: por exemplo, executar a ação de abrir a porta quando já estava aberta (na formalização acima) faz o predicado ${displaystyle mathrm {occludeopen} }$ verdadeiro e faz ${displaystyle mathrm {open} }$ verdadeiro; no entanto, ${displaystyle mathrm {open} }$ não mudou o valor, como já era verdade.

Solução de conclusão predicada

Esta codificação é semelhante à solução de oclusão fluente, mas os predicados adicionais denotam mudança, não permissão para mudar. Por exemplo, $(t)}$ representa o fato de que o predicado ${displaystyle mathrm {open} }$ mudará do tempo $Não.$ para $Não.$. Como resultado, um predicado muda se e somente se o predicado de mudança correspondente é verdadeiro. Uma ação resulta em uma mudança se e somente se torna realidade uma condição que era anteriormente falsa ou vice-versa.

${displaystyle neg mathrm {open} (0)$

$(0)}$

${displaystyle neg mathrm {open} (0)implies mathrm {changeopen} (0)$

${displaystyle forall t.mathrm {changeopen} (t)iff (neg mathrm {open} (t)iff mathrm {open} (t+1)}$

${displaystyle forall t.mathrm {changeon} (t)iff (neg mathrm {on} (t)iff mathrm {on} (t+1)}$

A terceira fórmula é uma maneira diferente de dizer que abrir a porta faz com que a porta seja aberta. Precisamente, ele afirma que abrir a porta muda o estado da porta se ela tivesse sido previamente fechada. As duas últimas condições afirmam que uma condição muda o valor no momento $Não.$ se e somente se a mudança correspondente predicado é verdadeira no tempo $Não.$. Para completar a solução, os pontos de tempo em que os predicados de mudança são verdadeiros têm de ser tão poucos quanto possível, e isso pode ser feito aplicando a conclusão do predicado às regras especificando os efeitos das ações.

Solução de axiomas de estado sucessor

O valor de uma condição após a execução de uma ação pode ser determinado por o fato de que a condição é verdadeira se e somente se:

1. a ação torna a condição verdadeira; ou
2. a condição era anteriormente verdadeira e a ação não a torna falsa.

Um axioma do Estado sucessor é uma formalização na lógica desses dois fatos. Para exemplo, se ${displaystyle mathrm {opendoor} (t)}$ e $(t)}$ são dois condições usadas para denotar que a ação executada no momento $Não.$ foi para abrir ou fechar a porta, respectivamente, o exemplo em execução é codificado como segue.

${displaystyle neg mathrm {open} (0)$

$(0)}$

${displaystyle mathrm {opendoor} (0)$

${displaystyle forall t.mathrm {open} (t+1)iff mathrm {opendoor} (t)vee (mathrm {open} (t)wedge neg mathrm {closedoor} (t)})}$

Esta solução é centrada no valor das condições, em vez do efeitos das ações. Em outras palavras, existe um axioma para cada condição, em vez de uma fórmula para cada ação. Pré-condições para ações (que não são presentes neste exemplo) são formalizados por outras fórmulas. O estado sucessor axiomas são usados na variante do cálculo de situação proposto por Ray Reiter.

Solução de cálculo fluente

O cálculo fluente é uma variante do cálculo de situação. Ele resolve o problema do quadro usando lógica de primeira ordem termos, em vez de predicados, para representar os estados. Convertendo predicados em termos na lógica de primeira ordem é chamado de reificação; o cálculo fluente pode ser visto como uma lógica na qual os predicados que representam estado de condições são reificados.

A diferença entre um predicado e um termo na lógica de primeira ordem é que um termo é uma representação de um objeto (possivelmente um objeto complexo composto de outros objetos), enquanto um predicado representa uma condição que pode ser verdadeira ou falsa quando avaliados em um determinado conjunto de termos.

No cálculo fluente, cada estado possível é representado por um termo obtido por composição de outros termos, cada um representando as condições que são verdadeiras no estado. Por exemplo, o estado em que a porta está aberta e a luz está ligada é representado pelo termo ${displaystyle mathrm {open} circ mathrm {on} } }$. É importante notar que um termo não é verdadeiro ou falso por si mesmo, pois é um objeto e não uma condição. Em outras palavras, o termo ${displaystyle mathrm {open} circ mathrm {on} } }$ representar um estado possível, e não por si só significa que este é o estado atual. Uma condição separada pode ser declarada para especificar que este é realmente o estado em um determinado momento, por exemplo, ${displaystyle mathrm {state} (mathrm {open} circ mathrm {on}10)}$ significa que este é o estado no momento $Não.$.

A solução para o problema de frame fornecida no cálculo fluente é especificar os efeitos das ações declarando como um termo que representa o estado muda quando a ação é executada. Por exemplo, a ação de abrir a porta no tempo 0 é representada pela fórmula:

${displaystyle mathrm {state} (scirc mathrm {open}1)iff mathrm {state} (s,0)}$

A ação de fechar a porta, que torna uma condição falsa em vez de verdadeira, é representada de uma forma ligeiramente diferente:

${displaystyle mathrm {state} (s,1)iff mathrm {state} (scirc mathrm {open}0)}$

Esta fórmula funciona desde que os axiomas adequados são dados sobre $- Sim.$ e $- Sim.$, por exemplo, um termo contendo a mesma condição duas vezes não é um estado válido (por exemplo, ${displaystyle mathrm {state} (mathrm {open} circ scirc mathrm {open}t)}$ é sempre falso para cada $Não.$ e $Não.$).

Solução de cálculo de eventos

O cálculo de eventos usa termos para representar os fluentes, como o cálculo dos fluentes, mas também possui axiomas que restringem o valor dos fluentes, como os axiomas do estado sucessor. No cálculo de eventos, a inércia é imposta por fórmulas que afirmam que um fluente é verdadeiro se tiver sido verdadeiro em um determinado ponto de tempo anterior e nenhuma ação que o altere para falso tenha sido executada nesse meio tempo. A conclusão do predicado ainda é necessária no cálculo de eventos para obter que um fluente se torna verdadeiro somente se uma ação tornando-o verdadeiro foi executada, mas também para obter que uma ação foi executada somente se isso for explicitamente declarado.

Solução lógica padrão

O problema do quadro pode ser pensado como o problema de formalizar o princípio de que, por padrão, "presume-se que tudo permaneça no estado em que está" (Leibniz, "An Introduction to a Secret Encyclopædia", c. 1679). Esse padrão, às vezes chamado de lei de inércia do senso comum, foi expresso por Raymond Reiter na lógica padrão:

${displaystyle {frac {R(x,s);: R(x,mathrm {do} (a,s))}{R(x,mathrm {do} (a,s)}}}$

(se) ${displaystyle R(x)}$ é verdade em situação $Não.$, e pode ser assumido que ${displaystyle R(x)}$ permanece verdadeiro após a ação de execução $Não.$, então podemos concluir que ${displaystyle R(x)}$ permanece verdadeiro).

Steve Hanks e Drew McDermott argumentaram, com base em seu exemplo de tiro em Yale, que esta solução para o problema do quadro é insatisfatória. Hudson Turner mostrou, no entanto, que funciona corretamente na presença de postulados adicionais apropriados.

Solução de programação de conjuntos de respostas

A contrapartida da solução lógica padrão na linguagem de programação do conjunto de respostas é uma regra com negação forte:

${displaystyle r(X,T+1)leftarrow r(X,T),hbox{not }}sim r(X,T+1)}$

(se) $(X)}$ é verdade no tempo $Não. T.$, e pode ser assumido que $(X)}$ permanece verdadeiro no tempo $Não. T+1$, então podemos concluir que $(X)}$ permanece verdadeiro).

Solução de lógica de separação

Lógica de separação é um formalismo para raciocínio sobre programas de computador usando especificações pré/post do formulário $(precondição) } mathrm {code} {mathrm {postcondicionado} Sim.$. A lógica de separação é uma extensão da lógica Hoare orientada para raciocinar sobre estruturas de dados mutáveis na memória do computador e outros recursos dinâmicos, e tem uma conexão especial *, pronunciada "e separadamente", para apoiar o raciocínio independente sobre regiões de memória disjuntas.

A lógica de separação emprega uma interpretação rígida das especificações pré/pós, que dizem que o código pode apenas acessar locais de memória garantidos pela pré-condição. Isso leva à solidez da regra de inferência mais importante da lógica, a regra do frame

$(precondição) } mathrm {code} {mathrm {postcondicionado} }}{mathrm {precondicionado} ast mathrm {frame} } mathrm {code} {mathrm {postcondicionado} ast mathrm {frame} }}}}}}}}$

A regra do quadro permite que descrições de memória arbitrária fora do footprint (memória acessada) do código sejam adicionadas a uma especificação: isso permite que a especificação inicial se concentre apenas no footprint. Por exemplo, a inferência

${displaystyle {frac {{operatorname {list} (x)} mathrm {code} {operatorname {sortedlist} (x)}}{operatorname {list} (x)ast operatorname {sortedlist} (y)} mathrm {code} {operatorname {sortedlist} (x)ast operatorname {sortedlist}$

captura o código que classifica uma lista x não desclassifica uma lista separada y, e faz isso sem mencionar y em tudo a especificação inicial acima da linha.

A automação da regra de quadro levou a aumentos significativos na escalabilidade de técnicas de raciocínio automatizado para código, implantadas industrialmente em bases de código com dezenas de milhões de linhas.

Parece haver alguma semelhança entre a solução da lógica de separação para o problema do frame e aquela do cálculo fluente mencionado acima.

Linguagens de descrição de ação

As linguagens de descrição de ação eludem o problema do quadro em vez de resolvê-lo. Uma linguagem de descrição de ação é uma linguagem formal com uma sintaxe específica para descrever situações e ações. Por exemplo, que a ação $Não.$ faz a porta aberta se não estiver trancada é expressa por:

$Não.$ causas ${displaystyle mathrm {open} }$ se ${displaystyle neg mathrm {locked} }$

A semântica de uma linguagem de descrição de ação depende do que a linguagem pode expressar (ações concorrentes, efeitos retardados, etc.) e geralmente é baseada em sistemas de transição.

Como os domínios são expressos nessas linguagens em vez de diretamente na lógica, o problema do quadro surge apenas quando uma especificação fornecida em uma lógica de descrição de ação deve ser traduzida em lógica. Normalmente, no entanto, uma tradução é fornecida dessas linguagens para responder à programação de conjuntos, em vez da lógica de primeira ordem.