Problema de marco - Frame problem

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. 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 posteriores, 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 tales como cómo proporcionar supuestos por defecto racionales y lo que los humanos consideran de sentido común en un entorno virtual. Posteriormente, 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 se especifican típicamente 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 estar abierta o cerrada, y una luz, que puede estar encendida o apagada, está representada estáticamente por dos proposiciones y . Si estas condiciones pueden cambiar, están mejor representadas por dos predicados y que dependen del tiempo; tales predicados se denominan fluidos . Un dominio en el que la puerta está cerrada y la luz apagada en el momento 0, y la puerta abierta en el momento 1, se puede representar directamente en lógica mediante las siguientes fórmulas:

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 que la puerta se desbloqueara, se habría representado por . En la práctica, uno tendría un predicado para especificar cuándo se ejecuta una acción y una regla para especificar los efectos de las acciones. El artículo sobre el cálculo de situaciones ofrece más detalles.

Si bien las tres fórmulas anteriores son una expresión directa en la lógica de lo que se conoce, no son suficientes para dibujar 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.

   

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

   

El problema del marco es que especificar solo qué condiciones cambian mediante las acciones no implica que no se cambien todas las demás condiciones. Este problema se puede resolver agregando los llamados "axiomas marco", que especifican explícitamente que todas las condiciones no afectadas por las acciones no se modifican durante la ejecución de 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 indicaría que el estado de la luz no cambia del tiempo 0 al tiempo 1:

El problema del marco es que uno de esos axiomas del marco es necesario para cada par de acción y condición de manera que la acción no afecte a 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 asumir que se ha producido una cantidad mínima de cambios de condición; esta solución se formaliza en el marco de la circunscripción . El problema del rodaje de Yale , sin embargo, muestra que esta solución no siempre es correcta. A continuación, se propusieron soluciones alternativas que incluían la terminación de predicados, la oclusión fluida, los axiomas del 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 de marco" se siguió utilizando, 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 describen cómo se resuelve el problema del marco en varios formalismos. Los formalismos en sí mismos 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.

El fundamento 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 dado si se acaba de ejecutar una acción que hace que la condición sea verdadera o falsa como efecto. La oclusión puede verse como "permiso para cambiar": si una condición está ocluida, se libera de obedecer la restricción de la inercia.

En el ejemplo simplificado de la puerta y la luz, la oclusión se puede formalizar mediante dos predicados y . La razón es que una condición puede cambiar de valor solo si el predicado de oclusión correspondiente es verdadero en el siguiente momento. A su vez, el predicado de oclusión es verdadero solo cuando se ejecuta una acción que afecta la condición.

En general, cada acción que hace que una condición sea verdadera o falsa también hace que el predicado de oclusión correspondiente sea verdadero. En este caso, es verdadero, por lo que el antecedente de la cuarta fórmula anterior es falso para ; por lo tanto, la restricción que no se cumple . Por lo tanto, puede cambiar el valor, que es también lo que impone la tercera fórmula.

Para que esta condición funcione, los predicados de oclusión deben ser verdaderos solo cuando se convierten en verdaderos como efecto de una acción. Esto se puede lograr mediante la circunscripción o mediante la terminación del predicado. 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 que el predicado sea verdadero y lo hace verdadero; sin embargo, no ha cambiado de valor, como ya era cierto.

Solución de terminación de predicados

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, representa el hecho de que el predicado cambiará de vez en cuando . Como resultado, un predicado cambia si y solo si el predicado de cambio correspondiente es verdadero. Una acción da como resultado un cambio si y solo si convierte en verdadera una condición que antes era falsa o viceversa.

La tercera fórmula es una forma diferente de decir que abrir la puerta hace que se abra la puerta. Precisamente, afirma que la apertura de la puerta cambia el estado de la puerta si se hubiera cerrado previamente. Las dos últimas condiciones establecen que una condición cambia de valor en el momento si y solo si el predicado de cambio correspondiente es verdadero en el momento . Para completar la solución, los puntos de tiempo en los que los predicados de cambio son verdaderos deben ser los menos posibles, y esto se puede hacer aplicando la terminación de predicados 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 determinarse por el hecho de que la condición es verdadera si y solo si:

  1. la acción hace que la condición sea verdadera; o
  2. la condición era previamente verdadera y la acción no la convierte en falsa.

