Problema de quadro - Frame problem

Em inteligência artificial , o problema de 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. 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 fisicamente movido). O problema do frame é encontrar coleções adequadas de axiomas para uma descrição viável de um ambiente de robô.

John McCarthy e Patrick J. Hayes definiram esse problema em seu artigo de 1969, Some Philosophical Problems from the Standpoint of Artificial Intelligence . 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 da representação do conhecimento para a inteligência artificial. Questões como fornecer suposições padrão racionais e o que os humanos consideram bom senso em um ambiente virtual. Posteriormente, o termo adquiriu um significado mais amplo na filosofia , onde é formulado como o problema de limitar as crenças que precisam ser atualizadas em resposta às ações. No contexto lógico, as ações são normalmente especificadas por aquilo 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 acesa ou apagada, é representado estaticamente por duas proposições e . Se essas condições podem mudar, elas são melhor representadas por dois predicados e que dependem do tempo; esses predicados são chamados de fluentes . Um domínio no qual a porta é fechada e a luz apagada no tempo 0, e a porta aberta no tempo 1, pode ser representado diretamente na lógica pelas seguintes fórmulas:

As duas primeiras fórmulas representam a situação inicial; a terceira fórmula representa o efeito de executar a ação de abrir a porta no tempo 1. Se tal ação tivesse pré-condições, como a porta sendo destrancada, ela seria representada por . Na prática, haveria um predicado para especificar quando uma ação é executada e uma regra 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 na lógica do que é conhecido, elas não bastam 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.

   

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

   

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. Este problema pode ser resolvido adicionando os chamados “axiomas de quadro”, que especificam explicitamente que todas as condições não afetadas pelas ações não são alteradas durante a execução dessa ação. Por exemplo, uma vez que a ação executada no tempo 0 é a de abrir a porta, um axioma de moldura afirmaria que o status da luz não muda do tempo 0 para o tempo 1:

O problema da moldura é que um desses axiomas é 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 referencial.

A solução proposta por McCarthy para resolver este problema envolve assumir que uma quantidade mínima de mudanças de condição ocorreu; esta solução é formalizada no quadro da circunscrição . O problema do tiro em Yale , entretanto, mostra que essa solução nem sempre é correta. Soluções alternativas foram então propostas, envolvendo completamento de predicado, oclusão fluente, axiomas de estado sucessor , etc .; eles são explicados abaixo. No final da década de 1980, o problema da estrutura, conforme definido por McCarthy e Hayes, foi resolvido. Mesmo depois disso, no entanto, o termo "problema de quadro" ainda foi usado, em parte para se referir ao mesmo problema, mas em configurações diferentes (por exemplo, ações simultâneas), e em parte para se referir ao problema geral de representação e raciocínio com dinâmica 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 por completo: o que é apresentado 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 expresso primeiro nesta linguagem e, em seguida, 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. Este último é representado por outra condição, chamada oclusão. Uma condição é considerada ocluída em um determinado momento se uma ação que acaba de ser executada 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 for obstruí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 e . O raciocínio é que uma condição pode alterar o valor apenas se o predicado de oclusão correspondente for verdadeiro no próximo momento. Por sua vez, o predicado de oclusão é verdadeiro apenas quando uma ação que afeta a condição é executada.

Em geral, toda ação que torna uma condição verdadeira ou falsa também torna verdadeiro o predicado de oclusão correspondente. Nesse caso, é verdadeiro, tornando o antecedente da quarta fórmula acima falso para ; portanto, a restrição que não vale para . Portanto, pode alterar o valor, que é também o que é imposto pela terceira fórmula.

Para que essa condição funcione, os predicados de oclusão precisam ser verdadeiros apenas quando se tornam verdadeiros como efeito de uma ação. Isso pode ser alcançado pela circunscrição ou pela conclusão do predicado. É importante notar que a oclusão não implica necessariamente uma mudança: por exemplo, executar a ação de abrir a porta já aberta (na formalização acima) torna o predicado verdadeiro e torna verdadeiro; no entanto, não mudou de valor, como já era verdade.

Solução de completação de predicado

Essa codificação é semelhante à solução de oclusão fluente, mas os predicados adicionais denotam mudança, não permissão para mudar. Por exemplo, representa o fato de que o predicado mudará de tempos em tempos . Como resultado, um predicado muda se e somente se o predicado de mudança correspondente for verdadeiro. Uma ação resulta em uma mudança se e somente se torna verdadeira uma condição que era anteriormente falsa ou vice-versa.

