Проблема с рамой

В искусственном интеллекте , имеющем последствия для когнитивной науки , проблема фрейма описывает проблему использования логики первого порядка для выражения фактов о роботе в мире. Представление состояния робота с помощью традиционной логики первого порядка требует использования множества аксиом , которые просто подразумевают, что вещи в окружающей среде не меняются произвольно. Например, Хейс описывает « мир блоков » с правилами складывания блоков вместе. В логической системе первого порядка требуются дополнительные аксиомы, чтобы делать выводы об окружающей среде (например, что блок не может изменить положение, если его не перемещать физически). Проблема фрейма — это проблема поиска адекватного набора аксиом для жизнеспособного описания среды робота.

Джон Маккарти и Патрик Дж. Хейс определили эту проблему в своей статье 1969 года « Некоторые философские проблемы с точки зрения искусственного интеллекта» . В этой статье, как и во многих последующих, формальная математическая проблема стала отправной точкой для более общего обсуждения сложности представления знаний для искусственного интеллекта. Такие вопросы, как обеспечение рациональных допущений по умолчанию и то, что люди считают здравым смыслом в виртуальной среде.

В философии проблема фреймов стала трактоваться более широко в связи с проблемой ограничения убеждений, которые должны обновляться в ответ на действия. В логическом контексте действия обычно определяются тем, что они меняют, при неявном предположении, что все остальное (фрейм) остается неизменным.

Описание

Проблема фрейма возникает даже в очень простых доменах. Сценарий с дверью, которая может быть открыта или закрыта, и светом, который может быть включен или выключен, статически представлен двумя предложениями. $\mathrm {open}$ и $\mathrm {on}$. Если эти условия могут измениться, их лучше представить двумя предикатами. $\mathrm {open} (t)$ и $\mathrm {on} (t)$которые зависят от времени; такие предикаты называются флюэнтами . Область, в которой дверь закрыта и свет выключен в момент времени 0, а дверь открыта в момент времени 1, может быть непосредственно представлена ​​в логике. по следующим формулам:

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

$\neg \mathrm {on} (0)$

$\mathrm {open} (1)$

Первые две формулы представляют исходную ситуацию; третья формула представляет собой эффект выполнения действия по открытию двери в момент времени 1. Если бы такое действие имело предварительные условия, такие как отпирание двери, оно было бы представлено выражением $\neg \mathrm {locked} (0)\implies \mathrm {open} (1)$. На практике можно было бы иметь предикат $\mathrm {executeopen} (t)$ для указания момента выполнения действия и правила $\forall t.\mathrm {executeopen} (t)\implies \mathrm {open} (t+1)$для определения последствий действий. статье о ситуационном исчислении Более подробная информация представлена ​​в .

Хотя три приведенные выше формулы являются прямым логическим выражением того, что известно, их недостаточно для правильного вывода следствий. Хотя следующие условия (представляющие ожидаемую ситуацию) согласуются с тремя приведенными выше формулами, они не единственные.

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

Действительно, еще один набор условий, который согласуется с тремя приведенными выше формулами, таков:

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

Проблема фрейма заключается в том, что указание только того, какие условия изменяются действиями, не влечет за собой, что все остальные условия не изменяются. Эту проблему можно решить, добавив так называемые «аксиомы фрейма», которые явно указывают, что все условия, на которые не влияют действия, не изменяются при выполнении этого действия. Например, поскольку действие, выполняемое в момент времени 0, — это открытие двери, аксиома фрейма будет утверждать, что состояние света не меняется от времени 0 до момента 1:

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

Проблема фрейма заключается в том, что для каждой пары действия и условия необходима одна такая аксиома фрейма, чтобы действие не влияло на условие. Другими словами, проблема заключается в формализации динамической области без явного указания аксиом фрейма.

Решение, предложенное Маккарти для решения этой проблемы, предполагает предположение, что произошло минимальное количество изменений условий; это решение формализуется с использованием структуры ограничения . Однако проблема стрельбы в Йельском университете показывает, что это решение не всегда правильное. Затем были предложены альтернативные решения, включающие завершение предикатов, плавное закрытие, аксиомы состояний-преемников и т. д.; они объяснены ниже. К концу 1980-х годов проблема фрейма, определенная Маккарти и Хейсом, была решена. . Однако даже после этого термин «проблема фрейма» все еще использовался, частично для обозначения одной и той же проблемы, но в разных условиях (например, параллельные действия), а частично для обозначения общей проблемы представления и рассуждения с помощью динамических домены.

Решения

