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

В области искусственного интеллекта , то проблема кадров описывает проблему с помощью логики первого порядка , чтобы выразить факты о роботе в мире. Представление состояния робота с помощью логики первого порядка требует использования многих аксиом, которые просто подразумевают, что вещи в окружающей среде не изменяются произвольно. Например, Хейс описывает « блочный мир » с правилами объединения блоков. Проблема фрейма - это проблема поиска адекватных наборов аксиом для жизнеспособного описания среды робота. ^[1]

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

Описание [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

Решения [ править ]

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

Раствор для плавной окклюзии [ править ]

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Решение аксиом государства-преемника [ править ]

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

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

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

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

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

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

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

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

Решение для беглого исчисления [ править ]

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

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

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

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

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

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

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

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

Решение для исчисления событий [ править ]

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

Логическое решение по умолчанию [ править ]

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

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

(если верно в ситуации , и можно предположить ^[3], что остается верным после выполнения действия , то мы можем сделать вывод, что остается верным).${\displaystyle R(x)}$${\displaystyle s}$${\displaystyle R(x)}$${\displaystyle a}$${\displaystyle R(x)}$

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

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

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

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

(если верно во время , и можно предположить, что остается верным во время , то мы можем сделать вывод, что остается верным).${\displaystyle r(X)}$${\displaystyle T}$${\displaystyle r(X)}$${\displaystyle T+1}$${\displaystyle r(X)}$

Логическое решение разделения [ править ]

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

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

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

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

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

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

Автоматизация правила кадра привела к значительному увеличению масштабируемости автоматизированных методов рассуждений для кода ^{[7], которые в} конечном итоге были развернуты в промышленных масштабах для кодовых баз с десятками миллионов строк. ^[8]

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

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

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

${\displaystyle \mathrm {opendoor} }$вызывает если${\displaystyle \mathrm {open} }$${\displaystyle \neg \mathrm {locked} }$

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

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

См. Также [ править ]

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

Заметки [ править ]

Ссылки [ править ]

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

Внешние ссылки [ править ]

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