Problema de marco

En inteligencia artificial, el problema del marco describe un problema con el uso de lógica de primer orden (FOL) para expresar hechos sobre un robot en el mundo. Representar el estado de un robot con FOL tradicional requiere el uso de muchos axiomas que simplemente implican que las cosas en el entorno no cambian arbitrariamente. Por ejemplo, Hayes describe un "mundo de bloques" con reglas sobre apilar bloques juntos. En un sistema FOL, se requieren axiomas adicionales para hacer inferencias sobre el entorno (por ejemplo, que un bloque no puede cambiar de posición a menos que se mueva físicamente). El problema del marco es el problema de encontrar colecciones adecuadas de axiomas para una descripción viable de un entorno de robot.

John McCarthy y Patrick J. Hayes definieron este problema en su artículo de 1969, Algunos problemas filosóficos desde el punto de vista de la inteligencia artificial. En este artículo, y en muchos que vinieron después, el problema matemático formal fue un punto de partida para discusiones más generales sobre la dificultad de la representación del conocimiento para la inteligencia artificial. Cuestiones como la forma de proporcionar suposiciones predeterminadas racionales y lo que los humanos consideran sentido común en un entorno virtual. Más tarde, el término adquirió un significado más amplio en la filosofía, donde se formula como el problema de limitar las creencias que deben actualizarse en respuesta a las acciones. En el contexto lógico, las acciones generalmente se especifican por lo que cambian, con la suposición implícita de que todo lo demás (el marco) permanece sin cambios.

Descripción

El problema del marco ocurre incluso en dominios muy simples. Un escenario con una puerta, que puede ser abierta o cerrada, y una luz, que puede estar encendido o apagado, está estadísticamente representado por dos proposiciones open{displaystyle mathrm {open} y on{displaystyle mathrm {on}. Si estas condiciones pueden cambiar, están mejor representados por dos predicados open()t){displaystyle mathrm {open} (t)} y on()t){displaystyle mathrm {on} (t)} que dependen del tiempo; tales predicados se llaman fluidos. Un dominio en el que la puerta está cerrada y la luz apagada a la hora 0, y la puerta abierta a la hora 1, puede ser representado directamente en la lógica por las siguientes fórmulas:

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

¬ ¬ on()0){displaystyle neg mathrm {on} (0)}

open()1){displaystyle mathrm {open} (1)}

Las dos primeras fórmulas representan la situación inicial; la tercera fórmula representa el efecto de ejecutar la acción de abrir la puerta en el momento 1. Si tal acción tuviera condiciones previas, como la puerta que se desbloquea, habría estado representada por ¬ ¬ locked()0)⟹ ⟹ open()1){displaystyle neg mathrm {locked} (0) 'implies mathrm {open} (1)}. En la práctica, uno tendría un predicado executeopen()t){displaystyle mathrm {executeopen} (t)} para especificar cuándo se ejecuta una acción y una regla О О t.executeopen()t)⟹ ⟹ open()t+1){displaystyle forall t.mathrm {executeopen} (t)implies mathrm {open} (t+1)} para especificar los efectos de las acciones. El artículo sobre el cálculo de la situación da más detalles.

Si bien las tres fórmulas anteriores son una expresión lógica directa de lo que se sabe, no son suficientes para extraer correctamente las consecuencias. Si bien las siguientes condiciones (que representan la situación esperada) son consistentes con las tres fórmulas anteriores, no son las únicas.

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

De hecho, otro conjunto de condiciones que es consistente con las tres fórmulas anteriores es:

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

El problema del marco es que especificar solo qué condiciones cambian las acciones no implica que todas las demás condiciones no cambien. Este problema se puede resolver agregando los llamados "axiomas de marco", que especifican explícitamente que todas las condiciones que no se ven afectadas por las acciones no se modifican mientras se ejecuta esa acción. Por ejemplo, dado que la acción ejecutada en el tiempo 0 es la de abrir la puerta, un axioma del marco establecería que el estado de la luz no cambia del tiempo 0 al tiempo 1:

on()0)⟺ ⟺ on()1){displaystyle mathrm {on} (0)iff mathrm {on} (1)}

El problema del marco es que uno de esos axiomas del marco es necesario para cada par de acción y condición tal que la acción no afecte la condición. En otras palabras, el problema es el de formalizar un dominio dinámico sin especificar explícitamente los axiomas del marco.