Следующие решения показывают, как проблема фрейма решается в различных формализмах. Сами формализмы не представлены полностью: представлены упрощенные версии, достаточные для объяснения полного решения.

Решение для плавной окклюзии

Это решение было предложено Эриком Сандеволлом , который также определил формальный язык для спецификации динамических областей; следовательно, такая область может быть сначала выражена на этом языке, а затем автоматически переведена в логику. В этой статье показано только логическое выражение и только на упрощенном языке без названий действий.

Смысл этого решения заключается в том, чтобы представить не только значение условий с течением времени, но и то, может ли на них повлиять последнее выполненное действие. Последнее представлено другим состоянием, называемым окклюзией. Говорят, что условие закрыто в данный момент времени, если только что было выполнено действие, в результате которого условие становится истинным или ложным. Окклюзию можно рассматривать как «разрешение на изменение»: если условие закрыто, оно освобождается от подчинения ограничению инерции.

В упрощенном примере с дверью и светом окклюзия может быть формализована двумя предикатами. $\mathrm {occludeopen} (t)$ и $\mathrm {occludeon} (t)$. Смысл в том, что условие может изменить значение только в том случае, если соответствующий предикат окклюзии истинен в следующий момент времени. В свою очередь, предикат окклюзии истинен только тогда, когда выполняется действие, влияющее на условие.

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

$\neg \mathrm {on} (0)$

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

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

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

В общем, каждое действие, делающее условие истинным или ложным, также делает истинным соответствующий предикат окклюзии. В этом случае, $\mathrm {occludeopen} (1)$ верно, что делает антецедент четвертой формулы выше ложным для $t=1$; следовательно, ограничение, которое $\mathrm {open} (t-1)\iff \mathrm {open} (t)$ не выдерживает $t=1$. Поэтому, $\mathrm {open}$ может изменить значение, что также обеспечивается третьей формулой.

Чтобы это условие работало, предикаты перекрытия должны быть истинными только тогда, когда они становятся истинными в результате действия. Этого можно достичь либо путем ограничения , либо путем завершения предиката. Стоит заметить, что окклюзия не обязательно подразумевает изменение: например, выполнение действия открытия двери, когда она уже была открыта (в формализации выше), делает предикат $\mathrm {occludeopen}$ правда и делает $\mathrm {open}$истинный; однако, $\mathrm {open}$ не изменило значения, как это уже было верно.

Решение для завершения предиката

Это кодирование похоже на решение с плавным перекрытием, но дополнительные предикаты обозначают изменение, а не разрешение на изменение. Например, $\mathrm {changeopen} (t)$ представляет собой тот факт, что предикат $\mathrm {open}$ изменится со временем $t$ к $t+1$. В результате предикат изменяется тогда и только тогда, когда соответствующий предикат изменения истинен. Действие приводит к изменению тогда и только тогда, когда оно делает условие, которое ранее было ложным, и наоборот.

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

$\neg \mathrm {on} (0)$

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

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

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

Третья формула — это другой способ сказать, что открытие двери приводит к открытию двери. А именно, там говорится, что открытие двери меняет состояние двери, если она была ранее закрыта. Последние два условия утверждают, что условие меняет значение во времени. $t$ тогда и только тогда, когда соответствующий предикат изменения истинен в данный момент $t$. Чтобы завершить решение, моментов времени, в которых предикаты изменения являются истинными, должно быть как можно меньше, и это можно сделать, применив завершение предикатов к правилам, определяющим последствия действий.

состояния

Значение условия после выполнения действия можно определить по формуле тот факт, что условие истинно тогда и только тогда, когда:

1. действие делает условие истинным; или
2. условие ранее было истинным, и действие не делает его ложным.

представляет Аксиома государства-преемника собой логическую формализацию этих двух фактов. Для например, если $\mathrm {opendoor} (t)$ и $\mathrm {closedoor} (t)$два условия, используемые для обозначения того, что действие выполняется в данный момент $t$был открыть или закрыть дверь соответственно, запущенный пример кодируется как следует.

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

$\neg \mathrm {on} (0)$

$\mathrm {opendoor} (0)$

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

Это решение сосредоточено вокруг ценности условий, а не последствия действий. Другими словами, для каждого условия существует аксиома: а не формула для каждого действия. Предпосылки к действию (которые не присутствующие в этом примере) формализуются другими формулами. Государство-преемник аксиомы используются в варианте исчисления ситуаций, предложенном Рэй Рейтер .

Свободное решение исчисления

