stringtranslate.com

Problema de marco

En inteligencia artificial , con implicaciones para la ciencia cognitiva , el problema del marco describe un problema con el uso de la lógica de primer orden para expresar hechos sobre un robot en el mundo. Representar el estado de un robot con la lógica tradicional de primer orden 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 de lógica de primer orden, 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. [1]

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 otros posteriores, el problema matemático formal fue el 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 supuestos racionales predeterminados y lo que los humanos consideran sentido común en un entorno virtual. [2]

En filosofía , el problema del marco se interpretó de manera más amplia en relación con el problema de limitar las creencias que deben actualizarse en respuesta a las acciones. En el contexto lógico, las acciones suelen especificarse por lo que cambian, con la suposición implícita de que todo lo demás (el marco) permanece inalterado.

Descripción

El problema del marco se presenta 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, se representa estáticamente mediante dos proposiciones y . Si estas condiciones pueden cambiar, se representan mejor mediante dos predicados y que dependen del tiempo; dichos predicados se denominan fluentes . Un dominio en el que la puerta está cerrada y la luz apagada en el tiempo 0, y la puerta abierta en el tiempo 1, se puede representar directamente en lógica [ aclaración necesaria ] 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 dicha acción tuviera condiciones previas, como que la puerta estuviera desbloqueada, 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 proporciona más detalles.

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

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

El problema del marco es que especificar únicamente qué condiciones cambian con las acciones no implica que no se cambien todas las demás condiciones. Este problema se puede resolver añadiendo los llamados “axiomas del marco”, que especifican explícitamente que no se modifican todas las condiciones no afectadas por las acciones mientras se ejecuta esa acción. Por ejemplo, dado que la acción ejecutada en el momento 0 es la de abrir la puerta, un axioma del marco indicaría que el estado de la luz no cambia del momento 0 al momento 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 a la condición. [ aclaración necesaria ] 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 involucraban la finalizació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 tal como lo definieron McCarthy y Hayes [ aclaración necesaria ] . Sin embargo, incluso después de eso, el término "problema del marco" todavía se usaba, en parte para referirse al mismo problema pero en diferentes entornos (por ejemplo, acciones concurrentes), y en parte para referirse al problema general de representar y razonar con dominios dinámicos.

Soluciones

Las siguientes soluciones ilustran 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 lenguaje y luego traducirse automáticamente a lógica. En este artículo, solo se muestra la expresión en lógica y solo en el lenguaje simplificado sin nombres de acciones.

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. Esto último se representa mediante otra condición, llamada oclusión. Se dice que una condición está ocluida en un momento 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 un “permiso para cambiar”: si una condición está ocluida, se libera de obedecer la restricción de 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 punto temporal. A su vez, el predicado de oclusión es verdadero solo cuando se ejecuta una acción que afecta a 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, lo que hace que el antecedente de la cuarta fórmula anterior sea falso para ; por lo tanto, la restricción que no se cumple para . Por lo tanto, puede cambiar de valor, que es también lo que aplica la tercera fórmula.

Para que esta condición funcione, los predicados de oclusión deben ser verdaderos solo cuando se hacen verdaderos como efecto de una acción. Esto se puede lograr ya sea por circunscripción o por completitud de 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 hace que true; sin embargo, no ha cambiado de valor, ya que ya era verdadero.

Solución de compleción de predicado

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 tiempo a . 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 al abrir la puerta se abre la puerta. Precisamente, establece que al abrir la puerta se cambia el estado de la puerta si hubiera estado cerrada previamente. Las dos últimas condiciones establecen que una condición cambia de valor en el tiempo si y solo si el predicado de cambio correspondiente es verdadero en el tiempo . Para completar la solución, los puntos de tiempo en los que los predicados de cambio son verdaderos tienen que ser los menos posibles, y esto se puede hacer aplicando la finalización de predicados a las reglas que especifican los efectos de las acciones.

Solución de axiomas de estados sucesores

El valor de una condición después de la ejecución de una acción se puede determinar 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 anteriormente verdadera y la acción no la hace falsa.

Un axioma de estado sucesor es una formalización en 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 fue abrir o cerrar la puerta, respectivamente, el ejemplo de 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, en lugar de una fórmula para cada acción. Las precondiciones de las acciones (que no están presentes en este ejemplo) se formalizan mediante otras fórmulas. Los axiomas de estado sucesor se utilizan en la variante del cálculo de situaciones propuesta por Ray Reiter .

Solución de cálculo fluido

El cálculo fluido es una variante del cálculo de situaciones. Resuelve el problema del marco utilizando términos de lógica de primer orden , en lugar de predicados, para representar los estados. La conversión de predicados en términos de lógica de primer orden se denomina cosificación ; el cálculo fluido puede considerarse como una lógica en la que se cosifican los predicados que representan el estado de las 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 de otros objetos), mientras que un predicado representa una condición que puede ser verdadera o falsa cuando se evalúa sobre un conjunto dado de términos.

En el cálculo fluido, cada estado posible se representa mediante un término obtenido por composición de otros términos, cada uno de los cuales representa las condiciones que son verdaderas en el estado. Por ejemplo, el estado en el que la puerta está abierta y la luz está encendida se representa mediante 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 enunciar 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 que se da en el cálculo fluido consiste en 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 momento 0 se representa con 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 proporcionen 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 cada y ).

