stringtranslate.com

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

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

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

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

Описание

Проблема фрейма возникает даже в очень простых доменах. Сценарий с дверью, которая может быть открытой или закрытой, и светом, который может быть включен или выключен, статически представлен двумя предложениями и . Если эти условия могут измениться, их лучше представить двумя предикатами , зависящими от времени; такие предикаты называются флюэнтами . Область, в которой дверь закрыта и свет выключен в момент времени 0, а дверь открыта в момент времени 1, может быть непосредственно представлена ​​в логике [ необходимы пояснения ] следующими формулами:

Первые две формулы представляют исходную ситуацию; третья формула представляет собой эффект выполнения действия по открытию двери в момент 1. Если бы такое действие имело предварительные условия, такие как отпирание двери, оно было бы представлено как . На практике можно было бы иметь предикат для указания момента выполнения действия и правило для определения последствий действий. Более подробная информация представлена ​​в статье о ситуационном исчислении .

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

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

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

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

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

Решения

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

Свободное окклюзионное решение

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

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

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

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

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

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

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

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

Решение аксиом состояния преемника

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

.
.

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

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

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

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

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

(если верно в ситуации и можно предположить [4] , что оно остается истинным после выполнения действия , то можно сделать вывод, что оно остается истинным).

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

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

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

(если истинно в момент времени и можно предположить, что оно остается истинным в момент времени , то мы можем заключить, что оно остается истинным).

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

Логика разделения — это формализм для рассуждений о компьютерных программах с использованием спецификаций до и после в форме . Логика разделения — это расширение логики Хоара, ориентированное на рассуждения об изменяемых структурах данных в компьютерной памяти и других динамических ресурсах, и она имеет специальную связку *, произносимую «и отдельно», для поддержки независимых рассуждений о непересекающихся областях памяти. [5] [6]

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

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

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

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

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

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

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

причины , если

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

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

Смотрите также

Примечания

  1. ^ Хейс, Патрик (1973). «Проблема фрейма и связанные с ней проблемы искусственного интеллекта». Эдинбургский университет .
  2. ^ Маккарти, Дж; Пи Джей Хейс (1969). «Некоторые философские проблемы с точки зрения искусственного интеллекта». Машинный интеллект . 4 : 463–502. CiteSeerX 10.1.1.85.5082 . 
  3. ^ Шанахан, М. (1997) Решение проблемы каркаса: математическое исследование здравого закона инерции . МТИ Пресс.
  4. ^ т.е. противоречивая информация неизвестна
  5. ^ Рейнольдс, JC (2002). «Логика разделения: логика для общих изменяемых структур данных». Материалы 17-го ежегодного симпозиума IEEE по логике в информатике . Копенгаген, Дания: IEEE Comput. Соц. стр. 55–74. CiteSeerX 10.1.1.110.7749 . дои : 10.1109/LICS.2002.1029817. ISBN  978-0-7695-1483-3. S2CID  6271346.
  6. ^ О'Хирн, Питер (28 января 2019 г.). «Логика разделения». Коммуникации АКМ . 62 (2): 86–95. дои : 10.1145/3211968 . ISSN  0001-0782.
  7. ^ О'Хирн, Питер; Рейнольдс, Джон; Ян, Хонсок (2001). Фрибур, Лоран (ред.). Локальные рассуждения о программах, изменяющих структуры данных . Конспекты лекций по информатике. Том. 2142. Берлин, Гейдельберг: Springer. стр. 1–19. дои : 10.1007/3-540-44802-0_1. ISBN 978-3-540-44802-0. {{cite book}}: |journal=игнорируется ( помощь )
  8. ^ Кальканьо Криштиану; Дино Дистефано; Питер О'Хирн; Хонсок Ян (01 декабря 2011 г.). «Композиционный анализ формы посредством биабдукции». Журнал АКМ . 58 (6): 1–66. дои : 10.1145/2049697.2049700. S2CID  52808268.
  9. ^ Дистефано, Дино; Фендрих, Мануэль; Логоццо, Франческо; О'Хирн, Питер (24 июля 2019 г.). «Масштабирование статического анализа в Facebook». Коммуникации АКМ . 62 (8): 62–70. дои : 10.1145/3338112 .

Рекомендации

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