Беглое исчисление является разновидностью ситуационного исчисления. Он решает проблему фрейма, используя логику первого порядка. термины , а не предикаты, для представления состояний. Преобразование предикаты в термины в логике первого порядка называются овеществлением ; тот беглое исчисление можно рассматривать как логику, в которой предикаты, представляющие состояние условий овеществлено.

Разница между предикатом и термином в логике первого порядка заключается в том, что термин представляет собой представление объекта (возможно, сложного объекта, состоящего из других объектов), тогда как предикат представляет собой условие, которое может быть истинным или ложным при оценке по некоторому значению. заданный набор условий.

В беглом исчислении каждое возможное состояние представлено термином, полученным композицией других членов, каждый из которых представляет условия, которые истинны в данном состоянии. Например, состояние, в котором дверь открыта и свет горит, обозначается термином $\mathrm {open} \circ \mathrm {on}$. Важно отметить, что термин сам по себе не является истинным или ложным, поскольку он является объектом, а не условием. Другими словами, термин $\mathrm {open} \circ \mathrm {on}$представляют возможное состояние и само по себе не означает, что это текущее состояние. Можно указать отдельное условие, чтобы указать, что это действительно состояние в данный момент времени, например: $\mathrm {state} (\mathrm {open} \circ \mathrm {on} ,10)$ означает, что это состояние в данный момент $10$.

Решение проблемы фрейма, данное в беглом исчислении, состоит в том, чтобы указать эффекты действий, указав, как член, представляющий состояние, изменяется при выполнении действия. Например, действие открытия двери в момент 0 представляется формулой:

$\mathrm {state} (s\circ \mathrm {open} ,1)\iff \mathrm {state} (s,0)$

Действие закрытия двери, которое делает условие ложным вместо истинного, представлено несколько иначе:

$\mathrm {state} (s,1)\iff \mathrm {state} (s\circ \mathrm {open} ,0)$

Эта формула работает при условии, что даны подходящие аксиомы относительно $\mathrm {state}$ и $\circ$, например, термин, содержащий одно и то же условие дважды, не является допустимым состоянием (например, $\mathrm {state} (\mathrm {open} \circ s\circ \mathrm {open} ,t)$ всегда ложно для каждого $s$ и $t$).

Решение для исчисления событий

Исчисление событий использует термины для представления беглых состояний, например, исчисление беглости, но также имеет одну или несколько аксиом, ограничивающих ценность беглых состояний, например аксиомы состояний-преемников. Существует множество вариантов исчисления событий, но один из самых простых и полезных использует одну аксиому, описывающую закон инерции:

${\mathit {holdsAt}}(F,T2)\leftarrow$