La solución propuesta por McCarthy para resolver este problema implica suponer que se ha producido una cantidad mínima de cambios de condición; esta solución se formaliza utilizando el marco de la circunscripción. El problema del tiroteo de Yale, sin embargo, muestra que esta solución no siempre es correcta. Luego se propusieron soluciones alternativas, que involucraron la terminación de predicados, la oclusión fluida, los axiomas de estado sucesor, etc.; se explican a continuación. A fines de la década de 1980, se resolvió el problema del marco definido por McCarthy y Hayes. Incluso después de eso, sin embargo, el término "problema del marco" todavía se usaba, en parte para referirse al mismo problema pero bajo diferentes escenarios (por ejemplo, acciones concurrentes), y en parte para referirse al problema general de representar y razonar con dinámicas. dominios

Soluciones

Las siguientes soluciones muestran cómo se resuelve el problema del marco en varios formalismos. Los formalismos en sí no se presentan en su totalidad: lo que se presenta son versiones simplificadas que son suficientes para explicar la solución completa.

Solución de oclusión fluida

Esta solución fue propuesta por Erik Sandewall, quien también definió un lenguaje formal para la especificación de dominios dinámicos; por lo tanto, dicho dominio puede expresarse primero en este idioma y luego traducirse automáticamente a la lógica. En este artículo, solo se muestra la expresión en lógica, y solo en el lenguaje simplificado sin nombres de acción.

La lógica de esta solución es representar no solo el valor de las condiciones a lo largo del tiempo, sino también si pueden verse afectadas por la última acción ejecutada. Este último está representado por otra condición, llamada oclusión. Se dice que una condición está ocluida en un punto de tiempo determinado si acaba de ejecutarse una acción que hace que la condición sea verdadera o falsa como efecto. La oclusión puede verse como un "permiso para cambiar": si se ocluye una condición, se le libera de obedecer la restricción de la inercia.

En el ejemplo simplificado de la puerta y la luz, la oclusión puede ser formalizada por dos predicados occludeopen()t){displaystyle mathrm {occludeopen} (t)} y occludeon()t){displaystyle mathrm {occludeon} (t)}. La justificación es que una condición puede cambiar el valor sólo si el predicado de oclusión correspondiente es cierto en el momento siguiente. A su vez, el predicado de oclusión es cierto sólo cuando una acción que afecta a la condición es ejecutada.

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

¬ ¬ on()0){displaystyle neg mathrm {on} (0)}

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

О О t.¬ ¬ occludeopen()t)⟹ ⟹ ()open()t− − 1)⟺ ⟺ open()t)){displaystyle forall t.neg mathrm {occludeopen} (t)implies (mathrm {open} (t-1)iff mathrm {open} (t)}}

О О t.¬ ¬ occludeon()t)⟹ ⟹ ()on()t− − 1)⟺ ⟺ on()t)){displaystyle forall t.neg mathrm {occludeon} (t)implies (mathrm {on} (t-1)iff mathrm {on} (t)}}