A terceira fórmula é uma maneira diferente de dizer que abrir a porta faz com que a porta seja aberta. Precisamente, afirma que a abertura da porta altera o estado da porta se ela tivesse sido fechada anteriormente. As duas últimas condições afirmam que uma condição altera o valor no momento, se e somente se o predicado de alteração correspondente for verdadeiro no momento . Para completar a solução, os pontos de tempo em que os predicados de mudança são verdadeiros devem ser os menores possíveis, e isso pode ser feito aplicando a conclusão de predicado às regras que especificam 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 pelo 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 de estado sucessor é uma formalização na lógica desses dois fatos. Por exemplo, se e são duas condições usadas para denotar que a ação executada no momento era abrir ou fechar a porta, respectivamente, o exemplo em execução é codificado da seguinte maneira.

Essa solução é centrada no valor das condições, e não nos efeitos das ações. Em outras palavras, existe um axioma para cada condição, ao invés de uma fórmula para cada ação. As pré-condições para ações (que não estão presentes neste exemplo) são formalizadas por outras fórmulas. Os axiomas de estado sucessor 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 termos lógicos de primeira ordem , em vez de predicados, para representar os estados. A conversão de predicados em termos na lógica de primeira ordem é chamada de reificação ; o cálculo fluente pode ser visto como uma lógica na qual predicados que representam o 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 avaliada sobre um determinado conjunto de termos.

No cálculo fluente, cada estado possível é representado por um termo obtido pela 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 acesa é representado pelo termo . É importante notar que um termo não é verdadeiro ou falso por si só, pois é um objeto e não uma condição. Em outras palavras, o termo representa um estado possível e não significa por si só que esse é o estado atual. Uma condição separada pode ser estabelecida para especificar que este é realmente o estado em um determinado momento, por exemplo, significa que este é o estado no momento .

A solução para o problema de quadro dado 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 momento 0 é representada pela fórmula:

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

Esta fórmula funciona desde que sejam fornecidos axiomas adequados sobre e , por exemplo, um termo contendo a mesma condição duas vezes não é um estado válido (por exemplo, é sempre falso para todos e ).

Solução de cálculo de eventos

O cálculo de evento usa termos para representar fluentes, como o cálculo fluente, mas também tem axiomas que restringem o valor dos fluentes, como os axiomas de estado sucessor. No cálculo de evento, a inércia é reforçada por fórmulas que afirmam que um fluente é verdadeiro se tiver sido verdadeiro em um determinado ponto de tempo anterior e nenhuma ação de alterá-lo para falso foi realizada nesse ínterim. O preenchimento do predicado ainda é necessário no cálculo do evento para obter que um fluente se torne verdadeiro apenas se uma ação que o torna verdadeiro tiver sido executada, mas também para obter que uma ação foi executada apenas se isso for explicitamente declarado.

Solução lógica padrão

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

(se for verdadeiro na situação , e pode ser assumido que permanece verdadeiro após a execução da ação , então podemos concluir que permanece verdadeiro).

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

Solução de programação de conjunto de respostas

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

(se for verdadeiro no momento , e pode ser assumido que permanece verdadeiro no momento , então podemos concluir que permanece verdadeiro).

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

A lógica de separação é um formalismo para raciocinar sobre programas de computador usando especificações pré / pós do formulário . A lógica de separação é uma extensão da lógica de Hoare orientada para o raciocínio sobre estruturas de dados mutáveis ​​na memória do computador e outros recursos dinâmicos, e tem um conectivo especial *, pronunciado "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 de especificações pré / pós, que dizem que o código só pode acessar locais de memória garantidos para existir pela pré-condição. Isso leva à solidez da regra de inferência mais importante da lógica, a regra de quadro

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

captura aquele código que classifica uma lista x não remove a classificação de uma lista separada y, e faz isso sem mencionar y na 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, eventualmente implantadas industrialmente em bases de código com 10s de milhões de linhas.

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

Linguagens de descrição de ação

As linguagens de descrição de ação evitam 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 abre a porta, se não estiver trancada, é expresso por:

causa se

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

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

Veja também

Notas

Referências

links externos