QA3 (Question Answering system, version 3): обзор

В июле 1969 года Кордел Грин (Cordell Green) представил публике свою диссертационную работу [Green C., 1969a], посвященную вопросно-ответной системе, которая называлась QA3. Система QA3 хотя и была вопросно-ответной системой, однако содержала в себе еще и механизмы для решения задач. В частности, эта система могла отвечать на вопросы такого типа: "Существует ли последовательность действий такая, что объект object1 окажется в комнате room4, если изначально он находится в комнате room2?" Такая формулировка вопроса является, по сути, постановкой задачи планирования. Но так как целю системы QA3 были все-таки ответы на вопросы, а не решение задач, да и реализация механизма решения задач имела множество ограничений, эта система не претендует на звание первого планировщика.

Работа системы QA3 основывалась на механизме доказательства теорем методом резолюций. Т.е. вопросы к системе формулировались в виде формул исчисления предикатов первого порядка (first-order logic). В такой же форме хранились и знания. Формула-вопрос рассматривалась как теорема, которую нужно доказать, основываясь на формулах-знаниях. Система выдавала результат, в котором содержалась информация о том, нашла ли система ответ, и множество значений для переменных из формулы-вопроса, которые и являлись ответом. Например, вопрос можно было сформулировать так "Кто родился в 1831 году?" Этот вопрос можно переформулировать, например следующим образом: "Существует ли z такое, что родился z в 1831 году?". Такая формулировка имеет прямое отражение в формулу исчисления предикатов первого порядка. Система QA3 ищет ответ на этот вопрос-формулу, проверяя выводимость формулы-вопроса из формул-знаний системы. При выводе определяется подстановка для z, которая и будет ответом. Например, система может вывести что z="Шишкин Иван Иванович — известный русский живописец".

Кратко рассмотрим, как же система QA3 отвечала на вопросы о последовательностях действий. Чуть ранее, в мае 1969 года в трудах 1-ой Международной конференции по искусственному интеллекту (IJCAI'69) Грин описал [Green C., 1969b] технологию, как можно решать задачу о существовании целенаправленной последовательности действий при помощи доказательства теорем методом резолюций. Он нашел способ описания состояний (state) и преобразований состояний (state transformation) в рамках исчисления предикатов. Рассмотрим на примере, как он это сделал.

Факты о мире, на вопросы о котором отвечает система, выражались в форме предложений логики предикатов первого порядка (далее просто, логики первого порядка). Вопросы формулировались в виде утверждений, которые необходимо доказать. Предполагалось, что в любой момент времени мир находится в некотором состоянии. Будем обозначать состояния буквой s с индексом внизу, например, s7. Состояния описываются при помощи предикатов. Например, если предикат AT(object1, room4, s1) истинен, то это значит, что в состоянии s1 объект object1 находится в комнате room4. Множество предикатов, связанных с одним состоянием и будут полностью определять состояние. Пусть вышеозначенный предикат будет аксиомой A1.

A1:   AT(object1, room4, s1)

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

("s) [ P(s) —> Q(f(s)) ]

где
s — переменная, обозначающая состояние (state variable),
P — предикат, описывающий состояние до применения действия,
Q — предикат, описывающий состояние после применения действия,
f — функция (соответствующая некоторому действию), которая отражает некоторое состояние в новое состояние (достигаемое посредством выполнения действия).

В качестве примера рассмотрим аксиому, описывающую то, что предмет object1 может быть перемещен из комнаты room4 в комнату room2.

A2:   ("s) [ AT(object1, room4, s) —> AT(object1, room2, transfer(object1, room4, room2, s)) ]

Здесь функция transfer(object1, room4, room2, s) соответствует действию перемещения предмета object1 из room4 в room2.

Теперь рассмотрим вопрос "существует ли последовательность действий такая, что предмет object1 будет находиться в room2?" Тот же вопрос можно выразить следующей фразой, "существует ли состояние, возможно полученное в результате применения действий-функций, такое, что предмет object1 будет находиться в room2?" Этот вопрос может быть записан в виде утверждения в логике первого порядка: ($s) AT(object1, room2, s). Это утверждение может быть доказано на основании аксиом A1 и A2 при помощи метода резолюций. И в качестве ответа будет выступать подстановка s=transfer(object1, room4, room2, s1).

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

Например, пусть у нас есть еще одна аксиома:

A3:   ("s) [ AT(object1, room2, s) —> AT(object1, room9, transfer(object1, room2, room9, s)) ].

Тогда последовательность действий, перемещающая предмет object1 из помещения room4 в room9, начиная с состояния s1, может быть записана следующим образом через композицию функций: transfer(object1, room2, room9, transfer(object1, room4, room2, s1)).

В той же работе Грин приводит расширенный вариант формулировки задачи. В предыдущем варианте мы не могли указать начальное состояние как параметр поиска. Грин предложил более гибкий вариант формулировки, в которой функция-действие отражает не предикат до применения действия в предикат после применения действия, а состояние в новое состояние. В качестве аргументов эта функция получает действие и состояние, к которому действие применяется, а на выходе формируется новое состояние — newState=function(action, oldState). Используя такой формализм, мы можем внести начальное состояние мира в постановку задачи. Например, задача может быть сформулирована так, "существует ли последовательность действий x, которая отражает состояние s0 в состояние, в котором истинен предикат Q?" Или, говоря математическим языком, ($x) Q(f(x, s0)). Например, ($x) AT(object1, room2, f(x, s0)).

Кроме этого Грин предложил использовать (при необходимости) аксиомы, не изменяющие состояние. Эти аксиомы являлись, по сути, импликацией в рамках состояния и могли служить, например, для отражения зависимости между объектами. Полезность таких аксиом можно продемонстрировать следующим утверждением: (" x, y, z, s) [ LEFT(x, y, s) & LEFT(y, z, s) —> LEFT(x, z, s) ]. Т.е. Если объект x находится левее y, а объект y находится левее z, то и x находится левее z в любом состоянии.

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

ACE1:      (" w, x, y, z) [ w = x —> select(w, x, y, z) = y ]

ACE2:   (" w, x, y, z) [ ¬(w = x) —> select(w, x, y, z) = z ]

Тогда условный эффект можно было выразить при помощи перехода в то или иное состояние в зависимости от некоторого условия. Например, выражение для получения состояния по условию можно записать так: s = select(a, b, f(x, s0), f(y, s0), т.е. в зависимости от равенства a и b будет выполнено действие x или y.

Не смотря на возможность решать некоторые задачи планирования, система не получила развития, как планировщик. Система STRIPS использовала только часть методов QA3, а именно, доказательство теорем методом резолюций.

 

Библиография

[Green C., 1969a]
Green C., The Application of Theorem Proving to Question-Answering System. Garland Publishing, New York, 1969.
[Green C., 1969b]
Green C., Application of Theorem Proving to Problem Solving. IJCAI'69, 1969, стр. 219-240.

 

Трофимов И.В.

апрель 2005