En general, cada acción que hace una condición verdadera o falsa también hace que la oclusión correspondiente predicar verdadero. En este caso, occludeopen()1){displaystyle mathrm {occludeopen} (1)} es cierto, haciendo el antecedente de la cuarta fórmula por encima de falso t=1{displaystyle t=1}; por consiguiente, la limitación de que open()t− − 1)⟺ ⟺ open()t){displaystyle mathrm {open} (t-1)iff mathrm {open} (t)} no espera t=1{displaystyle t=1}. Por lo tanto, open{displaystyle mathrm {open} puede cambiar el valor, que es también lo que se aplica por la tercera fórmula.

Para que esta condición funcione, los predicados de oclusión tienen que ser verdaderos sólo cuando se hacen realidad como un efecto de una acción. Esto se puede lograr ya sea por circunscripción o por terminación predicada. Vale la pena notar que la oclusión no implica necesariamente un cambio: por ejemplo, ejecutar la acción de abrir la puerta cuando ya estaba abierta (en la formalización anterior) hace el predicado occludeopen{displaystyle mathrm {occludeopen} verdadero y open{displaystyle mathrm {open} verdadero; sin embargo, open{displaystyle mathrm {open} no ha cambiado el valor, ya que era cierto.

Solución de finalización predicada

Esta codificación es similar a la solución de oclusión fluida, pero los predicados adicionales denotan cambio, no permiso para cambiar. Por ejemplo, changeopen()t){displaystyle mathrm {changeopen} (t)} representa el hecho de que el predicado open{displaystyle mathrm {open} cambiará de tiempo t{displaystyle t} a t+1{displaystyle t+1}. Como resultado, un predicado cambia si y sólo si el correspondiente cambio predicado es cierto. Una acción resulta en un cambio si y sólo si hace realidad una condición que era anteriormente falsa o viceversa.

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

¬ ¬ on()0){displaystyle neg mathrm {on} (0)}

¬ ¬ open()0)⟹ ⟹ changeopen()0){displaystyle neg mathrm {open} (0)implies mathrm {changeopen} (0)}

О О t.changeopen()t)⟺ ⟺ ()¬ ¬ open()t)⟺ ⟺ open()t+1)){displaystyle forall t.mathrm {changeopen} (t)iff (neg mathrm {open} (t)iff mathrm {open} (t+1)}

О О t.changeon()t)⟺ ⟺ ()¬ ¬ on()t)⟺ ⟺ on()t+1)){displaystyle forall t.mathrm {changeon} (t)iff (neg mathrm {on} (t)iff mathrm {on} (t+1)}

La tercera fórmula es una manera diferente de decir que abrir la puerta hace que la puerta sea abierta. Precisamente, afirma que abrir la puerta cambia el estado de la puerta si había sido previamente cerrada. Las dos últimas condiciones indican que una condición cambia de valor a tiempo t{displaystyle t} si y sólo si el determinante del cambio correspondiente es verdadero en el tiempo t{displaystyle t}. Para completar la solución, los puntos de tiempo en los que los determinantes del cambio son verdaderos tienen que ser tan pocos como sea posible, y esto se puede hacer aplicando la terminación predicada a las reglas que especifican los efectos de las acciones.

Solución de axiomas de estado sucesor

El valor de una condición después de la ejecución de una acción puede ser determinado por el hecho de que la condición es verdadera si y sólo si:

1. la acción hace que la condición sea verdadera; o
2. la condición era anteriormente verdadera y la acción no lo hace falso.

Un axioma estatal sucesor es una formalización en la lógica de estos dos hechos. Para ejemplo, si opendoor()t){displaystyle mathrm {opendoor} (t)} y closedoor()t){displaystyle mathrm {closedoor} (t)} dos condiciones utilizadas para denotar que la acción ejecutada a tiempo t{displaystyle t} era para abrir o cerrar la puerta, respectivamente, el ejemplo de funcionamiento se codifica como sigue.

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

¬ ¬ on()0){displaystyle neg mathrm {on} (0)}

opendoor()0){displaystyle mathrm {opendoor} (0)}

О О t.open()t+1)⟺ ⟺ opendoor()t)Alternativa Alternativa ()open()t)∧ ∧ ¬ ¬ closedoor()t)){displaystyle forall t.mathrm {open} (t+1)iff mathrm {opendoor} (t)vee (mathrm {open} (t)wedge neg mathrm {closedoor} (t)}}}

Esta solución se centra en el valor de las condiciones, en lugar de la efectos de las acciones. En otras palabras, hay un axioma para cada condición, en lugar de una fórmula para cada acción. Condiciones previas a las acciones (que no son presentes en este ejemplo) se formalizan mediante otras fórmulas. El estado sucesor Los axiomas se utilizan en la variante al cálculo de situación propuesta por Ray Reiter.

Solución de cálculo fluido

El cálculo fluido es una variante del cálculo de situación. Resuelve el problema del marco usando lógica de primer orden. términos, en lugar de predicados, para representar los estados. Mudado predicados en términos en la lógica de primer orden se llama cosificación; el El cálculo fluido puede verse como una lógica en la que los predicados que representan el se cosifican los estados de condiciones.

La diferencia entre un predicado y un término en la lógica de primer orden es que un término es una representación de un objeto (posiblemente un objeto complejo compuesto por otros objetos), mientras que un predicado representa una condición que puede ser verdadera o falsa cuando evaluada sobre un conjunto dado de términos.

