В искусственном интеллекте , с последствиями для когнитивной науки , проблема фрейма описывает проблему с использованием логики первого порядка для выражения фактов о роботе в мире. Представление состояния робота с помощью традиционной логики первого порядка требует использования многих аксиом , которые просто подразумевают, что вещи в окружающей среде не изменяются произвольно. Например, Хейс описывает « блочный мир » с правилами о том, как складывать блоки вместе. В системе логики первого порядка требуются дополнительные аксиомы для того, чтобы делать выводы об окружающей среде (например, что блок не может изменить положение, если его физически не переместить). Проблема фрейма — это проблема нахождения адекватных наборов аксиом для жизнеспособного описания среды робота. [1]
Джон Маккарти и Патрик Дж. Хейс определили эту проблему в своей статье 1969 года « Некоторые философские проблемы с точки зрения искусственного интеллекта» . В этой статье и многих последующих формальная математическая проблема стала отправной точкой для более общих обсуждений сложности представления знаний для искусственного интеллекта. Такие вопросы, как то, как обеспечить рациональные предположения по умолчанию и то, что люди считают здравым смыслом в виртуальной среде. [2]
В философии проблема фрейма стала трактоваться более широко в связи с проблемой ограничения убеждений, которые должны обновляться в ответ на действия. В логическом контексте действия обычно определяются тем, что они изменяют, с неявным предположением, что все остальное (фрейм) остается неизменным.
Проблема фрейма возникает даже в очень простых доменах. Сценарий с дверью, которая может быть открыта или закрыта, и светом, который может быть включен или выключен, статически представлен двумя предложениями и . Если эти условия могут изменяться, их лучше представить двумя предикатами и , которые зависят от времени; такие предикаты называются флюентами . Домены, в которых дверь закрыта и свет выключен в момент времени 0, а дверь открыта в момент времени 1, могут быть напрямую представлены в логике [ необходимо разъяснение ] следующими формулами:
Первые две формулы представляют начальную ситуацию; третья формула представляет эффект выполнения действия по открытию двери в момент времени 1. Если бы такое действие имело предварительные условия, например, дверь была бы разблокирована, оно было бы представлено как . На практике можно было бы иметь предикат для указания того, когда действие выполняется, и правило для указания эффектов действий. Статья о ситуационном исчислении дает более подробную информацию.
Хотя три формулы выше являются прямым выражением в логике того, что известно, их недостаточно для правильного вывода следствий. Хотя следующие условия (представляющие ожидаемую ситуацию) согласуются с тремя формулами выше, они не единственные.
Действительно, еще один набор условий, который согласуется с тремя приведенными выше формулами, это:
Проблема фрейма заключается в том, что указание только тех условий, которые изменяются действиями, не влечет за собой, что все остальные условия не изменяются. Эту проблему можно решить, добавив так называемые «аксиомы фрейма», которые явно указывают, что все условия, не затронутые действиями, не изменяются при выполнении этого действия. Например, поскольку действие, выполненное в момент времени 0, — это открытие двери, аксиома фрейма будет утверждать, что состояние света не меняется с момента времени 0 до момента времени 1:
Проблема фрейма заключается в том, что для каждой пары действия и условия необходима одна такая аксиома фрейма, при этом действие не влияет на условие. [ необходимо разъяснение ] Другими словами, проблема заключается в формализации динамической области без явного указания аксиом фрейма.
Решение, предложенное Маккарти для решения этой проблемы, предполагает, что произошло минимальное количество изменений условий; это решение формализуется с использованием фреймворка ограничения . Однако задача стрельбы Йельского университета показывает, что это решение не всегда верно. Затем были предложены альтернативные решения, включающие завершение предикатов, текущую окклюзию, аксиомы состояния-преемника и т. д.; они объясняются ниже. К концу 1980-х годов проблема фрейма, как она определена Маккарти и Хейсом, была решена [ необходимо разъяснение ] . Однако даже после этого термин «проблема фрейма» все еще использовался, отчасти для обозначения той же проблемы, но в разных условиях (например, одновременные действия), а отчасти для обозначения общей проблемы представления и рассуждения с динамическими областями.
Следующие решения показывают, как решается проблема фрейма в различных формализмах. Сами формализмы не представлены полностью: представлены упрощенные версии, достаточные для объяснения полного решения.
Это решение было предложено Эриком Сандеваллом , который также определил формальный язык для спецификации динамических доменов; следовательно, такой домен может быть сначала выражен на этом языке, а затем автоматически переведен в логику. В этой статье показано только выражение в логике, и только на упрощенном языке без названий действий.
Обоснование этого решения заключается в том, чтобы представить не только значение условий с течением времени, но и то, могут ли они быть затронуты последним выполненным действием. Последнее представлено другим условием, называемым окклюзией. Условие считается окклюдированным в заданной точке времени, если только что было выполнено действие, которое делает условие истинным или ложным как эффект. Окклюзию можно рассматривать как «разрешение на изменение»: если условие окклюдировано, оно освобождается от подчинения ограничению инерции.
В упрощенном примере двери и света окклюзия может быть формализована двумя предикатами и . Обоснование заключается в том, что условие может изменить значение только в том случае, если соответствующий предикат окклюзии истинен в следующий момент времени. В свою очередь, предикат окклюзии истинен только тогда, когда выполняется действие, влияющее на условие.
В общем случае каждое действие, делающее условие истинным или ложным, также делает соответствующий предикат окклюзии истинным. В этом случае истинно, что делает антецедент четвертой формулы выше ложным для ; следовательно, ограничение, которое не выполняется для . Следовательно, может изменить значение, что также обеспечивается третьей формулой.
Чтобы это условие работало, предикаты окклюзии должны быть истинными только тогда, когда они становятся истинными в результате действия. Это может быть достигнуто либо путем ограничения , либо путем завершения предиката. Стоит отметить, что окклюзия не обязательно подразумевает изменение: например, выполнение действия открытия двери, когда она уже была открыта (в формализации выше), делает предикат истинным и делает истинным; однако не изменило значение, так как оно уже было истинным.
Это кодирование похоже на решение с текучей окклюзией, но дополнительные предикаты обозначают изменение, а не разрешение на изменение. Например, представляет тот факт, что предикат будет меняться с момента до . В результате предикат изменяется тогда и только тогда, когда соответствующий предикат изменения является истинным. Действие приводит к изменению тогда и только тогда, когда оно делает истинным условие, которое ранее было ложным, или наоборот.
Третья формула — это другой способ сказать, что открытие двери приводит к ее открытию. А именно, она утверждает, что открытие двери изменяет состояние двери, если она была ранее закрыта. Последние два условия утверждают, что условие изменяет значение в момент времени тогда и только тогда, когда соответствующий предикат изменения истинен в момент времени . Чтобы завершить решение, временные точки, в которых предикаты изменения истинны, должны быть как можно меньше, и это можно сделать, применив завершение предикатов к правилам, определяющим эффекты действий.
Значение условия после выполнения действия можно определить по тому факту, что условие истинно тогда и только тогда, когда:
Аксиома состояния-последователя — это логическая формализация этих двух фактов. Например, если и — два условия, используемые для обозначения того, что действие, выполненное в момент времени, состояло в том, чтобы открыть или закрыть дверь, соответственно, то работающий пример кодируется следующим образом.
Это решение сосредоточено вокруг значения условий, а не эффектов действий. Другими словами, для каждого условия есть аксиома, а не формула для каждого действия. Предпосылки к действиям (которые отсутствуют в этом примере) формализуются другими формулами. Аксиомы состояния-преемника используются в варианте исчисления ситуаций, предложенном Рэем Рейтером .
Текучее исчисление является вариантом ситуационного исчисления. Оно решает проблему фрейма, используя термины логики первого порядка , а не предикаты , для представления состояний. Преобразование предикатов в термины в логике первого порядка называется овеществлением ; текучее исчисление можно рассматривать как логику, в которой предикаты, представляющие состояние условий, овеществляются.
Разница между предикатом и термином в логике первого порядка заключается в том, что термин является представлением объекта (возможно, сложного объекта, состоящего из других объектов), тогда как предикат представляет собой условие, которое может быть истинным или ложным при оценке по заданному набору терминов.
В текучем исчислении каждое возможное состояние представлено термином, полученным путем композиции других терминов, каждый из которых представляет условия, которые истинны в состоянии. Например, состояние, в котором дверь открыта и горит свет, представлено термином . Важно отметить, что термин не является истинным или ложным сам по себе, поскольку он является объектом, а не условием. Другими словами, термин представляет возможное состояние и сам по себе не означает, что это текущее состояние. Можно указать отдельное условие, чтобы указать, что это на самом деле состояние в данный момент времени, например, означает, что это состояние в момент времени .
Решение проблемы фрейма, данное в текучем исчислении, заключается в определении эффектов действий путем указания того, как термин, представляющий состояние, изменяется при выполнении действия. Например, действие открытия двери в момент времени 0 представлено формулой:
Действие закрытия двери, которое делает условие ложным, а не истинным, представлено несколько иначе:
Эта формула работает при условии, что заданы подходящие аксиомы относительно и , например, термин, содержащий одно и то же условие дважды, не является допустимым состоянием (например, всегда ложно для любого и ).
Исчисление событий использует термины для представления флюентов, как и исчисление флюентов, но также имеет одну или несколько аксиом, ограничивающих значение флюентов, как аксиомы состояния-преемника. Существует много вариантов исчисления событий, но один из самых простых и полезных использует одну аксиому для представления закона инерции:
Аксиома гласит, что текучесть имеет место в любой момент времени , если событие происходит и начинается в более раннее время , и нет события , которое происходит и заканчивается после или в то же время, что и до .
Чтобы применить исчисление событий к конкретной проблемной области, необходимо определить и предикаты для этой области. Например:
Чтобы применить исчисление событий к конкретной проблеме в предметной области, необходимо указать события, которые происходят в контексте проблемы. Например:
Чтобы решить задачу, например, какие флюэнты сохраняются в момент времени 5?, необходимо сформулировать задачу в виде цели, например:
В этом случае получение единственного решения:
Исчисление событий решает проблему фрейма, устраняя нежелательные решения, используя немонотонную логику , такую как логика первого порядка с ограничением [3], или рассматривая исчисление событий как логическую программу, использующую отрицание в качестве отказа .
Проблему фрейма можно рассматривать как проблему формализации принципа, что по умолчанию «все предполагается в том состоянии, в котором оно находится» ( Лейбниц , «Введение в секретную энциклопедию», ок . 1679). Это умолчание, иногда называемое законом инерции здравого смысла , было выражено Раймондом Рейтером в логике умолчаний :
(если истинно в ситуации , и можно предположить [4] , что остается истинным после выполнения действия , то мы можем заключить, что остается истинным).
Стив Хэнкс и Дрю Макдермотт утверждали, основываясь на своем примере стрельбы из Йеля , что это решение проблемы кадра неудовлетворительно. Хадсон Тернер показал, однако, что оно работает правильно при наличии соответствующих дополнительных постулатов.
Аналогом логического решения по умолчанию на языке программирования наборов ответов является правило с сильным отрицанием :
(если истинно в момент времени , и можно предположить, что остается истинным в момент времени , то мы можем заключить, что остается истинным).
Разделительная логика — это формализм для рассуждений о компьютерных программах с использованием пред/пост спецификаций формы . Разделительная логика — это расширение логики Хоара, ориентированное на рассуждения об изменчивых структурах данных в компьютерной памяти и других динамических ресурсах, и в ней есть специальный соединительный элемент *, произносимый как «и отдельно», для поддержки независимых рассуждений о непересекающихся областях памяти. [5] [6]
Логика разделения использует строгую интерпретацию спецификаций pre/post, которые говорят, что код может получить доступ только к тем ячейкам памяти, существование которых гарантировано предварительным условием. [7] Это приводит к обоснованности самого важного правила вывода логики, правила фрейма.
Правило фрейма позволяет добавлять описания произвольной памяти за пределами следа (памяти, к которой осуществляется доступ) кода к спецификации: это позволяет первоначальной спецификации сосредоточиться только на следе. Например, вывод
фиксирует тот код, который сортирует список x, но не рассортировывает отдельный список y, и делает это без упоминания y в исходной спецификации над строкой.
Автоматизация правила фрейма привела к значительному повышению масштабируемости автоматизированных методов рассуждения для кода [8] , в конечном итоге развернутых в промышленных масштабах для кодовых баз с десятками миллионов строк. [9]
Кажется, существует некоторое сходство между решением проблемы фрейма с помощью логики разделения и решением упомянутого выше текучего исчисления. [ необходимо дополнительное объяснение ]
Языки описания действий уклоняются от проблемы фрейма, а не решают ее. Язык описания действий — это формальный язык с синтаксисом, который специфичен для описания ситуаций и действий. Например, то, что действие заставляет дверь открываться, если она не заперта, выражается следующим образом:
Семантика языка описания действий зависит от того, что язык может выразить (одновременные действия, отложенные эффекты и т. д.), и обычно основана на системах переходов .
Поскольку домены выражаются в этих языках, а не напрямую в логике, проблема фрейма возникает только тогда, когда спецификация, заданная в логике описания действия, должна быть переведена в логику. Однако обычно перевод дается из этих языков для ответа на программирование множеств, а не на логику первого порядка.