Un axioma de estado sucesor es una formalización lógica de estos dos hechos. Por ejemplo, si y son dos condiciones que se utilizan para indicar que la acción ejecutada en el momento era abrir o cerrar la puerta, respectivamente, el ejemplo en ejecución se codifica de la siguiente manera.

Esta solución se centra en el valor de las condiciones, más que en los efectos de las acciones. En otras palabras, existe un axioma para cada condición, más que una fórmula para cada acción. Las condiciones previas a las acciones (que no están presentes en este ejemplo) se formalizan mediante otras fórmulas. Los axiomas del estado sucesor se utilizan en la variante del cálculo de situaciones propuesto por Ray Reiter .

Solución de cálculo fluida

El cálculo fluido es una variante del cálculo de situaciones. Resuelve el problema del marco utilizando términos lógicos de primer orden , en lugar de predicados, para representar los estados. Convertir predicados en términos en lógica de primer orden se llama reificación ; el cálculo fluido puede verse como una lógica en la que se cosifican los predicados que representan el estado 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 se evalúa sobre un determinado conjunto de términos.

En el cálculo fluido, cada estado posible está representado por un término obtenido por 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 . 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 representa un estado posible y no significa por sí mismo que este sea el estado actual. Se puede establecer una condición separada para especificar que este es realmente el estado en un momento dado, por ejemplo, significa que este es el estado en el momento .

La solución al problema del marco dada 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:

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:

Esta fórmula funciona siempre que se den axiomas adecuados sobre y , por ejemplo, un término que contiene la misma condición dos veces no es un estado válido (por ejemplo, siempre es falso para todos y ).

Solución de cálculo de eventos

El cálculo de eventos usa términos para representar fluidos, como el cálculo fluido, pero también tiene axiomas que restringen el valor de los fluidos, como los axiomas del estado sucesor. En el caso de cálculo, la inercia se aplica mediante fórmulas que indican que un fluido es verdadero si ha sido verdadero en un punto de tiempo anterior dado y no se ha realizado ninguna acción para cambiarlo a falso mientras tanto. La finalización de predicados todavía es necesaria en el cálculo de eventos para obtener que un fluido se haga verdadero solo si se ha realizado una acción que lo hace verdadero, pero también para obtener que una acción se haya realizado solo si eso se establece explícitamente.

Solución lógica predeterminada

El problema del marco puede pensarse 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 :

(si es cierto en una situación , y se puede suponer que sigue siendo cierto después de ejecutar la acción , entonces podemos concluir que sigue siendo cierto).

Steve Hanks y Drew McDermott argumentaron, sobre la base de su ejemplo de rodaje de 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 conjuntos de respuestas

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

(si es cierto en el momento , y se puede suponer que sigue siendo cierto en el momento , entonces podemos concluir que sigue siendo cierto).

Solución lógica de separación

La lógica de separación es un formalismo para razonar sobre programas de computadora utilizando especificaciones previas / posteriores del formulario . La lógica de separación es una extensión de la lógica de Hoare orientada al razonamiento 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 respaldar el razonamiento independiente sobre regiones de memoria disjuntas.

La lógica de separación emplea una interpretación estricta de las especificaciones previas / posteriores, que dicen que el código solo puede acceder a ubicaciones de memoria cuya existencia se garantiza mediante la condición previa. Esto conduce a la solidez de la regla de inferencia más importante de la lógica, la regla del marco.

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

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

La automatización de la regla del marco ha dado lugar a aumentos significativos en la escalabilidad de las técnicas de razonamiento automatizado para el código, que finalmente se implementaron industrialmente en bases de código con decenas de millones de líneas.

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

Idiomas de descripción de acciones

Los lenguajes de descripción de acciones eluden el problema del marco en lugar de resolverlo. Un lenguaje de descripción de acciones es un lenguaje formal con una sintaxis específica para describir situaciones y acciones. Por ejemplo, que la acción hace que la puerta se abra si no está bloqueada se expresa mediante:

causas si

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 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 en lógica. Normalmente, sin embargo, se proporciona una traducción de estos lenguajes para responder a la programación de conjuntos en lugar de la lógica de primer orden.

Ver también

Notas

Referencias

enlaces externos