En el cálculo fluido, cada estado posible está representado por un término obtenido por la composición de otros términos, cada uno representando las condiciones que son verdaderas en el estado. Por ejemplo, el estado en el que la puerta está abierta y la luz está encendida está representado por el término open∘ ∘ on{displaystyle mathrm {open} circ mathrm {on}. Es importante notar que un término no es verdadero o falso por sí mismo, ya que es un objeto y no una condición. En otras palabras, el término open∘ ∘ on{displaystyle mathrm {open} circ mathrm {on} representar un estado posible, y no significa por sí mismo que este es el estado actual. Se puede indicar una condición separada para especificar que este es en realidad el estado en un momento dado, por ejemplo, state()open∘ ∘ on,10){displaystyle mathrm {state} (mathrm {open} circ mathrm {on}10)} significa que este es el estado a tiempo 10{displaystyle 10}.

La solución al problema del marco dado en el cálculo fluido es especificar los efectos de las acciones indicando cómo cambia un término que representa el estado cuando se ejecuta la acción. Por ejemplo, la acción de abrir la puerta en el tiempo 0 está representada por la fórmula:

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

La acción de cerrar la puerta, que hace que una condición sea falsa en lugar de verdadera, se representa de una manera ligeramente diferente:

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

Esta fórmula funciona siempre que se dan axiomas adecuados state{displaystyle mathrm {state} y ∘ ∘ {displaystyle circ }, por ejemplo, un término que contiene la misma condición dos veces no es un estado válido (por ejemplo, state()open∘ ∘ s∘ ∘ open,t){displaystyle mathrm {state} (mathrm {open} circ scirc mathrm {open}t)} es siempre falso para cada s{displaystyle s} y t{displaystyle t}).

Solución de cálculo de eventos

El cálculo de eventos utiliza términos para representar fluidez, como el cálculo de fluidez, pero también tiene axiomas que restringen el valor de fluidez, como los axiomas de estado sucesor. En el cálculo de eventos, la inercia se impone mediante fórmulas que establecen que un fluido es verdadero si ha sido verdadero en un punto de tiempo anterior dado y mientras tanto no se ha realizado ninguna acción para cambiarlo a falso. La terminación de predicados sigue siendo necesaria en el cálculo de eventos para obtener que un fluent se hace verdadero solo si se ha realizado una acción que lo hace verdadero, pero también para obtener que una acción se ha realizado solo si eso se establece explícitamente.

Solución lógica predeterminada

El problema del marco se puede considerar como el problema de formalizar el principio de que, por defecto, "se presume que todo permanece en el estado en que se encuentra" (Leibniz, "Introducción a una enciclopedia secreta", c. 1679). Este valor predeterminado, a veces llamado la ley de inercia del sentido común, fue expresado por Raymond Reiter en la lógica predeterminada:

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

(si R()x){displaystyle R(x)} es cierto en la situación s{displaystyle s}, y se puede suponer que R()x){displaystyle R(x)} se mantiene fiel después de la ejecución de medidas a{displaystyle a}, entonces podemos concluir que R()x){displaystyle R(x)} sigue siendo cierto).

Steve Hanks y Drew McDermott argumentaron, sobre la base de su ejemplo de tiro en Yale, que esta solución al problema del marco no es satisfactoria. Hudson Turner demostró, sin embargo, que funciona correctamente en presencia de postulados adicionales apropiados.

Solución de programación de conjunto de respuestas

La contrapartida de la solución lógica predeterminada en el lenguaje de programación del conjunto de respuestas es una regla con negación fuerte:

r()X,T+1)← ← r()X,T),no♪ ♪ r()X,T+1){displaystyle r(X,T+1)leftarrow r(X,T), {hbox{not }sim r(X,T+1)}

(si r()X){displaystyle r(X)} es verdad a tiempo T{displaystyle T}, y se puede suponer que r()X){displaystyle r(X)} sigue siendo cierto a la vez T+1{displaystyle T+1}, entonces podemos concluir que r()X){displaystyle r(X)} sigue siendo cierto).

Solución lógica de separación