Solución de cálculo de eventos

El cálculo de eventos utiliza términos para representar fluidos, como el cálculo fluido, pero también tiene uno o más axiomas que restringen el valor de los fluidos, como los axiomas de estado sucesor. Existen muchas variantes del cálculo de eventos, pero una de las más simples y útiles emplea un solo axioma para representar la ley de inercia:

El axioma establece que un fluido se cumple en un tiempo , si un evento sucede y se inicia en un tiempo anterior , y no hay ningún evento que suceda y termine después o al mismo tiempo que y antes .

Para aplicar el cálculo de eventos a un dominio de problemas en particular, es necesario definir los predicados y para ese dominio. Por ejemplo:

Para aplicar el cálculo de eventos a un problema particular del dominio, es necesario especificar los eventos que ocurren en el contexto del problema. Por ejemplo:

.
.

Para resolver un problema, como por ejemplo ¿qué fluidos se mantienen en el tiempo 5?, es necesario plantear el problema como un objetivo, como por ejemplo:

En este caso obteniendo la solución única:

El cálculo de eventos resuelve el problema del marco, eliminando soluciones no deseadas, utilizando una lógica no monótona , como la lógica de primer orden con circunscripción [3] o tratando el cálculo de eventos como un programa lógico que utiliza la negación como falla .

Solución lógica predeterminada

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

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

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

Solución de programación del conjunto 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 negación fuerte :

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

Solución lógica de separación

La lógica de separación es un formalismo para razonar sobre programas informáticos que utiliza especificaciones pre/post de la forma . 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 *, que se pronuncia "y por separado", para respaldar el razonamiento independiente sobre regiones de memoria disjuntas. [5] [6]

La lógica de separación emplea una interpretación estricta de las especificaciones pre/post, que establecen que el código solo puede acceder a las ubicaciones de memoria cuya existencia está garantizada por la condición previa. [7] 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 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

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 llevado a aumentos significativos en la escalabilidad de las técnicas de razonamiento automatizado para código, [8] eventualmente implementadas industrialmente en bases de código con decenas de millones de líneas. [9]

Parece haber cierta similitud entre la solución de la lógica de separación para el problema del marco y la del cálculo fluido mencionado anteriormente. [ se necesita más explicación ]

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 haga que la puerta se abra si no está cerrada se expresa de la siguiente manera:

causas si

La semántica de un lenguaje de descripción de acciones depende de lo que el lenguaje puede 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 hacerlo directamente en la lógica, el problema del marco solo surge cuando se debe traducir a lógica una especificación dada en una descripción de acción. Sin embargo, normalmente se proporciona una traducción desde estos lenguajes para responder a la programación de conjuntos en lugar de a la lógica de primer orden.

Véase también

Notas

  1. ^ Hayes, Patrick (1973). "El problema del marco y problemas relacionados en inteligencia artificial". Universidad de Edimburgo .
  2. ^ McCarthy, J; PJ Hayes (1969). "Algunos problemas filosóficos desde el punto de vista de la inteligencia artificial". Machine Intelligence . 4 : 463–502. CiteSeerX 10.1.1.85.5082 . 
  3. ^ Shanahan, M. (1997) Solución del problema del marco: una investigación matemática de la ley de inercia del sentido común . MIT Press.
  4. ^ es decir, no se conoce información contradictoria
  5. ^ Reynolds, JC (2002). "Lógica de separación: una lógica para estructuras de datos mutables compartidas". Actas del 17.º Simposio anual IEEE sobre lógica en informática . Copenhague, Dinamarca: IEEE Comput. Soc. pp. 55–74. CiteSeerX 10.1.1.110.7749 . doi :10.1109/LICS.2002.1029817. ISBN .  978-0-7695-1483-3. Número de identificación del sujeto  6271346.
  6. ^ O'Hearn, Peter (28 de enero de 2019). "Lógica de separación". Comunicaciones de la ACM . 62 (2): 86–95. doi : 10.1145/3211968 . ISSN  0001-0782.
  7. ^ O'Hearn, Peter; Reynolds, John; Yang, Hongseok (2001). "Razonamiento local sobre programas que alteran estructuras de datos". En Fribourg, Laurent (ed.). Lógica informática . Apuntes de clase sobre informática. Vol. 2142. Berlín, Heidelberg: Springer. págs. 1–19. doi :10.1007/3-540-44802-0_1. ISBN. 978-3-540-44802-0.
  8. ^ Calcagno Cristiano; Dino Distefano; Peter O'Hearn; Hongseok Yang (1 de diciembre de 2011). "Análisis de la forma compositiva mediante biabducción". Revista de la ACM . 58 (6): 1–66. doi :10.1145/2049697.2049700. S2CID  52808268.
  9. ^ Distefano, Dino; Fähndrich, Manuel; Logozzo, Francesco; O'Hearn, Peter (24 de julio de 2019). "Escalando análisis estáticos en Facebook". Comunicaciones de la ACM . 62 (8): 62–70. doi : 10.1145/3338112 .

Referencias

Enlaces externos