$[{\mathit {happensAt}}(E1,T1)\wedge {\mathit {initiates}}(E1,F,T1)\wedge (T1<T2)\wedge$

$\neg \exists E2,T[{\mathit {happensAt}}(E2,T)\wedge {\mathit {terminates}}(E2,F,T)\wedge (T1\leq T<T2)]$

Аксиома гласит, что беглый $F$ держится за раз $T2$, если событие $E1$ происходит и инициируется $F$ в более раннее время $T1$, и нет никакого события $E2$ это происходит и прекращается $F$ после или одновременно с $T1$ и раньше $T2$.

Чтобы применить исчисление событий к конкретной проблемной области, необходимо определить $initiates$ и $terminates$предикаты для этого домена. Например:

${\mathit {initiates}}(opendoor,open,T).$

${\mathit {terminates}}(opendoor,closed,T).$

${\mathit {initiates}}(closedoor,closed,T).$

${\mathit {terminates}}(closeddoor,open,T).$

Чтобы применить исчисление событий к конкретной проблеме в предметной области, необходимо указать события, которые происходят в контексте проблемы. Например:

${\mathit {happensAt}}(opendoor,0)$.

${\mathit {happensAt}}(closedoor,3)$.

Чтобы решить проблему, например, какие беглые слова сохраняются в момент 5? , необходимо поставить проблему как цель, например:

$\exists Fluent[{\mathit {holdsAt(Fluent,5)}}].$

В этом случае получение единственного решения:

$Fluent=closed.$

Исчисление событий решает проблему фрейма, устраняя нежелательные решения, используя немонотонную логику , например логику первого порядка с ограничением. или рассматривая исчисление событий как логическую программу, используя отрицание как неудачу .

Логическое решение по умолчанию

Проблему фрейма можно рассматривать как проблему формализации принципа, согласно которому по умолчанию «предполагается, что все остается в том состоянии, в котором оно есть» ( Лейбниц , «Введение в секретную энциклопедию», ок . 1679). Это значение по умолчанию, иногда называемое законом инерции здравого смысла , было выражено Раймондом Рейтером в логике по умолчанию :

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

(если $R(x)$ верно в ситуации $s$, и можно предположить что $R(x)$ остается истинным после выполнения действия $a$, то мы можем заключить, что $R(x)$ остается верным).

Стив Хэнкс и Дрю МакДермотт , основываясь на своем примере со стрельбой в Йельском университете , утверждали , что такое решение проблемы кадра является неудовлетворительным. Однако Хадсон Тернер показал, что она работает правильно при наличии соответствующих дополнительных постулатов.

Решение для программирования набора ответов

Аналогом логического решения по умолчанию на языке программирования набора ответов является правило со строгим отрицанием :

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

(если $r(X)$ это правда в свое время $T$, и можно предположить, что $r(X)$ остается верным во времени $T+1$, то мы можем заключить, что $r(X)$ остается верным).

Логическое решение разделения

Логика разделения - это формализм для рассуждений о компьютерных программах с использованием спецификаций до / после формы $\{\mathrm {precondition} \}\ \mathrm {code} \ \{\mathrm {postcondition} \}$. Логика разделения — это расширение логики Хоара, ориентированное на рассуждения об изменяемых структурах данных в компьютерной памяти и других динамических ресурсах, и она имеет специальную связку *, произносимую «и отдельно», для поддержки независимых рассуждений о непересекающихся областях памяти.

Логика разделения использует строгую интерпретацию спецификаций до и после, которые говорят, что код может получить доступ только к областям памяти, существование которых гарантировано предварительным условием. Это приводит к правильности самого важного правила логического вывода — правила фрейма .

${\frac {\{\mathrm {precondition} \}\ \mathrm {code} \ \{\mathrm {postcondition} \}}{\{\mathrm {precondition} \ast \mathrm {frame} \}\ \mathrm {code} \ \{\mathrm {postcondition} \ast \mathrm {frame} \}}}$

Правило фрейма позволяет добавлять в спецификацию описания произвольной памяти за пределами занимаемого пространства (памяти, к которой осуществляется доступ) кода: это позволяет исходной спецификации концентрироваться только на занимаемом месте. Например, вывод

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

фиксирует тот код, который сортирует список x , не сортируя отдельный список y, и делает это без упоминания y вообще в исходной спецификации над строкой.

Автоматизация правила фрейма привела к значительному увеличению масштабируемости методов автоматического рассуждения для кода. в конечном итоге промышленно развернуто в кодовых базах с десятками миллионов строк.

Кажется, существует некоторое сходство между решением проблемы фрейма с помощью логики разделения и решением упомянутой выше беглого исчисления.

Языки описания действий

Языки описания действий скорее ускользают от проблемы фрейма, чем решают ее. Язык описания действий — это формальный язык с синтаксисом, специфичным для описания ситуаций и действий. Например, что действие $\mathrm {opendoor}$ заставляет дверь открываться, если она не заперта, выражается:

$\mathrm {opendoor}$ причины $\mathrm {open}$ если $\neg \mathrm {locked}$

Семантика языка описания действий зависит от того, что язык может выражать (одновременные действия, отложенные эффекты и т. д.) и обычно основана на системах переходов .

Поскольку домены выражаются на этих языках, а не непосредственно в логике, проблема фрейма возникает только тогда, когда спецификация, заданная в логике описания действия, должна быть переведена в логику. Однако обычно с этих языков дается перевод для ответа на программирование множеств, а не на логику первого порядка.

См. также

• Проблема привязки
• Здравый смысл
• Рассуждения здравого смысла
• Оправданное рассуждение
• Линейная логика
• Логика разделения
• Немонотонная логика
• Проблема квалификации
• Проблема ветвления
• Символ заземления
• Проблема со стрельбой в Йельском университете

Ссылки

• Доэрти, П.; Густафссон Дж.; Карлссон, Л.; Кварнстрем, Дж. (1998). «TAL: Спецификация языка логики временных действий и учебное пособие» . Электронные транзакции по искусственному интеллекту . 2 (3–4): 273–306.
• Гельфонд, М.; Лифшиц, В. (1993). «Представление действий и изменений с помощью логических программ». Журнал логического программирования . 17 (2–4): 301–322. дои : 10.1016/0743-1066(93)90035-ф .
• Гельфонд, М.; Лифшиц, В. (1998). «Языки действия» . Электронные транзакции по искусственному интеллекту . 2 (3–4): 193–210.
• Хэнкс, С.; Макдермотт, Д. (1987). «Немонотонная логика и временная проекция». Искусственный интеллект . 33 (3): 379–412. дои : 10.1016/0004-3702(87)90043-9 .
• Левеск, Х.; Пирри, Ф.; Райтер, Р. (1998). «Основы ситуационного расчета» . Электронные транзакции по искусственному интеллекту . 2 (3–4): 159–178.
• Либераторе, П. (1997). «Сложность языка А» . Электронные транзакции по искусственному интеллекту . 1 (1–3): 13–37.
• Лифшиц, В. (2012). «Проблема рамы тогда и сейчас» (PDF) . Техасский университет в Остине . Архивировано (PDF) из оригинала 11 февраля 2014 г. Представлено на праздновании достижений Джона Маккарти в Стэнфордском университете 25 марта 2012 г.
• Маккарти, Дж.; Хейс, П.Дж. (1969). «Некоторые философские проблемы с точки зрения искусственного интеллекта» . Машинный интеллект . 4 : 463–502. CiteSeerX   10.1.1.85.5082 .
• Маккарти, Дж. (1986). «Применение ограничений для формализации здравого смысла» . Искусственный интеллект . 28 : 89–116. CiteSeerX   10.1.1.29.5268 . дои : 10.1016/0004-3702(86)90032-9 .
• Миллер, Р.; Шанахан, М. (1999). «Исчисление событий в классической логике – альтернативные аксиоматизации» . Электронные транзакции по искусственному интеллекту . 3 (1): 77–105.
• Пирри, Ф.; Райтер, Р. (1999). «Некоторые вклады в метатеорию ситуационного исчисления». Журнал АКМ . 46 (3): 325–361. дои : 10.1145/316542.316545 . S2CID   16203802 .
• Райтер, Р. (1980). «Логика рассуждений по умолчанию» (PDF) . Искусственный интеллект . 13 (1–2): 81–132. CiteSeerX   10.1.1.250.9224 . дои : 10.1016/0004-3702(80)90014-4 .
• Райтер, Р. (1991). «Проблема фрейма в ситуационном исчислении: простое решение (иногда) и результат полноты для регрессии цели». В Лифшице, Владимире (ред.). Искусственный интеллект и математическая теория вычислений: статьи в честь Джона Маккарти . Нью-Йорк: Академическая пресса. стр. 359–380. CiteSeerX   10.1.1.137.2995 .
• Сандеволл, Э. (1972). «Подход к проблеме фрейма и ее реализация». Машинный интеллект . 7 : 195–204.
• Сандеволл, Э. (1994). Особенности и Fluents . Том. (т. 1). Нью-Йорк: Издательство Оксфордского университета. ISBN  978-0-19-853845-5 .
• Сандеволл, Э.; Шохам, Ю. (1995). «Немонотонные временные рассуждения». В Габбае, DM; Хоггер, CJ; Робинсон, Дж. А. (ред.). Справочник по логике в искусственном интеллекте и логическом программировании . Том. (т. 4). Издательство Оксфордского университета. стр. 439–498. ISBN  978-0-19-853791-5 .
• Сандеволл, Э. (1998). «Когнитивная логика робототехники и ее метатеория: новый взгляд на особенности и беглость речи» . Электронные транзакции по искусственному интеллекту . 2 (3–4): 307–329.
• Шанахан, М. (1997). Решение проблемы каркаса: математическое исследование здравого закона инерции . МТИ Пресс. ISBN  9780262193849 .
• Тильшер, М. (1998). «Введение в беглый исчисление» . Электронные транзакции по искусственному интеллекту . 2 (3–4): 179–192.
• Тот, Дж. А. (1995). «Рецензия на книгу. Кеннет М. и Патрик Дж. Хейс, ред.» . Рассуждающие агенты в динамическом мире: проблема фрейма. Искусственный интеллект . 73 (1–2): 323–369. дои : 10.1016/0004-3702(95)90043-8 .
• Тернер, Х. (1997). «Представление действий в логических программах и теориях по умолчанию: подход ситуационного исчисления» (PDF) . Журнал логического программирования . 31 (1–3): 245–298. дои : 10.1016/s0743-1066(96)00125-2 .

Внешние ссылки

• Залта, Эдвард Н. (ред.). «Проблема кадра» . Стэнфордская энциклопедия философии .
• Некоторые философские проблемы с точки зрения искусственного интеллекта ; оригинальная статья Маккарти и Хейса, в которой была предложена проблема.