La lógica de separación es un formalismo para razonar sobre programas informáticos utilizando especificaciones pre/post de la forma {}precondition}code{}postcondition}{displaystyle {mathrm {precondition} }mathrm {code} {mathrm {postcondition} {}}. La lógica de separación es una extensión de la lógica Hoare orientada a razonar sobre estructuras de datos mutables en la memoria de la computadora y otros recursos dinámicos, y tiene un * conector especial, pronunciado "y por separado", para apoyar el razonamiento independiente sobre las regiones de memoria descomunadas.

La lógica de separación emplea una interpretación restringida de las especificaciones previas y posteriores, que dice que el código solo puede acceder a las ubicaciones de memoria cuya existencia está garantizada por la condición previa. Esto lleva a la solidez de la regla de inferencia más importante de la lógica, la regla del marco

{}precondition}code{}postcondition}{}preconditionAlternativa Alternativa frame}code{}postconditionAlternativa Alternativa frame}{displaystyle {frac {fnMicrosoft Sans Serif} }mathrm {code} {mathrm {postcondition} {\fnMicrom {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif} {fnMicrosoft Sans Serif}}} {fnMicrom {fnMicrosoft} {fnMicrom} {fnMicrom {fnMicrom {fnMicrom} {fnMicrosoft}}}}}}} {f}}}}} {f}}}} {\\\\fnMicrom} {fnMicrom} {fnMicrom}}}}}}}}}}}}} {\\\\\\\\\fnMicrom} {fnMicrom {\\\\fnMicrom}}}}}} {\fnMicrom}} {\fnMicrom {fnMicrom {fnMicrom}}}}}}} ast mathrm {frame} } mathrm {code} {mathrm {postcondition} ast mathrm {frame}}}}}}}}

La regla del marco permite que se agreguen a una especificación descripciones de memoria arbitraria fuera de la huella (memoria a la que se accede) del código: esto permite que la especificación inicial se concentre solo en la huella. Por ejemplo, la inferencia

{}lista⁡ ⁡ ()x)}code{}Lista clasificada⁡ ⁡ ()x)}{}lista⁡ ⁡ ()x)Alternativa Alternativa Lista clasificada⁡ ⁡ ()Sí.)}code{}Lista clasificada⁡ ⁡ ()x)Alternativa Alternativa Lista clasificada⁡ ⁡ ()Sí.)}{displaystyle {frac {\{fnMinisterio {list}(x)}\mathrm {code} {\\\\\fnMiembro {} {fnMiembro de operador} {cluido} {fnMiembro de operador} {fnMie)} {fnMicrosoft} {fnMicrosoft}fnMicrosoft}fnMicrosoft}fnMicrosoft}fnMicrosoft}fnMicronombre {f}fnMicrosoft}fnMicrosoft}fnMicrosoft}fnMicrosoft}fnMinMinMicrosoft}fnMicrosoft}fnMinMinMinMicrosoft}fnMicrosoft}fnción {fnMicrosoft {fnMicrosoft}

captura el código que ordena una lista x no ordena una lista separada y, y lo hace sin mencionar y en absoluto en la especificación inicial encima de la línea.

La automatización de la regla del marco ha llevado a aumentos significativos en la escalabilidad de las técnicas de razonamiento automatizado para el código, eventualmente implementadas industrialmente en bases de código con decenas de millones de líneas.

Parece haber cierta similitud entre la solución lógica de separación del problema del marco y la del cálculo fluido mencionado anteriormente.

Idiomas de descripción de acciones

Los idiomas de descripción de la acción eluden el problema del marco en lugar de resolverlo. Un lenguaje de descripción de la acción es un lenguaje formal con una sintaxis específica para describir situaciones y acciones. Por ejemplo, que la acción opendoor{displaystyle mathrm {opendoor} hace que la puerta abierta si no cerrada se expresa por:

opendoor{displaystyle mathrm {opendoor} causas open{displaystyle mathrm {open} si ¬ ¬ locked{displaystyle neg mathrm {locked}

La semántica de un lenguaje de descripción de acciones depende de lo que el lenguaje pueda expresar (acciones concurrentes, efectos retardados, etc.) y generalmente se basa en sistemas de transición.

Dado que los dominios se expresan en estos lenguajes en lugar de directamente en la lógica, el problema del marco solo surge cuando una especificación dada en una lógica de descripción de acción debe traducirse a lógica. Sin embargo, por lo general, se da una traducción de estos lenguajes para responder a la programación de conjuntos en lugar de la lógica de primer orden.